coq - The formal proof system

Age	Commit message (Expand)	Author
2009-01-18	Getting rid of the previous implementation of setoid_rewrite which was	msozeau
2008-09-03	Fix bug #1935, reworking the reflexivity, symmetry... tactics to use	msozeau
2008-06-10	- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)	herbelin
2008-04-12	Adding 'at' to rewrite, as it is already implemented in setoid_rewrite.	msozeau
2008-02-07	Mise en place d'une toute petite amélioration de l'unification de	herbelin
2006-08-22	+ Changing "in <hyp>" to "in <clause>" (no at, no InValue and no	jforest
2006-05-02	Changement de comportement de rewrite: face a une egalité setoid, on	letouzey
2005-01-21	Compatibilité ocamlweb pour cible doc	herbelin
2004-10-19	Proof term size reduction (again).	sacerdot
2004-10-18	* Code simplification and clean-up. In particular there is no more code	sacerdot
2004-10-18	The "lem" field of a morphism used to be the compatibility proof, but it	sacerdot
2004-10-07	New commands	sacerdot
2004-10-06	* New syntactic sugar: Add Relation ... transitivity proved by ...	sacerdot
2004-10-06	added transitivity	barras
2004-10-01	add_setoid has a new parameter used to synthesize the morphism name.	sacerdot
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-29	New syntax	sacerdot
2004-09-29	Hugly temporary notation	sacerdot
2004-09-24	New: (temporary) concrete syntax to specify the morphism signature:	sacerdot
2004-09-13	The ML part of the tactic now knows about covariant and contravariant morphism	sacerdot
2004-09-10	add_new_morphism has now a new argument that is the signature	sacerdot
2004-09-03	New reflexive implementation of setoid_rewrite. The new implementation	sacerdot
2004-07-23	Major bug fixing and improvement of the setoid_{replace,rewrite} tactics:	sacerdot
2004-07-16	Nouvelle en-tête	herbelin
2002-11-14	Réforme de l'interprétation des termes :	herbelin
2002-05-29	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin
2001-07-10	Ajout du .ml pour la tactique Setoid_replace	clrenard