coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	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
*	Cleaning up of Evd. Extruding the tower of modules used to define evar_maps.	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
*	State Transaction Machine	gareuselesinge	2013-08-08
*	Removing now useless merging primitives from Evd.	ppedrot	2013-08-04
*	Small fixes due to the arrival of OCaml 3.12.	ppedrot	2013-08-03
*	Small cleaning of Evd interface.	ppedrot	2013-05-06
*	Removing a redundant function from Evd.	ppedrot	2013-05-03
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	A version of Univ.check_eq with no anomaly for Evd.set_eq_sort	letouzey	2013-03-12
*	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
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
*	Modulification of name	ppedrot	2012-12-18
*	Moved Intset and Intmap to Int namespace.	ppedrot	2012-12-14
*	Removed some FIXME related to equality on universes.	ppedrot	2012-11-26
*	Small cleaning of interface in Univ	ppedrot	2012-11-26
*	Monomorphization (pretyping)	ppedrot	2012-11-22
*	Cleaning and small optimization in CList.	ppedrot	2012-11-20
*	Reversed roles of undefined/defined evars in Evd, thus saving precious	ppedrot	2012-11-03
*	Removed many calls to OCaml generic equality. This was done by	ppedrot	2012-10-29
*	univ inconsistency error message gives evidence of a cycle	barras	2012-10-17
*	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey	2012-10-02
*	Some documentation and cleaning of CList and Util interfaces.	ppedrot	2012-09-15
*	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
*	Updating headers.	herbelin	2012-08-08
*	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot	2012-06-22
*	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey	2012-05-29
*	Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd	letouzey	2012-05-29
*	Univ: enforce_leq instead of enforce_geq for more uniformity	letouzey	2012-03-22
*	Generalized the use of evar candidates in type inference unification:	herbelin	2012-03-20
*	Noise for nothing	pboutill	2012-03-02
*	Added ability to take the type of applied metas into account when	herbelin	2011-12-17
*	Introducing a notion of evar candidates to be used when an evar is	herbelin	2011-12-16
*	When checking for emptiness, use Foo.is_empty instead of (=) Foo.empty	letouzey	2011-10-26
*	Continuing r14585 (ill-typed restriction bug).	herbelin	2011-10-25
*	Fixing uncaught exception in pr_evar_map (pr_global failed for unknown global...	herbelin	2011-10-22
*	More on r14536 (an unused pattern-matching remained in the commit).	herbelin	2011-10-11
*	Little code simplification of instantiate_evar in evd.ml	herbelin	2011-10-10
*	Added information about evar origin in pretty-printing evd for debug	herbelin	2011-10-10
*	Passed conv_algo to evar_define and move call to solve_refl to	herbelin	2011-10-10
*	More robust evar_map debugging printer	herbelin	2011-08-02
*	Cleaning debugging printer relative to new proof engine. In	herbelin	2011-06-21