aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2013-10-04Fix comment for new string syntax (OCaml trunk).xclerc
2013-10-03A shallow copy of a pre_env does not contain the vm cachegareuselesinge
2013-10-03STM: understand -coq-slaves-opts extra-env=VAR=valgareuselesinge
2013-10-03STM: if -coq-slaves off really imitate the old CoqIDEgareuselesinge
2013-10-03CoqIDE: when jumping to an error also move the cursorgareuselesinge
2013-10-03STM: add options to disable fallbacks to ease regression testinggareuselesinge
2013-10-03Regression test suite for STMgareuselesinge
2013-10-03STM: number of slaves passed by the command linegareuselesinge
2013-10-03STM: avoid "kill 9 pid" if we know the slave diedgareuselesinge
2013-10-03STM: delegate proofs to slaves only if they are not trivialgareuselesinge
2013-10-03STM: take a shallow snapshot for the first proof stepgareuselesinge
2013-10-01CoqIDE: when checking the whole document, center script view on errorgareuselesinge
2013-10-01CoqIDE: fixed advance_until wrt unfocusinggareuselesinge
2013-10-01typogareuselesinge
2013-10-01demo file for paral-itpgareuselesinge
2013-10-01CoqIDE: do not print cmd_stack too oftengareuselesinge
2013-10-01STM: fully force a proof ourput before sending it back to the mastergareuselesinge
2013-10-01STM: better error messages in case of marshal failuregareuselesinge
2013-10-01STM: fix reporting of ongoing tasksgareuselesinge
2013-10-01STM: exceptions caming from slaves are now localizedgareuselesinge
2013-10-01CoqIDE: do not fail hard if a message is asynchronousgareuselesinge
2013-10-01STM: Unix.kill can failgareuselesinge
2013-10-01CoqIDE: fix reset initialgareuselesinge
2013-09-30CoqIDE: use #present to raise error windowgareuselesinge
2013-09-30Backtrace.record_backtrace in CoqIDE toogareuselesinge
2013-09-30CoqIDE: wg_Tooltip removed, new tooltip handlinggareuselesinge
2013-09-30STM: better handle proof modesgareuselesinge
2013-09-30fake_ide: call Coq.init as the first actiongareuselesinge
2013-09-30ideutils: stock_to_widget was ignoring the ~size argumentgareuselesinge
2013-09-30wg_Command: detachable, less "from the 80s", query panegareuselesinge
2013-09-30wg_Session: fix copy/paste of tagged textgareuselesinge
2013-09-30STM: some refactoring, support revised CoqIDE protocolgareuselesinge
2013-09-30CoqIDE ported to the revides protocolgareuselesinge
2013-09-30fake_ide ported to the new protocol (FIXME tests fail)gareuselesinge
2013-09-30CoqIDE protocol/serialization revisedgareuselesinge
2013-09-30lib/cstack: various improvementsgareuselesinge
2013-09-30lib/vcs: various improvementsgareuselesinge
2013-09-30lib/dag: various improvementsgareuselesinge
2013-09-30lib/future: computations that are Exn can be replacedgareuselesinge
2013-09-28Made rewrite tactic strategies pure. They were using quite uglilyppedrot
2013-09-27Removing a bunch of generic equalities.ppedrot
2013-09-26Opacifying the type of strategies.ppedrot
2013-09-26Splitting Rewrite into a code part and a CAMLP4-dependent one.ppedrot
2013-09-25Removing useless evar-related stuff.ppedrot
2013-09-24Adding evar printing to debugger.ppedrot
2013-09-24Fixing ocamldebug compilation by adding thread linking.ppedrot
2013-09-20Fix name clash in "failure/inductive.v".xclerc
2013-09-20Merge "circular_subtyping?.v" tests into a single "circular_subtyping.v" test.xclerc
2013-09-20Merge "inductive?.v" tests into a single "inductive.v" test.xclerc
2013-09-20Get rid of "shouldsucceed" subdirectory by moving tests to parent directory.xclerc