coq - The formal proof system

Age	Commit message (Expand)	Author
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2014-04-23	Removing dead code, thanks to new OCaml warnings and a bit of scripting.	Pierre-Marie Pédrot
2013-09-18	At least made the evar type opaque! There are still 5 remaining unsafe	ppedrot
2013-05-30	export Unification.abstract_list_all_with_dependencies	pboutill
2012-12-18	Fixed a little inefficiency of "set/destruct" over a pattern. Now	herbelin
2012-10-04	Improving error message when abtraction over goal (abstract_list_all	herbelin
2012-08-08	Updating headers.	herbelin
2011-12-17	Added a flag to control the use of typing when instantiating applied	herbelin
2011-10-11	Moved to a more standard order of arguments (i.e. env followed by evar_map)	herbelin
2011-08-04	Fix unification: detect invalid evar instantiations due to scoping earlier.	msozeau
2011-06-18	Generalizing flag use_evars_pattern_unification into a flag	herbelin
2011-06-13	Added a flag to restrict conversion in tactic unification on the	herbelin
2011-06-12	Added a new flag for freezing evars in tactic unification. Used this	herbelin
2011-06-10	Moved allow_K to a unification flag	herbelin
2011-04-18	Add a flag to control betaiota reduction during unification to maintain backw...	msozeau
2011-03-13	- Add modulo_delta_types flag for unification to allow full	msozeau
2010-09-20	Added eta-expansion in kernel, type inference and tactic unification,	herbelin
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-06-22	New script dev/tools/change-header to automatically update Coq files headers.	herbelin
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2010-04-29	Move from ocamlweb to ocamdoc to generate mli documentation	pboutill
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