index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2013-10-04
Fix comment for new string syntax (OCaml trunk).
xclerc
2013-10-03
A shallow copy of a pre_env does not contain the vm cache
gareuselesinge
2013-10-03
STM: understand -coq-slaves-opts extra-env=VAR=val
gareuselesinge
2013-10-03
STM: if -coq-slaves off really imitate the old CoqIDE
gareuselesinge
2013-10-03
CoqIDE: when jumping to an error also move the cursor
gareuselesinge
2013-10-03
STM: add options to disable fallbacks to ease regression testing
gareuselesinge
2013-10-03
Regression test suite for STM
gareuselesinge
2013-10-03
STM: number of slaves passed by the command line
gareuselesinge
2013-10-03
STM: avoid "kill 9 pid" if we know the slave died
gareuselesinge
2013-10-03
STM: delegate proofs to slaves only if they are not trivial
gareuselesinge
2013-10-03
STM: take a shallow snapshot for the first proof step
gareuselesinge
2013-10-01
CoqIDE: when checking the whole document, center script view on error
gareuselesinge
2013-10-01
CoqIDE: fixed advance_until wrt unfocusing
gareuselesinge
2013-10-01
typo
gareuselesinge
2013-10-01
demo file for paral-itp
gareuselesinge
2013-10-01
CoqIDE: do not print cmd_stack too often
gareuselesinge
2013-10-01
STM: fully force a proof ourput before sending it back to the master
gareuselesinge
2013-10-01
STM: better error messages in case of marshal failure
gareuselesinge
2013-10-01
STM: fix reporting of ongoing tasks
gareuselesinge
2013-10-01
STM: exceptions caming from slaves are now localized
gareuselesinge
2013-10-01
CoqIDE: do not fail hard if a message is asynchronous
gareuselesinge
2013-10-01
STM: Unix.kill can fail
gareuselesinge
2013-10-01
CoqIDE: fix reset initial
gareuselesinge
2013-09-30
CoqIDE: use #present to raise error window
gareuselesinge
2013-09-30
Backtrace.record_backtrace in CoqIDE too
gareuselesinge
2013-09-30
CoqIDE: wg_Tooltip removed, new tooltip handling
gareuselesinge
2013-09-30
STM: better handle proof modes
gareuselesinge
2013-09-30
fake_ide: call Coq.init as the first action
gareuselesinge
2013-09-30
ideutils: stock_to_widget was ignoring the ~size argument
gareuselesinge
2013-09-30
wg_Command: detachable, less "from the 80s", query pane
gareuselesinge
2013-09-30
wg_Session: fix copy/paste of tagged text
gareuselesinge
2013-09-30
STM: some refactoring, support revised CoqIDE protocol
gareuselesinge
2013-09-30
CoqIDE ported to the revides protocol
gareuselesinge
2013-09-30
fake_ide ported to the new protocol (FIXME tests fail)
gareuselesinge
2013-09-30
CoqIDE protocol/serialization revised
gareuselesinge
2013-09-30
lib/cstack: various improvements
gareuselesinge
2013-09-30
lib/vcs: various improvements
gareuselesinge
2013-09-30
lib/dag: various improvements
gareuselesinge
2013-09-30
lib/future: computations that are Exn can be replaced
gareuselesinge
2013-09-28
Made rewrite tactic strategies pure. They were using quite uglily
ppedrot
2013-09-27
Removing a bunch of generic equalities.
ppedrot
2013-09-26
Opacifying the type of strategies.
ppedrot
2013-09-26
Splitting Rewrite into a code part and a CAMLP4-dependent one.
ppedrot
2013-09-25
Removing useless evar-related stuff.
ppedrot
2013-09-24
Adding evar printing to debugger.
ppedrot
2013-09-24
Fixing ocamldebug compilation by adding thread linking.
ppedrot
2013-09-20
Fix name clash in "failure/inductive.v".
xclerc
2013-09-20
Merge "circular_subtyping?.v" tests into a single "circular_subtyping.v" test.
xclerc
2013-09-20
Merge "inductive?.v" tests into a single "inductive.v" test.
xclerc
2013-09-20
Get rid of "shouldsucceed" subdirectory by moving tests to parent directory.
xclerc
[next]