coq - The formal proof system

Age	Commit message (Expand)	Author
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-24	New: (temporary) concrete syntax to specify the morphism signature:	sacerdot
2004-09-17	restructuration des printers: proofs passe avant parsing	barras
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-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-08-24	Calling setoid_rewrite on a term H whose type (eq x y) was not an application	sacerdot
2004-07-23	Major bug fixing and improvement of the setoid_{replace,rewrite} tactics:	sacerdot
2004-07-16	Nouvelle en-tête	herbelin
2004-03-31	Morphismes déclarés comme Lemma pas comme Definition	herbelin
2003-11-24	Prise en compte des defs syntaxiques dans is_global et global_reference qui p...	herbelin
2003-10-10	Affichage des buts par Pfedit pour utilisation par les tactiques (Setoid_repl...	herbelin
2003-10-07	Correction du bug 335 et Export/Require Export dans un module	coq
2003-09-12	Indépendance vis à vis de Declare	herbelin
2003-03-31	Ajout d'un message à FailTac	herbelin
2003-03-31	factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )	corbinea
2003-03-29	eq fusionne avec eqT et devient par défaut sur Type,	herbelin
2003-03-12	* empty log message *	barras
2003-01-22	Correction bug réecriture à la racine pour le sétoide Prop.	clrenard
2002-12-09	Ajout Simpl et Change sur des sous-termes	herbelin
2002-11-14	Réforme de l'interprétation des termes :	herbelin
2002-11-05	Intégration des modifs de la branche mowgli :	herbelin
2002-10-23	Ajout de la syntaxe "Theorem f [binders] : t", comme pour Definition et Local	herbelin
2002-10-01	bug de noms long pour eqT.	clrenard
2002-09-29	Que des niveaux d'univers frais dans le type des constantes globales	herbelin
2002-08-02	Modules dans COQ\!\!\!\!	coq
2002-05-29	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin
2002-05-14	Changement de eq en eqT comme equivalence de setoide par defaut.	clrenard
2002-05-02	Minor correction of get_lem_name	coq
2002-03-04	Nouveau Rewrite-in plus economique	barras