coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Wish of Maggesi implemented: the type of the morphism compatibility lemma	sacerdot	2004-10-15
*	maj	filliatr	2004-10-14
*	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
*	maj	filliatr	2004-10-13
*	Compatibilité de Hint Rewrite avec Write State	herbelin	2004-10-13
*	maj	filliatr	2004-10-12
*	Desactivation de la construction 'lazy match' en attendant une autre solution	herbelin	2004-10-12
*	Mise en conformité de la syntaxe de Theorem/Lemma avec la doc: les lieurs so...	herbelin	2004-10-12
*	Réinstallation des lieurs avant l'énoncé de Theorem/Lemma (non documenté ...	herbelin	2004-10-12
*	Prise en compte dans cut_ident des idents de la form _23 qui sont officiellem...	herbelin	2004-10-12
*	option -no-hash-consing pour supprimmer le hash-consing	filliatr	2004-10-12
*	maj	filliatr	2004-10-11
*	'match term' now evaluates by default. Added 'lazy' keyword to delay the eval...	herbelin	2004-10-11
*	Suppression IsConjecture redondant avec Conjectural	herbelin	2004-10-11
*	maj	filliatr	2004-10-10
*	maj	filliatr	2004-10-08
*	maj	filliatr	2004-10-07
*	setoid_symmetry in ... implemented.	sacerdot	2004-10-07
*	New commands	sacerdot	2004-10-07
*	iff and impl are now declared as transitive relations.	sacerdot	2004-10-07
*	Now Print Setoids prints also the transitivity justification of transitive	sacerdot	2004-10-07
*	maj	filliatr	2004-10-06
*	* New syntactic sugar: Add Relation ... transitivity proved by ...	sacerdot	2004-10-06
*	added transitivity	barras	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
*	maj	filliatr	2004-10-05
*	maj	filliatr	2004-10-05
*	* 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
*	maj	filliatr	2004-10-04
*	Added "as ..." parameter to Add Morphism.	sacerdot	2004-10-04
*	un paquet de corrections de bugs	letouzey	2004-10-04
*	maj	filliatr	2004-10-03
*	maj	filliatr	2004-10-01
*	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
*	add_setoid has a new parameter used to synthesize the morphism name.	sacerdot	2004-10-01
*	Added "as ..." parameters to "Add Setoid"	sacerdot	2004-10-01
*	The "Add Setoid" command now has a new argument "as name" that is used	sacerdot	2004-10-01
*	maj	filliatr	2004-09-30
*	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