coq - The formal proof system

Age	Commit message (Expand)	Author
2004-09-25	- Prise en compte de Fail n (n>0) dans plusieurs cas qui avaient	herbelin
2004-09-24	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-23	maj	filliatr
2004-09-23	error if binder was already defined	barras
2004-09-22	maj	filliatr
2004-09-22	maj	filliatr
2004-09-22	link order again	barras
2004-09-21	maj	filliatr
2004-09-20	maj	filliatr
2004-09-20	pbs with link order and deps	barras
2004-09-19	maj	filliatr
2004-09-17	maj	filliatr
2004-09-17	restructuration des printers: proofs passe avant parsing	barras
2004-09-17	repaired deps	barras
2004-09-16	maj	filliatr
2004-09-15	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-14	maj	filliatr
2004-09-14	maj	filliatr
2004-09-14	evar tactic bugfix	corbinea
2004-09-13	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-12	maj	filliatr
2004-09-12	maj	filliatr
2004-09-12	inclusion de meta_map dans evar_defs	barras
2004-09-10	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-09	maj	filliatr
2004-09-09	Crédit	herbelin
2004-09-09	Ajout de or-pattern pour le match-with v8	herbelin
2004-09-08	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