coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	mimick: unify types before making assignation	barras	2004-09-06
*	optimized the non-backtracking case	barras	2004-09-06
*	bad env in mimick code	barras	2004-09-06
*	reparation des Extract Constant avec Haskell	letouzey	2004-09-06
*	maj	filliatr	2004-09-05
*	Correction commit precedent	herbelin	2004-09-04
*	maj	filliatr	2004-09-03
*	maj	filliatr	2004-09-03
*	deplacement de clenv vers pretyping	barras	2004-09-03
*	premiere reorganisation de l\'unification	barras	2004-09-03
*	Bug List.hd vs list_last	herbelin	2004-09-03
*	MAJ options coqtop et coqc	herbelin	2004-09-03
*	* New test (for setoid_replace in the general case)	sacerdot	2004-09-03
*	* setoid_test.v removed and added again in new syntax	sacerdot	2004-09-03
*	Ported to the new implementation of setoid_*.	sacerdot	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
*	The old implementation of (setoid_replace c1 with c2) used to replace	sacerdot	2004-09-03