coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Restauration type casted_open_constr pour tactique refine car l'unification n...	herbelin	2004-12-09
*	Uniformisation du nom d'entrée openconstr en le nom du type open_constr	herbelin	2004-12-06
*	Déplacement de la coercion vis à vis du but au niveau de Refine	herbelin	2004-12-06
*	Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des tacti...	herbelin	2004-12-06
*	Mise en conformité de Derive Inversion et Derive Dependent Inversion avec la...	herbelin	2004-11-15
*	Ajout 'dependent rewrite in'	herbelin	2004-10-28
*	Restructuration fonctions de réécriture depuis égalité dépendante	herbelin	2004-10-27
*	New commands	sacerdot	2004-10-07
*	* New syntactic sugar: Add Relation ... transitivity proved by ...	sacerdot	2004-10-06
*	The "Add Setoid" command now has a new argument "as name" that is used	sacerdot	2004-10-01
*	New tactic	sacerdot	2004-09-30
*	New tactic [setoid_]rewrite ... in ... [generate side conditions ...].	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
*	Add_new_morphism has now a new optional argument that is the signature of	sacerdot	2004-09-10
*	New command "Add Relation ..." (for the new implementation of setoid_*).	sacerdot	2004-09-03
*	Setoid_replace.setoid_replace last argument (that was supposed to be always	sacerdot	2004-07-23
*	Nouvelle en-tête	herbelin	2004-07-16
*	syntax compatibility fix	corbinea	2004-07-02
*	moved instantiate binding to extratactics	corbinea	2004-06-29
*	more evar stuff	corbinea	2004-06-28
*	Backtrack sur commit 1.20	herbelin	2004-03-18
*	Desactivation de la syntaxe v7 de Hint Rewrite en v8	herbelin	2004-03-17
*	Ajout tactiques stepl et stepr de Nimègue	herbelin	2004-03-10
*	Ajout d'une entrée hyp de type HypArgType pour parser et interpréter les no...	herbelin	2004-03-02
*	Ajout 'replace in'	herbelin	2004-03-01
*	Idtac peut prendre un argument à afficher	narboux	2003-11-12
*	petits changements de syntaxe	barras	2003-11-12
*	reorganisation des niveaux (ex: = est a 70)	barras	2003-10-22
*	Extension de l'utilisation de contradiction	herbelin	2003-10-19
*	Cablage en dur de inversion	herbelin	2003-10-10
*	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin	2003-04-07
*	notations <>, Assumption avec existentiel, replace term	mohring	2003-03-28
*	* empty log message *	barras	2003-03-12
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	Subst (tout court)	filliatr	2002-09-16
*	tactique Subst x1 ... xn	filliatr	2002-09-11
*	tactique Subst	filliatr	2002-07-17
*	Repercussion de la possibilit de mettre des hyps quantifiees dans Simplify_eq...	herbelin	2002-06-05
*	Rpercussion de la possibilit de mettre des hyps quantifies dans Simplify_eq e...	herbelin	2002-06-05
*	Ajout d'extensions de syntaxe ARGUMENT EXTEND et VERNAC ARGUMENT EXTEND; rpar...	herbelin	2002-06-05
*	Fichiers tactics/.ml4 remplacent les tactics/.v	herbelin	2002-05-29