aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2013-10-18Future: ported to Ephemeron + exception enhancinggareuselesinge
2013-10-18Ephemeron: marshaling friendly keysgareuselesinge
2013-10-18Summary: if an unfreeze function fails, print an error messagegareuselesinge
2013-10-18STM: not optimize proofs containing an Undogareuselesinge
2013-10-16Reintroduce "or" instead of "||" as the latter is redifined in "sos_lib.ml" w...xclerc
2013-10-14Some more hand-written comparison functions to avoid polymorphic comparison.xclerc
2013-10-14Avoid polymorphic comparison (plugins/rtauto).xclerc
2013-10-14Avoid polymorphic comparison (plugins/cc).xclerc
2013-10-14Avoid polymorphic comparison (coqdoc).xclerc
2013-10-14Remove some uses of local modules (some were unused, some were costly).xclerc
2013-10-14Getting rid of the use of deprecated elements (from the OCaml standard library).xclerc
2013-10-11CoqIDE: make error background configurablegareuselesinge
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 09:40:12 +0000