coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Optimizing some evar_maps manipulation. In particular, using a [map] instead	ppedrot	2013-09-05
*	Partly replacing list-based access functions in Evd. This is still	ppedrot	2013-09-03
*	Actually using the domain function for maps.	ppedrot	2013-08-25
*	Replacing lists by sets in clear tactic.	ppedrot	2013-08-25
*	Merging Context and Sign.	ppedrot	2013-04-29
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	code simplifications concerning Summary	letouzey	2013-04-22
*	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
*	Renaming evar_env/evar_unfiltered_env into evar_filtered_env/evar_env	herbelin	2013-01-29
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
*	Fixing one part of #2830 (anomaly "defined twice" due to nested calls to	herbelin	2013-01-28
*	Modulification of identifier	ppedrot	2012-12-14
*	Moved Intset and Intmap to Int namespace.	ppedrot	2012-12-14
*	Fixed bug #2930: folded let-in's were hiding a violation to the occur	herbelin	2012-11-25
*	Monomorphization (pretyping)	ppedrot	2012-11-22
*	Cleaning and small optimization in CList.	ppedrot	2012-11-20
*	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey	2012-10-02
*	Cleaning interface of Util.	ppedrot	2012-09-18
*	Some documentation and cleaning of CList and Util interfaces.	ppedrot	2012-09-15
*	As r15801: putting everything from Util.array_* to CArray.*.	ppedrot	2012-09-14
*	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot	2012-09-14
*	This patch removes unused "open" (automatically generated from	regisgia	2012-09-14
*	The new ocaml compiler (4.00) has a lot of very cool warnings,	regisgia	2012-09-14
*	Updating headers.	herbelin	2012-08-08
*	Fixing #2836 (materialize_evar might refine as a side effect the	herbelin	2012-07-29
*	Another correction to the dependent existential variable printing	aspiwack	2012-07-10
*	Fixes bug #2678	aspiwack	2012-07-06
*	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot	2012-06-22
*	More cleaning	ppedrot	2012-06-01
*	Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd	letouzey	2012-05-29
*	Corrects a bug in the refine tactic which could drop evar bodies.	aspiwack	2012-04-18
*	Fixing a "Not_Found" bug related to commit 15061 on the use of evar candidates.	herbelin	2012-04-16
*	Speedup free_vars_and_rels_up_alias_expansion (evarconv)	gareuselesinge	2012-04-05
*	Unification: Fixing bug in materialize_evar (spotted by MathClasses).	herbelin	2012-03-26
*	Unification: Added a heuristic to solve problems of the form	herbelin	2012-03-26
*	Little bug in r15061 leading to unusable debug mode.	herbelin	2012-03-23
*	Use a careful analysis of dependencies in restricting instances to	herbelin	2012-03-20
*	Unification: when matching "?n[...,(C u1..un),...] = C u1..un" keep a	herbelin	2012-03-20
*	Generalized the use of evar candidates in type inference unification:	herbelin	2012-03-20
*	Reorganizing the structure of evarutil.ml (only restructuration, no	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
*	Fix in evarutil: add a conversion problem for ?x ts = ?x us only if ts and us...	msozeau	2012-02-15
*	Type inference unification: fixed a 8.4 bug in the presence of unification	herbelin	2012-01-04
*	Introducing a notion of evar candidates to be used when an evar is	herbelin	2011-12-16
*	Registering universe and meta/evar counters as summaries so as to	herbelin	2011-12-05