name the dependent type used in precategory_data, for use in other proofs
Declare precategory_id_comp to take values in UU

Unfortunately, total2, and hence dirprod, take values in
Type, and thus certain uses of "destruct" don't work
because UU and Type don't match.

A better fix would be to declare total2 to take values
in UU, but that breaks some coercions, because UU is
not a "SortClass".
undo previous commit
improve "make TAGS" command
Merge branch 'master' of github.com:benediktahrens/rezk_completion
update .gitignore
Merge branch 'master' of github.com:DanGrayson/rezk_completion
Merge branch 'master' of github.com:benediktahrens/rezk_completion
maintain compatibility with coq 8.4, patched
Merge pull request #6 from DanGrayson/master

compatibility with coq 8.4