coq - The formal proof system

Age	Commit message (Expand)	Author
2016-03-06	Moving Eauto to a simple ML file.	Pierre-Marie Pédrot
2002-05-29	Fichiers tactics/.ml4 remplacent les tactics/.v	herbelin
2001-12-13	compat ocaml 3.03	filliatr
2001-11-29	nouvel algo de conversion plus uniforme	barras
2001-11-19	Diverses petites simplications de la machine de preuves.	clrenard
2001-11-05	GROS COMMIT:	barras
2001-06-29	Autoriser Apply avec un but sous forme d'implication ou de quantification	barras
2001-05-23	amelioration des messages d'erreurs vis a vis des evars	barras
2001-03-28	amelioration de la structure des univers	barras
2001-03-15	entetes	filliatr
2001-03-08	changement comparaison etats	filliatr
2001-03-06	Modification de e_give_exact pour eviter d'echouer sur l'unification	mohring
2001-03-06	eta-expansion	mohring
2001-03-06	EAutod (debug)	filliatr
2001-03-05	module Explore générique et réécriture EAuto avec ce module; occur check ...	filliatr
2001-02-28	modif	mohring
2001-02-27	EAuto mixte (largeur puis profondeur)	mohring
2001-02-26	Eauto version en largeur	mohring
2000-11-23	Reparation IsMutConstruct + Transparent	mohring
2000-11-02	suppression des (* open Generic *)	filliatr
2000-10-13	Suppression du test de convertibilite inutile pour la plupart des exact; 2 ve...	herbelin
2000-10-11	Prise en compte de l'env local dans make_apply_entry	herbelin
2000-09-14	Abstraction de constr	herbelin
2000-09-12	Modification mkAppL; abstraction via kind_of_term; changement dans Reduction	herbelin
2000-09-10	Correction pour make doc	herbelin
2000-09-10	Ajout d'un LetIn primitif.	herbelin
2000-07-24	Passage à des contextes de vars et de rels pouvant contenir des déclarations	herbelin
2000-06-28	Modifs de presentation.	delahaye
2000-06-21	portage EAuto et Ring	filliatr