coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	More monomorphic List.mem + List.assoc + ...	letouzey	2013-10-24
*	Turn many List.assoc into List.assoc_f	letouzey	2013-10-24
*	cList: a few alternative to hashtbl-based uniquize, distinct, subset	letouzey	2013-10-23
*	cList.index is now cList.index_f, same for index0	letouzey	2013-10-23
*	cList: set-as-list functions are now with an explicit comparison	letouzey	2013-10-23
*	Small optimizations in unification.	ppedrot	2013-10-23
*	Removing List.mem in Namegen. We may choose a better fitted datastructure tha...	ppedrot	2013-10-23
*	Removing some generic equalities.	ppedrot	2013-10-22
*	Moving potentially costly computation from exception raising to message	ppedrot	2013-10-22
*	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
*	Various optimizations in Constr, such as term sharing and allocation	ppedrot	2013-10-22
*	Small code cleaning in Evarutil.	ppedrot	2013-10-08
*	Removing useless evar code.	ppedrot	2013-10-06
*	Removing uses of Evar.add in class-related functions.	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 a bunch of generic equalities.	ppedrot	2013-09-27
*	Removing useless evar-related stuff.	ppedrot	2013-09-25
*	Get rid of the uses of deprecated OCaml elements (still remaining compatible ...	xclerc	2013-09-19
*	At least made the evar type opaque! There are still 5 remaining unsafe	ppedrot	2013-09-18
*	Removing the last global evar generation in Term_dnet. The very	ppedrot	2013-09-18
*	Removing unused code from Term_dnet.	ppedrot	2013-09-18
*	Removing almost all new_untyped_evar, and a bunch of Evd.add.	ppedrot	2013-09-18
*	Taming the simpl evar hack that used to use negative evars.	ppedrot	2013-09-18
*	Unplugging Autoinstance. The code is still here if someone wishes	ppedrot	2013-09-12
*	Optimizing some evar_maps manipulation. In particular, using a [map] instead	ppedrot	2013-09-05
*	Documentation of Evd.	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
*	Removing association lists in Reductionops. Btw, defining the dual of the	ppedrot	2013-08-25
*	Actually using the domain function for maps.	ppedrot	2013-08-25
*	Added a more efficient way to recover the domain of a map.	ppedrot	2013-08-25
*	Replacing lists by sets in clear tactic.	ppedrot	2013-08-25
*	Nicer code concerning dirpaths and modpath around Lib	letouzey	2013-08-22
*	Misc changes around coqtop.ml :	letouzey	2013-08-22
*	Universe counters on slaves are in sync with master	gareuselesinge	2013-08-20
*	State Transaction Machine	gareuselesinge	2013-08-08
*	Removing useless casts between arrays and lists.	ppedrot	2013-08-04
*	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
*	Fixing #3088. Translation from globconstrs to patterns was forgetting	ppedrot	2013-08-01
*	Added printing of instance priority to the Print Instances command.	ppedrot	2013-08-01
*	- Fix uncaught exception NotASort from reductionops, moving decomp_sort to re...	msozeau	2013-07-19
*	Revising r16550 about providing intro patterns for applying injection:	herbelin	2013-07-09
*	Using the whole tactic environment while Pretyping.	ppedrot	2013-06-24
*	Generalizing the use of maps instead of lists in the interpretation	ppedrot	2013-06-22
*	- Keep the refinement of existing evars comming from unification with a rewri...	msozeau	2013-06-19
*	One more fix for rewrite: disallow resolving of the (partial) constraints	msozeau	2013-06-12
*	Replacing lists by maps in matching interpretation.	ppedrot	2013-06-05