coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Update copyright headers.	Maxime Dénès	2016-01-20
*	Tactical `progress` compares term up to potentially equalisable universes.	Arnaud Spiwack	2015-04-22
*	STM: proof state also includes meta counters	Enrico Tassi	2015-02-25
*	[Proofview.tclPROGRESS]: do not consider that trivial goal instantiation is p...	Arnaud Spiwack	2015-02-24
*	Update headers.	Maxime Dénès	2015-01-12
*	Tentatively more informative report of failure when inferring	Hugo Herbelin	2014-12-11
*	Occur-check in refine.	Arnaud Spiwack	2014-12-04
*	Move the handling of the principal evar from refine to evd.	Arnaud Spiwack	2014-10-16
*	A few Global.env removed.	Hugo Herbelin	2014-10-04
*	Add syntax for naming new goals in refine: writing ?[id] instead of _	Hugo Herbelin	2014-09-30
*	Merging some functions from evarutil.ml/evd.ml.	Hugo Herbelin	2014-09-29
*	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