coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Closure: fix an issue with r16959 spotted by Matthieu	letouzey	2013-11-02
*	Mod_subst.update_delta_resolver : avoid loosing Inline(_,Some _)	letouzey	2013-10-31
*	Fixing Kerpair.hash. Since the beginning, it dit not respect the type	ppedrot	2013-10-31
*	Future: better doc + restore ~pure optimization	gareuselesinge	2013-10-31
*	CoqIDE: scroll to the right position if there is an interp error	gareuselesinge	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-31
*	Avoiding useless allocations in Closure.	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
*	Revert the two last commits. My bad, I messed up git-svn commands...	ppedrot	2013-10-29
*	Profile only when CAMLRUNPARAM is set.	ppedrot	2013-10-29
*	Printing heap on every processed sentence.	ppedrot	2013-10-29
*	Sharing identity evar filters.	ppedrot	2013-10-29
*	Allocation-friendly version of [Pre_env.push_named].	ppedrot	2013-10-29
*	Optimizing universes: tail-rec, allocation friendly [compare_leq].	ppedrot	2013-10-29
*	- install evar printer for debugging	msozeau	2013-10-29
*	Native compiler: library compilation errors are now non fatal.	mdenes	2013-10-28
*	Evar leak in "absurd" tactic.	ppedrot	2013-10-28
*	Removing Evd.undefined_evars.	ppedrot	2013-10-28
*	Useless array to list conversions in proof/logic.ml.	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
*	More sharing in Constr.map_with_binders.	ppedrot	2013-10-27
*	Closure optimizations.	ppedrot	2013-10-27
*	More monomorphic List.mem + List.assoc + ...	letouzey	2013-10-24
*	inductive.ml : get rid of some obvious (Lazy.force (lazy t))	letouzey	2013-10-24
*	Rtree : cleanup of the comparing code	letouzey	2013-10-24
*	Specializing hash functions for widely used types.	ppedrot	2013-10-24
*	Restore my version of notation_ops.ml now that List.remove_assoc_f is fixed	letouzey	2013-10-24
*	Fix the semantic of the new List.remove_assoc_f	letouzey	2013-10-24
*	Oups, repair the compilation (micromega + Morphism_prop)	letouzey	2013-10-24
*	Ephemeron: add a function to run a collection cycle	gareuselesinge	2013-10-24
*	CoqIDE: fix coloring bug when jumping back to the first phrase	gareuselesinge	2013-10-24
*	Get rid of polymorphic comparison in "plugins/btauto/refl_btauto.ml".	xclerc	2013-10-24
*	Get rid of polymorphic equality in "checker/subtyping.ml".	xclerc	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.factorize_left with a parametric equality	letouzey	2013-10-23
*	CList.prefix_of and CList.drop_prefix with a parametric equality	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
*	Tacintern: avoid a match (fst (List.hd ...))	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