coq - The formal proof system

Age	Commit message (Expand)	Author
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
2004-07-16	Abstraction vis a vis de dummy_loc	herbelin
2004-07-02	syntax compatibility fix	corbinea
2004-06-30	instantiate entry: constr -> lconstr	corbinea
2004-06-29	moved instantiate binding to extratactics	corbinea
2004-06-28	more evar stuff	corbinea
2004-06-28	Ajout de la coercion id dans context vers evaluable constant (bug #777)	herbelin
2004-06-26	effective evar refining	corbinea
2004-06-02	bug #787 de Roland	barras
2004-06-02	Clarify the distinction between quantified_hypothesis and declared_or_quantif...	herbelin
2004-05-07	Bug mauvais sigma	herbelin
2004-04-30	Terminologie plus intuitive: evaluable -> unfoldable	herbelin
2004-03-31	Morphismes déclarés comme Lemma pas comme Definition	herbelin
2004-03-30	Distinction entre declarations internes (p.ex. _subproof) et declarations uti...	herbelin
2004-03-18	Backtrack sur commit 1.20	herbelin
2004-03-17	Desactivation de la syntaxe v7 de Hint Rewrite en v8	herbelin
2004-03-17	Message d'erreur	herbelin
2004-03-15	bug d'Inversion #529 (pb avec ordre d'evaluation)	barras
2004-03-15	Nouvelle reparation pour Abstract en presence de variables de contexte: on co...	herbelin
2004-03-13	Backtrack sur la réparation de Abstract qui casse autre chose; le problème ...	herbelin
2004-03-12	Retablissement de la correction bug d'inversion faite dans la version 1.116 e...	herbelin
2004-03-12	Ne pas ajouter le contexte de section dans Abstract, il est deja inclus (avec...	herbelin
2004-03-11	code obsolete	herbelin
2004-03-11	Suppression de la distinction entre elimination de Type vers Type ou pas (Fal...	herbelin
2004-03-10	Ajout tactiques stepl et stepr de Nimègue	herbelin
2004-03-10	Correction bug internalisation 'context'	herbelin
2004-03-09	bug de l'inversion (coq-bugs #529)	barras
2004-03-05	modif des fixpoints pour que si on donne une notation au produit, les pts fix...	barras
2004-03-02	Ajout d'une entrée hyp de type HypArgType pour parser et interpréter les no...	herbelin
2004-03-02	Ajout d'une entrée hyp de type HypArgType pour parser et interpréter les no...	herbelin