aboutsummaryrefslogtreecommitdiff
path: root/stm
AgeCommit message (Expand)Author
2015-02-27STM: Considering Stack_overflow as a normal tactic error (Close #3576)Enrico Tassi
2015-02-25STM: proof state also includes meta countersEnrico Tassi
2015-02-21Future: human readable name for delegated (Close #4065)Enrico Tassi
2015-02-16STM: when async_proofs_full is set process only tasks in the perspectiveEnrico Tassi
2015-02-16*Queue: API to wake up all threadsEnrico Tassi
2015-02-15Undo: back to 8.4 semantics (Close #3514)Enrico Tassi
2015-02-15Reset "section name" works again (Close #3933)Enrico Tassi
2015-02-14Abstract: "Qed export ident, .., ident" to preserve v8.4 behaviorEnrico Tassi
2015-02-11STM: is Flags.async_proofs_full then always delegateEnrico Tassi
2015-02-10Improving further e11854569b8 and 3e5b9ab9f75e4 on when to print goals in coq...Hugo Herbelin
2015-02-09Fix bug #4014.Pierre-Marie Pédrot
2015-02-07STM: tolerate simple side effects in async proofs (Close: 4006)Enrico Tassi
2015-02-05Fix automatic undo after nonsensical Qed in tty mode (Close: 3980)Enrico Tassi
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2015-01-09STM: fix handling of side effects in vio2voEnrico Tassi
2015-01-07Hook when state arrives on master.Enrico Tassi
2015-01-06rename: vi -> vioEnrico Tassi
2015-01-04STM: Make assert unneeded (Close 3898)Enrico Tassi
2014-12-27STM: check with the kernel proof terms on the worker tooEnrico Tassi
2014-12-27STM: fix processing of errorsEnrico Tassi
2014-12-27STM: module Pp is openEnrico Tassi
2014-12-26STM: do not call process_error twice (Close: 3880)Enrico Tassi
2014-12-26STM: remove dead codeEnrico Tassi
2014-12-25Inlining Spawn.kill_if in the one place were it was actually used, thusPierre-Marie Pédrot
2014-12-23STM: cleanup code for AdmittedEnrico Tassi
2014-12-23Vi2vo: fix handling of univ constraints coming from the bodyEnrico Tassi
2014-12-18Proof using: New vernacular to name sets of section variablesEnrico Tassi
2014-12-17Fix compilation with ocaml 4.0.0Enrico Tassi
2014-12-17STM: resilient on errors in non delegated proofsEnrico Tassi
2014-12-17CoqIDE: cleanup jobs window on worker deathEnrico Tassi
2014-12-17STM: rename and simplify flagsEnrico Tassi
2014-12-17STM: simplify state managementEnrico Tassi
2014-12-17AsyncTaskQueue: simpler model (no parking area, continuation tasks)Enrico Tassi
2014-12-17WorkerPool: simpler fuctor and no more parking areaEnrico Tassi
2014-12-17TQueue: a way to unblock threads begin destroyed waiting on popEnrico Tassi
2014-12-17Spawn: fix request of Gc statisticsEnrico Tassi
2014-12-17CThread: use a different type for thread friendly in_channelsEnrico Tassi
2014-12-16Getting rid of Exninfo hacks.Pierre-Marie Pédrot
2014-12-07Improving e11854569b8 on when to print goals in coqtop mode.Hugo Herbelin
2014-12-04Trying a new policy for when to automatically print goals (grantingHugo Herbelin
2014-11-28fix compilation on ocaml 3.12 (Close: 3833)Enrico Tassi
2014-11-28STM: if a-p-always-delegate fetch states from parked worker on edit-atEnrico Tassi
2014-11-27STM: hook called whenever a state is unreachableEnrico Tassi
2014-11-27async_queries_* merged with async_proofs_*Enrico Tassi
2014-11-27AsyncTaskQueue: parsin can also happen in the workers nowEnrico Tassi
2014-11-27STM: new API async_queryEnrico Tassi
2014-11-27AsyncTaskQueue: API to park a workerEnrico Tassi
2014-11-27WorkerPool: API to move a worker from an active pool to a parking oneEnrico Tassi
2014-11-27TQueue: let reader be picky when popping an itemEnrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 15:30:25 +0000