coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Update comments in matching.mli.	aspiwack	2013-11-14
*	Removing partial applications in Reductionops.	ppedrot	2013-11-08
*	Partial application hunt.	ppedrot	2013-11-07
*	Less partial applications in Vars, as well as better memory allocation.	ppedrot	2013-11-06
*	Preventing useless allocations in Reductionops.instance.	ppedrot	2013-11-05
*	Nicer infered names in refine.	aspiwack	2013-11-04
*	push_rel_context: do not rename section variables.	aspiwack	2013-11-02
*	Fix compilation of pattern matching wrt variables: alias.	aspiwack	2013-11-02
*	Fix the compilation of pattern matching wrt to variables.	aspiwack	2013-11-02
*	A newly introduced variable inside a named context is no longer α-renamed.	aspiwack	2013-11-02
*	Conv_orable made functional and part of pre_env	gareuselesinge	2013-10-31
*	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
*	Optimization in unification: when checking that the head of a term is an	ppedrot	2013-10-29
*	Useless array-to-list casts in Unification.	ppedrot	2013-10-29
*	Do not generate useless argument arrays in whd_* functions.	ppedrot	2013-10-29
*	Prevent [Evarutil.whd_head_evar] from uselessly reallocating arrays.	ppedrot	2013-10-29
*	[Reductionops.append_stack_app]: do not allocate a useless array.	ppedrot	2013-10-29
*	Sharing identity evar filters.	ppedrot	2013-10-29
*	- install evar printer for debugging	msozeau	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
*	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