coq - The formal proof system

Age	Commit message (Expand)	Author
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-06	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-05	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-04	maj	filliatr
2004-10-04	Added "as ..." parameter to Add Morphism.	sacerdot
2004-10-04	un paquet de corrections de bugs	letouzey
2004-10-03	maj	filliatr
2004-10-01	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-09-30	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	cutrewrite does not work with relations that are not Coq-like equalities.	sacerdot
2004-09-30	setoid_replace E1 with E2	sacerdot
2004-09-29	maj	filliatr
2004-09-29	* error messages improved	sacerdot
2004-09-29	Add Relation is now able to detect non well typed relation registrations.	sacerdot
2004-09-29	The Add Morphism command is now able to detect in advance:	sacerdot
2004-09-29	New syntax	sacerdot
2004-09-29	The Prod special case works only when the premise is of type Prop.	sacerdot
2004-09-29	1. major code clean-up for the Prod case	sacerdot
2004-09-29	impl is a reflexive relation (it used to be areflexive).	sacerdot
2004-09-29	impl relation and impl/and/or/not morphisms over impl declared.	sacerdot
2004-09-29	1) bug fixed: new goals where compared according to the relation arguments	sacerdot
2004-09-29	The list of possible solutions proposed by the tactic cannot contain any	sacerdot
2004-09-29	Test updated.	sacerdot
2004-09-29	Hugly temporary notation	sacerdot
2004-09-29	The quoting function is now 100% complete.	sacerdot
2004-09-28	maj	filliatr
2004-09-28	maj	filliatr
2004-09-28	The quoting function is now almost complete (in the sense that it can find	sacerdot