coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	New: (temporary) concrete syntax to specify the morphism signature:	sacerdot	2004-09-24
*	Simplifications concommitantes à la correction du bug #855	herbelin	2004-09-24
*	Correction bug report #855	herbelin	2004-09-24
*	restructuration des printers: proofs passe avant parsing	barras	2004-09-17
*	hiding the meta_map in evar_defs	barras	2004-09-15
*	put empty_env in hint clause (vo were becoming huge!)	barras	2004-09-15
*	evar tactic bugfix	corbinea	2004-09-14
*	* 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-13
*	inclusion de meta_map dans evar_defs	barras	2004-09-12
*	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-10
*	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-08
*	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-07
*	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-09-03
*	Calling setoid_rewrite on a term H whose type (eq x y) was not an application	sacerdot	2004-08-24
*	Protection contre un indice d'evar égal à 0	herbelin	2004-08-03
*	Protection erreur find_eq_data dans decompEqThen et uniformisation messages d...	herbelin	2004-07-30
*	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-23
*	Nouvelle en-tête	herbelin	2004-07-16
*	Abstraction vis a vis de dummy_loc	herbelin	2004-07-16
*	syntax compatibility fix	corbinea	2004-07-02
*	instantiate entry: constr -> lconstr	corbinea	2004-06-30
*	moved instantiate binding to extratactics	corbinea	2004-06-29
*	more evar stuff	corbinea	2004-06-28
*	Ajout de la coercion id dans context vers evaluable constant (bug #777)	herbelin	2004-06-28
*	effective evar refining	corbinea	2004-06-26
*	bug #787 de Roland	barras	2004-06-02
*	Clarify the distinction between quantified_hypothesis and declared_or_quantif...	herbelin	2004-06-02
*	Bug mauvais sigma	herbelin	2004-05-07
*	Terminologie plus intuitive: evaluable -> unfoldable	herbelin	2004-04-30
*	Morphismes déclarés comme Lemma pas comme Definition	herbelin	2004-03-31
*	Distinction entre declarations internes (p.ex. _subproof) et declarations uti...	herbelin	2004-03-30
*	Backtrack sur commit 1.20	herbelin	2004-03-18
*	Desactivation de la syntaxe v7 de Hint Rewrite en v8	herbelin	2004-03-17
*	Message d'erreur	herbelin	2004-03-17
*	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-15
*	Backtrack sur la réparation de Abstract qui casse autre chose; le problème ...	herbelin	2004-03-13
*	Retablissement de la correction bug d'inversion faite dans la version 1.116 e...	herbelin	2004-03-12