coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	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
*	Optimizing Vars.replace_vars	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
*	More efficient operations in CArray.	ppedrot	2013-10-22
*	STM: proper error message if the GUI edits_at a dummy state	gareuselesinge	2013-10-22
*	STM: do not enrich exceptions more than once	gareuselesinge	2013-10-22
*	CoqIDE: always retag on insert	gareuselesinge	2013-10-22
*	CoqIDE: do not try to backtrack to a dummy id	gareuselesinge	2013-10-22
*	emacs config: next-error search path ok even if default-directory unset.	courtieu	2013-10-22
*	Wg_Find: regex + case insensitive find/replace support	gareuselesinge	2013-10-22
*	wg_Detachable: move out of wg_Command	gareuselesinge	2013-10-22
*	Wg_Commands: fix warning "widget not within a GtkWindow"	gareuselesinge	2013-10-22
*	Wg_Commands: when detached display the buffer name	gareuselesinge	2013-10-22
*	CoqIDE: display in the errors window also the slaves status	gareuselesinge	2013-10-22
*	STM: send the gui the status of the slaves	gareuselesinge	2013-10-22
*	New feedback message: SlaveStatus	gareuselesinge	2013-10-22
*	wg_Commands: smaller icons in tabs	gareuselesinge	2013-10-22
*	ideutils: support custom size for stock icons	gareuselesinge	2013-10-22
*	proof modes: use ephemerons to represent them in proof state	gareuselesinge	2013-10-18
*	Coqtop: fix looping over a broken state.	gareuselesinge	2013-10-18
*	declaration_hooks use Ephemeron	gareuselesinge	2013-10-18