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
*	Tacinterp: refactoring using Monad.	Arnaud Spiwack	2014-02-27
*	Code refactoring thanks to the new Monad module.	Arnaud Spiwack	2014-02-27
*	Using Map.smartmap whenever deemed useful.	Pierre-Marie Pédrot	2014-01-29
*	When resetting an evarmap with the unsafe function Evd.evars_reset_evd with	Pierre-Marie Pédrot	2013-12-30
*	Useless instantiation function exported in Evd.	Pierre-Marie Pédrot	2013-11-30
*	Efficient filtered functions in Evd. We test that a filter is actually	ppedrot	2013-10-31
*	Various optimizations of Evd.meta_* functions.	ppedrot	2013-10-30
*	More efficient implementation of [Evd.retract_coercible_metas].	ppedrot	2013-10-30
*	Sharing identity evar filters.	ppedrot	2013-10-29
*	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
*	Closure optimizations.	ppedrot	2013-10-27
*	cList: set-as-list functions are now with an explicit comparison	letouzey	2013-10-23
*	Removing useless array-to-list and converse casts used in	ppedrot	2013-10-22
*	Optimizing evar filters. It seems to cost quite a lot in unification,	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
*	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