coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Tentative to make unification check types at every instanciation of an	msozeau	2011-03-11
*	- Better error messages taking unif. constraints into account.	msozeau	2011-03-11
*	Forgot a use of evars_reset_evd in nf_evars, add an optional argument as	msozeau	2011-03-10
*	- Use transparency information all the way through unification and	msozeau	2011-02-17
*	Misc improvements about evar_map	letouzey	2010-12-15
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Added Chung-Kil Hur's smart "pattern" tactic (h_resolve).	herbelin	2010-06-22
*	New script dev/tools/change-header to automatically update Coq files headers.	herbelin	2010-06-22
*	Improved the efficiency of evars traverals thanks to a split of	herbelin	2010-05-13