aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2013-10-28Removing Evd.undefined_evars.ppedrot
2013-10-28Useless array to list conversions in proof/logic.ml.ppedrot
2013-10-27Removing useless filter allocation in evar construction.ppedrot
2013-10-27Abstracting evar filter away. The API is not perfect, but better than nothing.ppedrot
2013-10-27More sharing in Constr.map_with_binders.ppedrot
2013-10-27Closure optimizations.ppedrot
2013-10-24More monomorphic List.mem + List.assoc + ...letouzey
2013-10-24inductive.ml : get rid of some obvious (Lazy.force (lazy t))letouzey
2013-10-24Rtree : cleanup of the comparing codeletouzey
2013-10-24Specializing hash functions for widely used types.ppedrot
2013-10-24Restore my version of notation_ops.ml now that List.remove_assoc_f is fixedletouzey
2013-10-24Fix the semantic of the new List.remove_assoc_fletouzey
2013-10-24Oups, repair the compilation (micromega + Morphism_prop)letouzey
2013-10-24Ephemeron: add a function to run a collection cyclegareuselesinge
2013-10-24CoqIDE: fix coloring bug when jumping back to the first phrasegareuselesinge
2013-10-24Get rid of polymorphic comparison in "plugins/btauto/refl_btauto.ml".xclerc
2013-10-24Get rid of polymorphic equality in "checker/subtyping.ml".xclerc
2013-10-24Turn many List.assoc into List.assoc_fletouzey
2013-10-23cList: a few alternative to hashtbl-based uniquize, distinct, subsetletouzey
2013-10-23CList.factorize_left with a parametric equalityletouzey
2013-10-23CList.prefix_of and CList.drop_prefix with a parametric equalityletouzey
2013-10-23cList.index is now cList.index_f, same for index0letouzey
2013-10-23cList: set-as-list functions are now with an explicit comparisonletouzey
2013-10-23Tacintern: avoid a match (fst (List.hd ...))letouzey
2013-10-23Small optimizations in unification.ppedrot
2013-10-23Removing List.mem in Namegen. We may choose a better fitted datastructure tha...ppedrot
2013-10-23Optimizing Vars.replace_varsppedrot
2013-10-22Removing some generic equalities.ppedrot
2013-10-22Moving potentially costly computation from exception raising to messageppedrot
2013-10-22Removing useless array-to-list and converse casts used inppedrot
2013-10-22Optimizing evar filters. It seems to cost quite a lot in unification,ppedrot
2013-10-22Various optimizations in Constr, such as term sharing and allocationppedrot
2013-10-22More efficient operations in CArray.ppedrot
2013-10-22STM: proper error message if the GUI edits_at a dummy stategareuselesinge
2013-10-22STM: do not enrich exceptions more than oncegareuselesinge
2013-10-22CoqIDE: always retag on insertgareuselesinge
2013-10-22CoqIDE: do not try to backtrack to a dummy idgareuselesinge
2013-10-22emacs config: next-error search path ok even if default-directory unset.courtieu
2013-10-22Wg_Find: regex + case insensitive find/replace supportgareuselesinge
2013-10-22wg_Detachable: move out of wg_Commandgareuselesinge
2013-10-22Wg_Commands: fix warning "widget not within a GtkWindow"gareuselesinge
2013-10-22Wg_Commands: when detached display the buffer namegareuselesinge
2013-10-22CoqIDE: display in the errors window also the slaves statusgareuselesinge
2013-10-22STM: send the gui the status of the slavesgareuselesinge
2013-10-22New feedback message: SlaveStatusgareuselesinge
2013-10-22wg_Commands: smaller icons in tabsgareuselesinge
2013-10-22ideutils: support custom size for stock iconsgareuselesinge
2013-10-18proof modes: use ephemerons to represent them in proof stategareuselesinge
2013-10-18Coqtop: fix looping over a broken state.gareuselesinge
2013-10-18declaration_hooks use Ephemerongareuselesinge
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 18:56:04 +0000