coq - The formal proof system

Age	Commit message (Expand)	Author
2014-02-03	Tracking memory misallocation by trying to improve sharing.	Pierre-Marie Pédrot
2014-01-29	Using Map.smartmap whenever deemed useful.	Pierre-Marie Pédrot
2014-01-27	Abstracting away coercion indexes in Classops.	Pierre-Marie Pédrot
2014-01-26	Coercions: avoid imperative data structure	Enrico Tassi
2014-01-07	STM: additional fix for STM + vm_compute	Enrico Tassi
2013-12-30	When resetting an evarmap with the unsafe function Evd.evars_reset_evd with	Pierre-Marie Pédrot
2013-12-30	Support for evars and metas in native compiler.	Maxime Dénès
2013-12-06	Fix test-suite/success/evars.v.	Arnaud Spiwack
2013-12-03	Removing useless meta-related functions.	Pierre-Marie Pédrot
2013-11-30	Better heuristic for name generation backward compatibility. We fallback	Pierre-Marie Pédrot
2013-11-30	Useless instantiation function exported in Evd.	Pierre-Marie Pédrot
2013-11-30	Tentative fix to recover fresh name generation as it was before	Pierre-Marie Pédrot
2013-11-27	Adding generic solvers to term holes. For now, no resolution mechanism nor	Pierre-Marie Pédrot
2013-11-25	Factoring: is_section_variable.	Arnaud Spiwack
2013-11-25	Typo resulting in bad eta-expansion of destructing let's body.	Hugo Herbelin
2013-11-14	Update comments in matching.mli.	aspiwack
2013-11-08	Removing partial applications in Reductionops.	ppedrot
2013-11-07	Partial application hunt.	ppedrot
2013-11-06	Less partial applications in Vars, as well as better memory allocation.	ppedrot
2013-11-05	Preventing useless allocations in Reductionops.instance.	ppedrot
2013-11-04	Nicer infered names in refine.	aspiwack
2013-11-02	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-10-31	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-30	Various optimizations of Evd.meta_* functions.	ppedrot
2013-10-30	More efficient implementation of [Evd.retract_coercible_metas].	ppedrot
2013-10-29	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-28	Removing Evd.undefined_evars.	ppedrot
2013-10-27	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-24	More monomorphic List.mem + List.assoc + ...	letouzey
2013-10-24	Turn many List.assoc into List.assoc_f	letouzey
2013-10-23	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-22	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