aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2013-10-11STM: prefix debug messages with slave-idgareuselesinge
2013-10-11More comments in ide_slavegareuselesinge
2013-10-11STM: cancel slaves working on outdated jobsgareuselesinge
2013-10-11Vcs: the gc method returns the set of nodes that were collectedgareuselesinge
2013-10-11Dag: some comments on the concept of clustergareuselesinge
2013-10-11CoqIDE: single underline for errorsgareuselesinge
2013-10-10CoqIDE: error reporting fixedgareuselesinge
2013-10-10Document: undoing inside a focused zone does not require unfocusinggareuselesinge
2013-10-10CoqIDE: ported to Documentgareuselesinge
2013-10-10fake_ide: ported to Document + 2 tests for editing a proof (locally)gareuselesinge
2013-10-10CoqIDE: move cmd_stack to a separate module: Documentgareuselesinge
2013-10-10STM: a proof with nested proofs cannot be delegatedgareuselesinge
2013-10-10STM: add "Stm Wait" to wait for the slaves to complete their jobsgareuselesinge
2013-10-10Clib: fold_left_until added to CListgareuselesinge
2013-10-10CoqIDE: a comment is not a sentencegareuselesinge
2013-10-09Fixing CAMLP4 compilation.ppedrot
2013-10-08Small code cleaning in Evarutil.ppedrot
2013-10-08Fixing 2 output test-suites.ppedrot
2013-10-07STM: new command "Stm PrintDag" to force printing the dag to /tmpgareuselesinge
2013-10-07STM: fix verbosity of queriesgareuselesinge
2013-10-07fake_ide: speak the new protocolgareuselesinge
2013-10-07STM: spit a warning if an out of bound Back* command is issuedgareuselesinge
2013-10-07coqtop: init STM before loading rcfilegareuselesinge
2013-10-07CoqIDE: fix jumpig out of a focused proofgareuselesinge
2013-10-07CoqIDE: cStack -> Documentgareuselesinge
2013-10-07cStack: make it just a Stack with some extra APIgareuselesinge
2013-10-06Removing useless evar code.ppedrot
2013-10-06Added a [modify] function to maps.ppedrot
2013-10-06Removing uses of Evar.add in class-related functions.ppedrot
2013-10-05Removing dubious use of evarmap manipulating functions in printingppedrot
2013-10-05Moving side effects into evar_map. There was no reason to keep anotherppedrot
2013-10-05Fixing potential evar leak in Rewrite, and removing dead code.ppedrot
2013-10-05Fixing potential evar leak in Equality.ppedrot