coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Réorganisation de la structure interne des types de déclarations (decl_kinds)	herbelin	2006-01-28
*	Restructuration et simplification des fonctions d'affichage, de détypage	herbelin	2006-01-11
*	Renommage des Ppnew en Pp (et déplacement dans parsing); renommage des G_*...	herbelin	2005-12-26
*	Changement des named_context	gregoire	2005-12-02
*	Nettoyage suite à la détection par défaut des variables inutilisées par o...	herbelin	2005-11-08
*	Sur le conseil de X.Leroy: x=[\|\|] devient Array.length x=0	letouzey	2005-08-19
*	New commit to allow definitions of morphisms on relations whose carrier is	sacerdot	2005-05-24
*	Setoid_replace: improved error message when trying to replace a term in a	sacerdot	2005-05-19
*	A wish by Bas Spitters granted: a little more of unification up to	sacerdot	2005-05-19
*	Bug (reported by Lionel Mamane) fixed: the test for non-occurrence of the	sacerdot	2005-01-18
*	Bug fixed (reported by Roland): the setoire_rewrite in tactic did not work	sacerdot	2005-01-17
*	Names.substitution (and related functions) and Term.subst_mps moved to	sacerdot	2004-11-16
*	Changement dans les boxed values .	gregoire	2004-11-12
*	Factorisation cut_replacing	herbelin	2004-10-27
*	Word "setoid" banned from the error messages. "relation" used instead.	sacerdot	2004-10-25
*	Missing check implemented (closes a bug from Bas Spitters).	sacerdot	2004-10-25
*	The morphism lemma type was simplified only in modules and not in module	sacerdot	2004-10-21
*	Error message improved.	sacerdot	2004-10-21
*	COMMITED BYTECODE COMPILER	barras	2004-10-20
*	The bug already closed in revision 1.90 was reintroduced again.	sacerdot	2004-10-20
*	Proof term size reduction (again).	sacerdot	2004-10-19
*	* Code simplification and clean-up. In particular there is no more code	sacerdot	2004-10-18
*	Code simplification and clean-up.	sacerdot	2004-10-18
*	The lem field was not computed properly for morphisms whose argument was	sacerdot	2004-10-18
*	The "lem" field of a morphism used to be the compatibility proof, but it	sacerdot	2004-10-18
*	Bug fixed: relations quantified more than once where abstracted in the wrong	sacerdot	2004-10-18
*	More informative error message when the tactic tries to generate a new	sacerdot	2004-10-18
*	zeta flag added to reduce LetIns in a morphism type. Morphisms with local	sacerdot	2004-10-18
*	Wrong comment committed. The tactic behaves correctly only when the	sacerdot	2004-10-15
*	Wish of Maggesi implemented: the type of the morphism compatibility lemma	sacerdot	2004-10-15
*	Bug fixed (reported by Maggesi): sometimes when the tactic had to generate new	sacerdot	2004-10-14
*	Code clean-up.	sacerdot	2004-10-14
*	reflexivity, symmetry, symmetry ... in e transitivity now fall-back	sacerdot	2004-10-14
*	setoid_symmetry in ... implemented.	sacerdot	2004-10-07
*	New commands	sacerdot	2004-10-07
*	Now Print Setoids prints also the transitivity justification of transitive	sacerdot	2004-10-07
*	* New syntactic sugar: Add Relation ... transitivity proved by ...	sacerdot	2004-10-06
*	added transitivity	barras	2004-10-06
*	Add Setoid now accepts also quantified setoids.	sacerdot	2004-10-06
*	* code clean up	sacerdot	2004-10-06
*	Th unification procedure has been made a bit more complete by recording the	sacerdot	2004-10-06
*	Leibniz equality is now a quantified relation.	sacerdot	2004-10-06
*	* code simplification	sacerdot	2004-10-05
*	* [ bug fixed ]: when a subterm (c x1 ... xn) it is checked whether	sacerdot	2004-10-05
*	* Bug fix: in case of non dependent implications the second argument was	sacerdot	2004-10-05
*	eq_constr replaced with a conversion test where possible.	sacerdot	2004-10-01
*	1. added new parameter "as ..." to Add Setoid. Used to synthesize the name	sacerdot	2004-10-01
*	New tactic	sacerdot	2004-09-30
*	New tactic [setoid_]rewrite ... in ... [generate side conditions ...].	sacerdot	2004-09-30
*	Proof term size optimization: setoid_rewrite H where H is an application of	sacerdot	2004-09-30