coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Fix test-suite files, change conflicting notation "->rel" and the others	msozeau	2008-03-29
*	Improve error handling and messages for typeclasses.	msozeau	2008-03-28
*	Various fixes on typeclasses:	msozeau	2008-03-27
*	Fix a bug found by B. Grégoire when declaring morphisms in module	msozeau	2008-03-23
*	Compatibility fixes, backtrack on definitions of reflexive,	msozeau	2008-03-22
*	Do another pass on the typeclasses code. Correct globalization of class	msozeau	2008-03-19
*	Implementation of rewriting under lambdas. Tested on exists only.	msozeau	2008-03-18
*	Correct implementation of normalization of signatures using setoid	msozeau	2008-03-18
*	Add the possibility of specifying constants to unfold for typeclass	msozeau	2008-03-17
*	Removed unneeded tactics from RelationClasses. Use	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-16
*	Add a missing morphism declaration that turns morphisms on R ==> R' to	msozeau	2008-03-09
*	Coquille vraisemblablement introduite par la révision 10628	notin	2008-03-06
*	Syntax changes in typeclasses, remove "?" for usual implicit arguments	msozeau	2008-03-06
*	Fix compilation problem (hopefully).	msozeau	2008-02-28
*	Proper implicit arguments handling for assumptions	msozeau	2008-02-26
*	Backtrack changes on eauto, move specialized version of eauto in	msozeau	2008-02-14
*	Fix the clrewrite tactic, change Relations.v to work on relations in Prop	msozeau	2008-02-09
*	New algorithm to resolve morphisms, after discussion with Nicolas	msozeau	2008-02-06