coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Providing a -type-in-type option for collapsing the universe hierarchy.	Hugo Herbelin	2014-09-13
*	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-09-12
*	- Fix has_undefined_evars not using its or_sorts argument anymore.	Matthieu Sozeau	2014-08-03
*	Add interface function to replace new_Type ()	Matthieu Sozeau	2014-07-14
*	Cleanup treatment of template universe polymorphism (thanks to E. Tassi	Matthieu Sozeau	2014-06-20
*	Fixing "clear" in internal_cut_replace: forbid dependencies in the	Hugo Herbelin	2014-06-13
*	Reuse universe level substitutions for template polymorphism, fixing performance	Matthieu Sozeau	2014-05-09
*	- 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-05-06
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Removing useless meta-related functions.	Pierre-Marie Pédrot	2013-12-03
*	A newly introduced variable inside a named context is no longer α-renamed.	aspiwack	2013-11-02
*	Abstracting evar filter away. The API is not perfect, but better than nothing.	ppedrot	2013-10-27
*	Removing useless evar-related stuff.	ppedrot	2013-09-25
*	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-18
*	Partly replacing list-based access functions in Evd. This is still	ppedrot	2013-09-03
*	Replacing lists by sets in clear tactic.	ppedrot	2013-08-25
*	Mini documentation (evar_absorb_arguments).	herbelin	2013-05-14
*	Merging Context and Sign.	ppedrot	2013-04-29
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	Continuation of r16346 on filtering local definitions. Refined	herbelin	2013-03-30
*	Allowing different types of, not to be mixed, generic Stores through	ppedrot	2013-03-12
*	Splitted Evarutil in two files	ppedrot	2013-02-10
*	Moved code from Pretype_error to Evarutil	ppedrot	2013-02-10
*	Modulification of name	ppedrot	2012-12-18
*	Modulification of identifier	ppedrot	2012-12-14
*	Moved Intset and Intmap to Int namespace.	ppedrot	2012-12-14
*	Updating headers.	herbelin	2012-08-08
*	Another correction to the dependent existential variable printing	aspiwack	2012-07-10
*	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot	2012-06-22
*	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-05-29
*	Unification: Added a heuristic to solve problems of the form	herbelin	2012-03-26
*	Generalized the use of evar candidates in type inference unification:	herbelin	2012-03-20
*	Remove support for "abstract typing constraints" that requires unicity of sol...	msozeau	2012-03-14
*	Noise for nothing	pboutill	2012-03-02
*	Introducing a notion of evar candidates to be used when an evar is	herbelin	2011-12-16
*	Discarding let-ins from the instances of the evars in the	herbelin	2011-12-04
*	Adds a pair of function in Evar_util to gather dependent evars in an	aspiwack	2011-11-23
*	Fixing incorrect change to pattern-unification over Meta's introduced	herbelin	2011-11-06
*	Continuing r1492 (useless changes were inadvertantly committed)	herbelin	2011-10-25
*	New strategy to infer return predicate of match construct when	herbelin	2011-10-25
*	More robust and uniform treatment of aliases in evarutil.ml	herbelin	2011-10-10
*	Applied the trick of Chung-Kil Hur to solve second-order matching	herbelin	2011-10-10
*	Passed conv_algo to evar_define and move call to solve_refl to	herbelin	2011-10-10
*	- Fix restrict_hyps to not allow filtering on a variable required to typechec...	msozeau	2011-06-07
*	Tentative to make unification check types at every instanciation of an	msozeau	2011-03-11