coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	The Coq part of the reflexive tactic is now able to handle also	sacerdot	2004-09-08
*	petit bug avec les effets de bords	barras	2004-09-08
*	Meilleur anglais (cf #841)	herbelin	2004-09-08
*	Un bug de simpl de 1995 + nettoyage (les args de list_fold_left_i etaient inc...	herbelin	2004-09-08
*	maj	filliatr	2004-09-07
*	maj	filliatr	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-07
*	maj	filliatr	2004-09-06
*	maj	filliatr	2004-09-06