coq - The formal proof system

Age	Commit message (Expand)	Author
2009-11-11	Promote evar_defs to evar_map (in Evd)	glondu
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-07-08	Reactivation of pattern unification of evars in apply unification, in	herbelin
2009-06-30	Add new variants of [rewrite] and [autorewrite] which differ in the	msozeau
2009-05-18	Minor unification changes:	msozeau
2008-04-27	- Backtrack sur option with_types suite à confusion sur l'utilisation	herbelin
2008-04-26	- Backtrack sur extension de syntaxe pour pose qui rentre en conflit avec	herbelin
2008-04-23	Prise en compte des coercions dans les clauses "with" même si le type	herbelin
2008-04-21	- Parameterize unification by two sets of transparent_state, one for open	msozeau
2008-04-17	Bug squashing day !	msozeau
2008-04-01	Ajout "simple apply" et "simple eapply" pour apply sans unfold	herbelin
2008-03-16	Using the "relation" constant made some unifications fail in the new	msozeau
2008-02-13	Essai de prise en compte de delta dans unify_0 (même sur termes non clos).	herbelin
2008-02-07	Mise en place d'une toute petite amélioration de l'unification de	herbelin
2007-10-03	Ajout de eelim, ecase, edestruct et einduction (expérimental).	herbelin
2007-05-28	Contrôle de la compatibilité de apply via une information dans les	herbelin
2004-09-27	?(mod_delta=true) parameter added to each unification function.	sacerdot
2004-09-17	restructuration des printers: proofs passe avant parsing	barras
2004-09-15	hiding the meta_map in evar_defs	barras
2004-09-12	inclusion de meta_map dans evar_defs	barras
2004-09-08	unification encore...	barras
2004-09-07	deuxieme vague de modifs: evar_defs fonctionnel	barras
2004-09-03	deplacement de clenv vers pretyping	barras
2004-09-03	premiere reorganisation de l\'unification	barras