coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	maj	filliatr	2004-09-24
*	maj	filliatr	2004-09-24
*	New: (temporary) concrete syntax to specify the morphism signature:	sacerdot	2004-09-24
*	Ajout bug #255	herbelin	2004-09-24
*	Simplifications concommitantes à la correction du bug #855	herbelin	2004-09-24
*	Correction bug report #855	herbelin	2004-09-24
*	maj	filliatr	2004-09-23
*	error if binder was already defined	barras	2004-09-23
*	maj	filliatr	2004-09-22
*	maj	filliatr	2004-09-22
*	link order again	barras	2004-09-22
*	maj	filliatr	2004-09-21
*	maj	filliatr	2004-09-20
*	pbs with link order and deps	barras	2004-09-20
*	maj	filliatr	2004-09-19
*	maj	filliatr	2004-09-17
*	restructuration des printers: proofs passe avant parsing	barras	2004-09-17
*	repaired deps	barras	2004-09-17
*	maj	filliatr	2004-09-16
*	maj	filliatr	2004-09-15
*	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
*	maj	filliatr	2004-09-14
*	maj	filliatr	2004-09-14
*	evar tactic bugfix	corbinea	2004-09-14
*	maj	filliatr	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-13
*	maj	filliatr	2004-09-12
*	maj	filliatr	2004-09-12
*	inclusion de meta_map dans evar_defs	barras	2004-09-12
*	maj	filliatr	2004-09-10
*	maj	filliatr	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-10
*	When refining a given term, the primitive refiner used to accepts some casts,	sacerdot	2004-09-10
*	maj	filliatr	2004-09-09
*	Crédit	herbelin	2004-09-09
*	Ajout de or-pattern pour le match-with v8	herbelin	2004-09-09
*	maj	filliatr	2004-09-08
*	maj	filliatr	2004-09-08
*	unification encore...	barras	2004-09-08
*	* cleaning/renaming in Setoids.v	sacerdot	2004-09-08
*	* cleaning/renaming	sacerdot	2004-09-08
*	The innersort is now computed as the more precise sort between the	sacerdot	2004-09-08
*	The code used to compare the synthesized and the expected type (if available)	sacerdot	2004-09-08
*	The Coq part of the reflexive part can now deal with irreflexive relations too.	sacerdot	2004-09-08