coq - The formal proof system

Age	Commit message (Expand)	Author
2014-12-11	Tentatively more informative report of failure when inferring	Hugo Herbelin
2014-12-04	Occur-check in refine.	Arnaud Spiwack
2014-10-16	Move the handling of the principal evar from refine to evd.	Arnaud Spiwack
2014-10-04	A few Global.env removed.	Hugo Herbelin
2014-09-30	Add syntax for naming new goals in refine: writing ?[id] instead of _	Hugo Herbelin
2014-09-29	Merging some functions from evarutil.ml/evd.ml.	Hugo Herbelin
2014-09-13	Providing a -type-in-type option for collapsing the universe hierarchy.	Hugo Herbelin
2014-09-12	Uniformisation of the order of arguments env and sigma.	Hugo Herbelin
2014-09-12	Referring to evars by names. Added a parser for evars (but parsing of	Hugo Herbelin
2014-08-03	- Fix has_undefined_evars not using its or_sorts argument anymore.	Matthieu Sozeau
2014-07-14	Add interface function to replace new_Type ()	Matthieu Sozeau
2014-06-20	Cleanup treatment of template universe polymorphism (thanks to E. Tassi	Matthieu Sozeau
2014-06-13	Fixing "clear" in internal_cut_replace: forbid dependencies in the	Hugo Herbelin
2014-05-09	Reuse universe level substitutions for template polymorphism, fixing performance	Matthieu Sozeau
2014-05-06	- Fix treatment of global universe constraints which should be passed along	Matthieu Sozeau
2014-05-06	Try a new way of handling template universe levels	Matthieu Sozeau
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2014-03-05	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey
2013-12-03	Removing useless meta-related functions.	Pierre-Marie Pédrot
2013-11-02	A newly introduced variable inside a named context is no longer α-renamed.	aspiwack
2013-10-27	Abstracting evar filter away. The API is not perfect, but better than nothing.	ppedrot
2013-09-25	Removing useless evar-related stuff.	ppedrot
2013-09-18	At least made the evar type opaque! There are still 5 remaining unsafe	ppedrot
2013-09-18	Removing almost all new_untyped_evar, and a bunch of Evd.add.	ppedrot
2013-09-03	Partly replacing list-based access functions in Evd. This is still	ppedrot
2013-08-25	Replacing lists by sets in clear tactic.	ppedrot
2013-05-14	Mini documentation (evar_absorb_arguments).	herbelin
2013-04-29	Merging Context and Sign.	ppedrot
2013-04-29	Splitting Term into five unrelated interfaces:	ppedrot
2013-03-30	Continuation of r16346 on filtering local definitions. Refined	herbelin
2013-03-12	Allowing different types of, not to be mixed, generic Stores through	ppedrot
2013-02-10	Splitted Evarutil in two files	ppedrot
2013-02-10	Moved code from Pretype_error to Evarutil	ppedrot
2012-12-18	Modulification of name	ppedrot
2012-12-14	Modulification of identifier	ppedrot
2012-12-14	Moved Intset and Intmap to Int namespace.	ppedrot
2012-08-08	Updating headers.	herbelin
2012-07-10	Another correction to the dependent existential variable printing	aspiwack
2012-06-22	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot
2012-05-29	remove many excessive open Util & Errors in mli's	letouzey
2012-05-29	Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd	letouzey
2012-03-26	Unification: Added a heuristic to solve problems of the form	herbelin
2012-03-20	Generalized the use of evar candidates in type inference unification:	herbelin
2012-03-14	Remove support for "abstract typing constraints" that requires unicity of sol...	msozeau
2012-03-02	Noise for nothing	pboutill
2011-12-16	Introducing a notion of evar candidates to be used when an evar is	herbelin
2011-12-04	Discarding let-ins from the instances of the evars in the	herbelin
2011-11-23	Adds a pair of function in Evar_util to gather dependent evars in an	aspiwack
2011-11-06	Fixing incorrect change to pattern-unification over Meta's introduced	herbelin
2011-10-25	Continuing r1492 (useless changes were inadvertantly committed)	herbelin