coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	- Fix hashing of levels to get the "right" order in universe contexts etc...	Matthieu Sozeau	2014-06-04
*	- Add a primitive tclEVARUNIVERSECONTEXT to reset the universe context of an ...	Matthieu Sozeau	2014-05-08
*	- Fix treatment of global universe constraints which should be passed along	Matthieu Sozeau	2014-05-06
*	Find a more efficient fix for dealing with template universes:	Matthieu Sozeau	2014-05-06
*	- Fix eq_constr_universes restricted to Sorts.equal	Matthieu Sozeau	2014-05-06
*	- Fix bug preventing apply from unfolding Fixpoints.	Matthieu Sozeau	2014-05-06
*	Restore reasonable performance by not allocating during universe checks,	Matthieu Sozeau	2014-05-06
*	Correct rebase on STM code. Thanks to E. Tassi for help on dealing with	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Better representation of evar filters: we represent the vacuous filters of	Pierre-Marie Pédrot	2014-04-23
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Tacinterp: refactoring using Monad.	Arnaud Spiwack	2014-02-27
*	Code refactoring thanks to the new Monad module.	Arnaud Spiwack	2014-02-27
*	Useless instantiation function exported in Evd.	Pierre-Marie Pédrot	2013-11-30
*	Removing Evd.undefined_evars.	ppedrot	2013-10-28
*	Removing useless filter allocation in evar construction.	ppedrot	2013-10-27
*	Abstracting evar filter away. The API is not perfect, but better than nothing.	ppedrot	2013-10-27
*	Removing useless array-to-list and converse casts used in	ppedrot	2013-10-22
*	Removing useless evar code.	ppedrot	2013-10-06
*	Removing dubious use of evarmap manipulating functions in printing	ppedrot	2013-10-05
*	Moving side effects into evar_map. There was no reason to keep another	ppedrot	2013-10-05
*	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
*	Optimizing some evar_maps manipulation. In particular, using a [map] instead	ppedrot	2013-09-05
*	Documentation of Evd.	ppedrot	2013-09-05
*	Partly replacing list-based access functions in Evd. This is still	ppedrot	2013-09-03
*	Added a more efficient way to recover the domain of a map.	ppedrot	2013-08-25
*	State Transaction Machine	gareuselesinge	2013-08-08
*	Removing now useless merging primitives from Evd.	ppedrot	2013-08-04
*	Small cleaning of Evd interface.	ppedrot	2013-05-06
*	Removing a redundant function from Evd.	ppedrot	2013-05-03
*	Merging Context and Sign.	ppedrot	2013-04-29
*	Allowing different types of, not to be mixed, generic Stores through	ppedrot	2013-03-12
*	Locating errors from consider_remaining_unif_problems if possible	herbelin	2013-02-17
*	Renaming evar_env/evar_unfiltered_env into evar_filtered_env/evar_env	herbelin	2013-01-29
*	Modulification of name	ppedrot	2012-12-18
*	Modulification of identifier	ppedrot	2012-12-14
*	Monomorphization (pretyping)	ppedrot	2012-11-22
*	Updating headers.	herbelin	2012-08-08
*	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
*	Adds a comment: precondition on Evd.add	aspiwack	2012-04-18
*	Noise for nothing	pboutill	2012-03-02
*	Introducing a notion of evar candidates to be used when an evar is	herbelin	2011-12-16
*	Continuing r14585 (ill-typed restriction bug).	herbelin	2011-10-25
*	Cleaning debugging printer relative to new proof engine. In	herbelin	2011-06-21
*	Added a new flag for freezing evars in tactic unification. Used this	herbelin	2011-06-12
*	A better procedure for checking presence of undefined evars.	aspiwack	2011-05-13
*	First phase removing obsolete support for eta up to conversion in	herbelin	2011-05-04