coq - The formal proof system

Age	Commit message (Expand)	Author
2016-03-20	Moving Evarutil and Proofview to engine/	Pierre-Marie Pédrot
2016-03-20	Making Evarutil independent from Reductionops.	Pierre-Marie Pédrot
2016-03-20	Splitting Evarutil in two distinct files.	Pierre-Marie Pédrot
2016-02-15	Monotonizing the Evarutil module.	Pierre-Marie Pédrot
2016-01-21	Merge branch 'v8.5'	Pierre-Marie Pédrot
2016-01-20	Update copyright headers.	Maxime Dénès
2016-01-11	CLEANUP: kernel/context.ml{,i}	Matej Kosik
2015-10-18	Making Evarutil.new_evar monotonous.	Pierre-Marie Pédrot
2015-09-26	Hardening the API of evarmaps.	Pierre-Marie Pédrot
2015-04-22	Tactical `progress` compares term up to potentially equalisable universes.	Arnaud Spiwack
2015-02-25	STM: proof state also includes meta counters	Enrico Tassi
2015-02-24	[Proofview.tclPROGRESS]: do not consider that trivial goal instantiation is p...	Arnaud Spiwack
2015-01-12	Update headers.	Maxime Dénès
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