coq - The formal proof system

Age	Commit message (Expand)	Author
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	* 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	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	Hugly temporary notation	sacerdot
2004-09-29	The quoting function is now 100% complete.	sacerdot
2004-09-28	The quoting function is now almost complete (in the sense that it can find	sacerdot
2004-09-27	The quoting function of the reflexive tactic is now sound: all the terms	sacerdot
2004-09-27	corrected bug when lhs is matched w.r.t delta	barras
2004-09-25	- Prise en compte de Fail n (n>0) dans plusieurs cas qui avaient	herbelin
2004-09-24	New: (temporary) concrete syntax to specify the morphism signature:	sacerdot
2004-09-24	Simplifications concommitantes à la correction du bug #855	herbelin
2004-09-24	Correction bug report #855	herbelin
2004-09-17	restructuration des printers: proofs passe avant parsing	barras
2004-09-15	hiding the meta_map in evar_defs	barras
2004-09-15	put empty_env in hint clause (vo were becoming huge!)	barras
2004-09-14	evar tactic bugfix	corbinea
2004-09-13	* The ML tactic is now also aware of rewriting directions.	sacerdot
2004-09-13	The ML part of the tactic now knows about covariant and contravariant morphism	sacerdot
2004-09-12	inclusion de meta_map dans evar_defs	barras
2004-09-10	simplification de clenv	barras
2004-09-10	Dead code removed.	sacerdot
2004-09-10	1. add_new_morphism now has a new optional argument that is the signature	sacerdot
2004-09-10	add_new_morphism has now a new argument that is the signature	sacerdot
2004-09-10	Add_new_morphism has now a new optional argument that is the signature of	sacerdot
2004-09-08	unification encore...	barras
2004-09-08	* cleaning/renaming in Setoids.v	sacerdot
2004-09-08	The Coq part of the reflexive part can now deal with irreflexive relations too.	sacerdot
2004-09-07	deuxieme vague de modifs: evar_defs fonctionnel	barras
2004-09-07	* The Coq part of the reflexive tactic setoid_rewrite is generalized to	sacerdot
2004-09-03	premiere reorganisation de l\'unification	barras
2004-09-03	New reflexive implementation of setoid_rewrite. The new implementation	sacerdot
2004-09-03	New command "Add Relation ..." (for the new implementation of setoid_*).	sacerdot
2004-08-24	Calling setoid_rewrite on a term H whose type (eq x y) was not an application	sacerdot
2004-08-03	Protection contre un indice d'evar égal à 0	herbelin
2004-07-30	Protection erreur find_eq_data dans decompEqThen et uniformisation messages d...	herbelin
2004-07-23	Major bug fixing and improvement of the setoid_{replace,rewrite} tactics:	sacerdot
2004-07-23	Since setoid_{replace,rewrite} now uses replace there is a circularity	sacerdot
2004-07-23	Setoid_replace.setoid_replace last argument (that was supposed to be always	sacerdot
2004-07-16	Nouvelle en-tête	herbelin