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
*
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
*
STM: new "par:" goal selector, like "all:" but in parallel
Enrico Tassi
2014-08-05
*
STM: code restructured to reuse task queue for tactics
Enrico Tassi
2014-08-05
*
STM: when looking up in the cache catch Expired exc
Carst Tankink
2014-08-04
*
STM: generate Feedback message for parsing errors
Enrico Tassi
2014-08-04
*
STM: use a real priority queue
Enrico Tassi
2014-08-04
*
STM: encapsulate Pp.message in Feedback.feedback
Carst Tankink
2014-08-04
*
STM: VtQuery holds the id of the state it refers to
Carst Tankink
2014-08-04
*
STM: print goals with no duplicates
Enrico Tassi
2014-07-29
*
STM: check-vi-task fixed
Enrico Tassi
2014-07-16
*
STM: Goal printing got wrong in a merge, fixed
Enrico Tassi
2014-07-16
*
STM: let toploop plugins specify the flags for STM workers
Enrico Tassi
2014-07-11
*
STM: flag to turn off branch reopening
Enrico Tassi
2014-07-11
*
STM: add optionally takes the id of the new tip
Enrico Tassi
2014-07-11
*
Feedback: LoadedFile + Goals
Enrico Tassi
2014-07-11
*
option to always delegate futures to workers
Enrico Tassi
2014-07-10
*
Patch from Enrico Tassi to get Drop compatible with stm.
Enrico Tassi
2014-07-01
*
Typo in stm error message.
Hugo Herbelin
2014-06-28
*
all coqide specific files moved into ide/
Enrico Tassi
2014-06-25
*
Removing dead code.
Pierre-Marie Pédrot
2014-06-17
*
Moving hook code from Future to Lemmas. This seemed to disrupt compilation of
Pierre-Marie Pédrot
2014-06-08
*
Enforce a correct exception handling in declaration_hooks
Enrico Tassi
2014-06-08
*
STM: handle "Time Abort" correctly (Closes: 3332)
Enrico Tassi
2014-06-08
*
poly: remove unused attribute to STM nodes and vernac classificaiton
Enrico Tassi
2014-05-15
*
- Fix bug preventing apply from unfolding Fixpoints.
Matthieu Sozeau
2014-05-06
*
Adapt universe polymorphic branch to new handling of futures for delayed proofs.
Matthieu Sozeau
2014-05-06
*
Correct rebase on STM code. Thanks to E. Tassi for help on dealing with
Matthieu Sozeau
2014-05-06
[next]