coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	- Parameterize unification by two sets of transparent_state, one for open	msozeau	2008-04-21
*	Document CHANGES in setoid rewrite, move DefaultRelation to	msozeau	2008-04-15
*	- Add "Global" modifier for instances inside sections with the usual	msozeau	2008-04-15
*	Update doc and remove another overloading of equiv_*.	msozeau	2008-04-14
*	Renamings to avoid clashes with definitions in Relation_Definitions, now	msozeau	2008-04-14
*	- A little cleanup in Classes/*. Separate standard morphisms on	msozeau	2008-04-08
*	Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaient	herbelin	2008-04-01
*	Various fixes on typeclasses:	msozeau	2008-03-27
*	Interpret patterns for hypotheses types in match goal in type_scope (if not a	msozeau	2008-03-25
*	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
*	Correct implementation of normalization of signatures using setoid	msozeau	2008-03-18
*	Removed unneeded tactics from RelationClasses. Use	msozeau	2008-03-16
*	Reorganize Program and Classes theories. Requiring Setoid no longer sets	msozeau	2008-03-16
*	Fix bugs that were reopened due to the change of setoid	msozeau	2008-03-08
*	Plug the new setoid implemtation in, leaving the original one commented	msozeau	2008-03-06
*	Syntax changes in typeclasses, remove "?" for usual implicit arguments	msozeau	2008-03-06
*	Backtrack changes on eauto, move specialized version of eauto in	msozeau	2008-02-14