coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Compatibilité ocamlweb pour cible doc	herbelin	2005-01-21
*	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
*	The "lem" field of a morphism used to be the compatibility proof, but it	sacerdot	2004-10-18
*	New commands	sacerdot	2004-10-07
*	* New syntactic sugar: Add Relation ... transitivity proved by ...	sacerdot	2004-10-06
*	added transitivity	barras	2004-10-06
*	add_setoid has a new parameter used to synthesize the morphism 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
*	cutrewrite does not work with relations that are not Coq-like equalities.	sacerdot	2004-09-30
*	New syntax	sacerdot	2004-09-29
*	Hugly temporary notation	sacerdot	2004-09-29
*	New: (temporary) concrete syntax to specify the morphism signature:	sacerdot	2004-09-24
*	The ML part of the tactic now knows about covariant and contravariant morphism	sacerdot	2004-09-13
*	add_new_morphism has now a new argument that is the signature	sacerdot	2004-09-10
*	New reflexive implementation of setoid_rewrite. The new implementation	sacerdot	2004-09-03
*	Major bug fixing and improvement of the setoid_{replace,rewrite} tactics:	sacerdot	2004-07-23
*	Nouvelle en-tête	herbelin	2004-07-16
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin	2002-05-29
*	Ajout du .ml pour la tactique Setoid_replace	clrenard	2001-07-10