aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* Get rid of polymorphic comparison in "plugins/btauto/refl_btauto.ml".Gravatar xclerc2013-10-24
* Get rid of polymorphic equality in "checker/subtyping.ml".Gravatar xclerc2013-10-24
* Turn many List.assoc into List.assoc_fGravatar letouzey2013-10-24
* cList: a few alternative to hashtbl-based uniquize, distinct, subsetGravatar letouzey2013-10-23
* CList.factorize_left with a parametric equalityGravatar letouzey2013-10-23
* CList.prefix_of and CList.drop_prefix with a parametric equalityGravatar letouzey2013-10-23
* cList.index is now cList.index_f, same for index0Gravatar letouzey2013-10-23
* cList: set-as-list functions are now with an explicit comparisonGravatar letouzey2013-10-23
* Tacintern: avoid a match (fst (List.hd ...))Gravatar letouzey2013-10-23
* Small optimizations in unification.Gravatar ppedrot2013-10-23
* Removing List.mem in Namegen. We may choose a better fitted datastructure tha...Gravatar ppedrot2013-10-23
* Optimizing Vars.replace_varsGravatar ppedrot2013-10-23
* Removing some generic equalities.Gravatar ppedrot2013-10-22
* Moving potentially costly computation from exception raising to messageGravatar ppedrot2013-10-22
* Removing useless array-to-list and converse casts used inGravatar ppedrot2013-10-22
* Optimizing evar filters. It seems to cost quite a lot in unification,Gravatar ppedrot2013-10-22
* Various optimizations in Constr, such as term sharing and allocationGravatar ppedrot2013-10-22
* More efficient operations in CArray.Gravatar ppedrot2013-10-22
* STM: proper error message if the GUI edits_at a dummy stateGravatar gareuselesinge2013-10-22
* STM: do not enrich exceptions more than onceGravatar gareuselesinge2013-10-22
* CoqIDE: always retag on insertGravatar gareuselesinge2013-10-22
* CoqIDE: do not try to backtrack to a dummy idGravatar gareuselesinge2013-10-22
* emacs config: next-error search path ok even if default-directory unset.Gravatar courtieu2013-10-22
* Wg_Find: regex + case insensitive find/replace supportGravatar gareuselesinge2013-10-22
* wg_Detachable: move out of wg_CommandGravatar gareuselesinge2013-10-22
* Wg_Commands: fix warning "widget not within a GtkWindow"Gravatar gareuselesinge2013-10-22
* Wg_Commands: when detached display the buffer nameGravatar gareuselesinge2013-10-22
* CoqIDE: display in the errors window also the slaves statusGravatar gareuselesinge2013-10-22
* STM: send the gui the status of the slavesGravatar gareuselesinge2013-10-22
* New feedback message: SlaveStatusGravatar gareuselesinge2013-10-22
* wg_Commands: smaller icons in tabsGravatar gareuselesinge2013-10-22
* ideutils: support custom size for stock iconsGravatar gareuselesinge2013-10-22
* proof modes: use ephemerons to represent them in proof stateGravatar gareuselesinge2013-10-18
* Coqtop: fix looping over a broken state.Gravatar gareuselesinge2013-10-18
* declaration_hooks use EphemeronGravatar gareuselesinge2013-10-18
* Future: ported to Ephemeron + exception enhancingGravatar gareuselesinge2013-10-18
* Ephemeron: marshaling friendly keysGravatar gareuselesinge2013-10-18
* Summary: if an unfreeze function fails, print an error messageGravatar gareuselesinge2013-10-18
* STM: not optimize proofs containing an UndoGravatar gareuselesinge2013-10-18
* Reintroduce "or" instead of "||" as the latter is redifined in "sos_lib.ml" w...Gravatar xclerc2013-10-16
* Some more hand-written comparison functions to avoid polymorphic comparison.Gravatar xclerc2013-10-14
* Avoid polymorphic comparison (plugins/rtauto).Gravatar xclerc2013-10-14
* Avoid polymorphic comparison (plugins/cc).Gravatar xclerc2013-10-14
* Avoid polymorphic comparison (coqdoc).Gravatar xclerc2013-10-14
* Remove some uses of local modules (some were unused, some were costly).Gravatar xclerc2013-10-14
* Getting rid of the use of deprecated elements (from the OCaml standard library).Gravatar xclerc2013-10-14
* CoqIDE: make error background configurableGravatar gareuselesinge2013-10-11
* STM: prefix debug messages with slave-idGravatar gareuselesinge2013-10-11
* More comments in ide_slaveGravatar gareuselesinge2013-10-11
* STM: cancel slaves working on outdated jobsGravatar gareuselesinge2013-10-11