coq - The formal proof system

Age	Commit message (Expand)	Author
2008-04-01	Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaient	herbelin
2008-03-31	- Fix for rewriting under dependent products.	msozeau
2008-03-28	Improve error handling and messages for typeclasses.	msozeau
2008-03-27	Various fixes on typeclasses:	msozeau
2008-03-25	Interpret patterns for hypotheses types in match goal in type_scope (if not a	msozeau
2008-03-23	Fix a bug found by B. Grégoire when declaring morphisms in module	msozeau
2008-03-22	Compatibility fixes, backtrack on definitions of reflexive,	msozeau
2008-03-20	Add a flag to control rewriting under lambdas. Otherwise makes some	msozeau
2008-03-19	Do another pass on the typeclasses code. Correct globalization of class	msozeau
2008-03-18	Implementation of rewriting under lambdas. Tested on exists only.	msozeau
2008-03-18	Correct implementation of normalization of signatures using setoid	msozeau
2008-03-17	Add the possibility of specifying constants to unfold for typeclass	msozeau
2008-03-16	Using the "relation" constant made some unifications fail in the new	msozeau
2008-03-16	Reorganize Program and Classes theories. Requiring Setoid no longer sets	msozeau
2008-03-16	Minor fixes on setoid rewriting. Now uses definitions of [relation] and	msozeau
2008-03-10	Fix compilation problem and finish little cleanup.	msozeau
2008-03-09	Add a missing morphism declaration that turns morphisms on R ==> R' to	msozeau
2008-03-08	New implementation of Add Relation as a DefaultRelation instance	msozeau
2008-03-08	Fix bugs that were reopened due to the change of setoid	msozeau
2008-03-07	Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As part	msozeau
2008-03-06	typo in last commit (?)	letouzey
2008-03-06	Plug the new setoid implemtation in, leaving the original one commented	msozeau
2008-02-26	Proper implicit arguments handling for assumptions	msozeau
2008-02-14	Some bad emacs messup that was commited...	msozeau
2008-02-14	Backtrack changes on eauto, move specialized version of eauto in	msozeau
2008-02-13	Move class_setoid to class_tactics.	msozeau