index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
stm
Commit message (
Expand
)
Author
Age
*
Putting the From parameter of the Require command into the AST.
Pierre-Marie Pédrot
2015-03-27
*
STM: refine the notion of "simply a tactic"
Enrico Tassi
2015-03-27
*
STM: change how proof mode switching commands are handled (decl_mode)
Enrico Tassi
2015-03-26
*
STM: avoid processing asynchronously empty proofs (Close: #4134)
Enrico Tassi
2015-03-25
*
STM: if Set Universe Polymorphism then synchronous (#4119)
Enrico Tassi
2015-03-22
*
STM: do not delegate proofs containing Print
Enrico Tassi
2015-03-22
*
STM: after every command restore the expected proof mode
Enrico Tassi
2015-03-22
*
Fixed #4138. In emacs mode Set/Unset does not print the goal anymore.
Pierre Courtieu
2015-03-20
*
STM: -debug: better explanation of why not async (#4125)
Enrico Tassi
2015-03-15
*
STM: -quick: async no Proof using but no Section (#4124)
Enrico Tassi
2015-03-15
*
Fixing bug #4055.
Pierre-Marie Pédrot
2015-03-12
*
STM: ease re-editing of Admitted proofs
Enrico Tassi
2015-03-11
*
admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)
Enrico Tassi
2015-03-11
*
STM: Considering Stack_overflow as a normal tactic error (Close #3576)
Enrico Tassi
2015-02-27
*
STM: proof state also includes meta counters
Enrico Tassi
2015-02-25
*
Future: human readable name for delegated (Close #4065)
Enrico Tassi
2015-02-21
*
STM: when async_proofs_full is set process only tasks in the perspective
Enrico Tassi
2015-02-16
*
*Queue: API to wake up all threads
Enrico Tassi
2015-02-16
*
Undo: back to 8.4 semantics (Close #3514)
Enrico Tassi
2015-02-15
*
Reset "section name" works again (Close #3933)
Enrico Tassi
2015-02-15
*
Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior
Enrico Tassi
2015-02-14
*
STM: is Flags.async_proofs_full then always delegate
Enrico Tassi
2015-02-11
*
Improving further e11854569b8 and 3e5b9ab9f75e4 on when to print goals in coq...
Hugo Herbelin
2015-02-10
*
Fix bug #4014.
Pierre-Marie Pédrot
2015-02-09
*
STM: tolerate simple side effects in async proofs (Close: 4006)
Enrico Tassi
2015-02-07
*
Fix automatic undo after nonsensical Qed in tty mode (Close: 3980)
Enrico Tassi
2015-02-05
*
Removing dead code.
Pierre-Marie Pédrot
2015-02-02
*
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
*
Inlining Spawn.kill_if in the one place were it was actually used, thus
Pierre-Marie Pédrot
2014-12-25
*
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
*
Proof using: New vernacular to name sets of section variables
Enrico Tassi
2014-12-18
*
Fix compilation with ocaml 4.0.0
Enrico Tassi
2014-12-17
*
STM: resilient on errors in non delegated proofs
Enrico Tassi
2014-12-17
*
CoqIDE: cleanup jobs window on worker death
Enrico Tassi
2014-12-17
*
STM: rename and simplify flags
Enrico Tassi
2014-12-17
*
STM: simplify state management
Enrico Tassi
2014-12-17
*
AsyncTaskQueue: simpler model (no parking area, continuation tasks)
Enrico Tassi
2014-12-17
*
WorkerPool: simpler fuctor and no more parking area
Enrico Tassi
2014-12-17
*
TQueue: a way to unblock threads begin destroyed waiting on pop
Enrico Tassi
2014-12-17
*
Spawn: fix request of Gc statistics
Enrico Tassi
2014-12-17
[next]