index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
stm
/
stm.ml
Commit message (
Expand
)
Author
Age
*
Update headers.
Maxime Dénès
2015-01-12
*
STM: fix handling of side effects in vio2vo
Enrico Tassi
2015-01-09
*
Hook when state arrives on master.
Enrico Tassi
2015-01-07
*
rename: vi -> vio
Enrico Tassi
2015-01-06
*
STM: Make assert unneeded (Close 3898)
Enrico Tassi
2015-01-04
*
STM: check with the kernel proof terms on the worker too
Enrico Tassi
2014-12-27
*
STM: fix processing of errors
Enrico Tassi
2014-12-27
*
STM: module Pp is open
Enrico Tassi
2014-12-27
*
STM: do not call process_error twice (Close: 3880)
Enrico Tassi
2014-12-26
*
STM: remove dead code
Enrico Tassi
2014-12-26
*
STM: cleanup code for Admitted
Enrico Tassi
2014-12-23
*
Vi2vo: fix handling of univ constraints coming from the body
Enrico Tassi
2014-12-23
*
STM: resilient on errors in non delegated proofs
Enrico Tassi
2014-12-17
*
STM: rename and simplify flags
Enrico Tassi
2014-12-17
*
STM: simplify state management
Enrico Tassi
2014-12-17
*
Getting rid of Exninfo hacks.
Pierre-Marie Pédrot
2014-12-16
*
Improving e11854569b8 on when to print goals in coqtop mode.
Hugo Herbelin
2014-12-07
*
Trying a new policy for when to automatically print goals (granting
Hugo Herbelin
2014-12-04
*
fix compilation on ocaml 3.12 (Close: 3833)
Enrico Tassi
2014-11-28
*
STM: if a-p-always-delegate fetch states from parked worker on edit-at
Enrico Tassi
2014-11-28
*
STM: hook called whenever a state is unreachable
Enrico Tassi
2014-11-27
*
async_queries_* merged with async_proofs_*
Enrico Tassi
2014-11-27
*
AsyncTaskQueue: parsin can also happen in the workers now
Enrico Tassi
2014-11-27
*
STM: new API async_query
Enrico Tassi
2014-11-27
*
STM: put hooks in key events to let plugins customize the feedback
Enrico Tassi
2014-11-27
*
Feedback: API cleaned up, documented and made user extensible
Enrico Tassi
2014-11-27
*
STM: code refactoring
Enrico Tassi
2014-11-03
*
STM: fix printing of goals when on a tty interface
Enrico Tassi
2014-11-03
*
Fix error reporting id on VtUnknown commands
Enrico Tassi
2014-11-03
*
Add [Info] command.
Arnaud Spiwack
2014-11-01
*
Feedback message: hold extra info to help routing
Enrico Tassi
2014-10-31
*
STM: new worker for queries
Enrico Tassi
2014-10-31
*
STM: reorganize code and file names
Enrico Tassi
2014-10-31
*
Fixes for PG (Close 3763, 3770)
Enrico Tassi
2014-10-27
*
Goal printing made uniform: always done in STM (close 3585)
Enrico Tassi
2014-10-22
*
Goal: remove most of the API (make [Goal.goal] concrete).
Arnaud Spiwack
2014-10-16
*
Fix -async-proofs-always-delegate (close 3740)
Enrico Tassi
2014-10-15
*
Stm: more precise representation of nested proofs
Enrico Tassi
2014-10-13
*
STM: primitives to snapshot a .vi while in interactive mode
Enrico Tassi
2014-10-13
*
STM: simplify how the term part of a side effect is retrieved
Enrico Tassi
2014-10-13
*
library/opaqueTables: enable their use in interactive mode
Enrico Tassi
2014-10-13
*
STM: report the (structured) goals as XML
Carst Tankink
2014-10-01
*
XML pretty printing for AST (work by François Poulain, project DoCoq)
Enrico Tassi
2014-09-29
*
Undo prints only if coqtop || emacs
Enrico Tassi
2014-09-16
*
Marshalling errors should be bold and red (should never happen actually)
Enrico Tassi
2014-09-09
*
Back: print subgoals as in 8.4 (Close: 3585)
Enrico Tassi
2014-09-09
*
BackTo not part of the doc when used by emacs
Enrico Tassi
2014-09-09
*
Undo: if the ui is coqtop (command line) then Undo is not part of the doc.
Enrico Tassi
2014-09-09
*
Dropped proofs (Abort) are evaluated synchronously (Closes: 3550, 3407)
Enrico Tassi
2014-09-09
*
stm: use xlabel insted of label in dot (debug) output
Enrico Tassi
2014-09-02
[next]