aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/stm.ml
Commit message (Expand)AuthorAge
* STM: ease re-editing of Admitted proofsGravatar Enrico Tassi2015-03-11
* admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Gravatar Enrico Tassi2015-03-11
* STM: Considering Stack_overflow as a normal tactic error (Close #3576)Gravatar Enrico Tassi2015-02-27
* STM: proof state also includes meta countersGravatar Enrico Tassi2015-02-25
* Future: human readable name for delegated (Close #4065)Gravatar Enrico Tassi2015-02-21
* STM: when async_proofs_full is set process only tasks in the perspectiveGravatar Enrico Tassi2015-02-16
* Undo: back to 8.4 semantics (Close #3514)Gravatar Enrico Tassi2015-02-15
* Abstract: "Qed export ident, .., ident" to preserve v8.4 behaviorGravatar Enrico Tassi2015-02-14
* STM: is Flags.async_proofs_full then always delegateGravatar Enrico Tassi2015-02-11
* Improving further e11854569b8 and 3e5b9ab9f75e4 on when to print goals in coq...Gravatar Hugo Herbelin2015-02-10
* STM: tolerate simple side effects in async proofs (Close: 4006)Gravatar Enrico Tassi2015-02-07
* Fix automatic undo after nonsensical Qed in tty mode (Close: 3980)Gravatar Enrico Tassi2015-02-05
* Update headers.Gravatar Maxime Dénès2015-01-12
* STM: fix handling of side effects in vio2voGravatar Enrico Tassi2015-01-09
* Hook when state arrives on master.Gravatar Enrico Tassi2015-01-07
* rename: vi -> vioGravatar Enrico Tassi2015-01-06
* STM: Make assert unneeded (Close 3898)Gravatar Enrico Tassi2015-01-04
* STM: check with the kernel proof terms on the worker tooGravatar Enrico Tassi2014-12-27
* STM: fix processing of errorsGravatar Enrico Tassi2014-12-27
* STM: module Pp is openGravatar Enrico Tassi2014-12-27
* STM: do not call process_error twice (Close: 3880)Gravatar Enrico Tassi2014-12-26
* STM: remove dead codeGravatar Enrico Tassi2014-12-26
* STM: cleanup code for AdmittedGravatar Enrico Tassi2014-12-23
* Vi2vo: fix handling of univ constraints coming from the bodyGravatar Enrico Tassi2014-12-23
* STM: resilient on errors in non delegated proofsGravatar Enrico Tassi2014-12-17
* STM: rename and simplify flagsGravatar Enrico Tassi2014-12-17
* STM: simplify state managementGravatar Enrico Tassi2014-12-17
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
* Improving e11854569b8 on when to print goals in coqtop mode.Gravatar Hugo Herbelin2014-12-07
* Trying a new policy for when to automatically print goals (grantingGravatar Hugo Herbelin2014-12-04
* fix compilation on ocaml 3.12 (Close: 3833)Gravatar Enrico Tassi2014-11-28
* STM: if a-p-always-delegate fetch states from parked worker on edit-atGravatar Enrico Tassi2014-11-28
* STM: hook called whenever a state is unreachableGravatar Enrico Tassi2014-11-27
* async_queries_* merged with async_proofs_*Gravatar Enrico Tassi2014-11-27
* AsyncTaskQueue: parsin can also happen in the workers nowGravatar Enrico Tassi2014-11-27
* STM: new API async_queryGravatar Enrico Tassi2014-11-27
* STM: put hooks in key events to let plugins customize the feedbackGravatar Enrico Tassi2014-11-27
* Feedback: API cleaned up, documented and made user extensibleGravatar Enrico Tassi2014-11-27
* STM: code refactoringGravatar Enrico Tassi2014-11-03
* STM: fix printing of goals when on a tty interfaceGravatar Enrico Tassi2014-11-03
* Fix error reporting id on VtUnknown commandsGravatar Enrico Tassi2014-11-03
* Add [Info] command.Gravatar Arnaud Spiwack2014-11-01
* Feedback message: hold extra info to help routingGravatar Enrico Tassi2014-10-31
* STM: new worker for queriesGravatar Enrico Tassi2014-10-31
* STM: reorganize code and file namesGravatar Enrico Tassi2014-10-31
* Fixes for PG (Close 3763, 3770)Gravatar Enrico Tassi2014-10-27
* Goal printing made uniform: always done in STM (close 3585)Gravatar Enrico Tassi2014-10-22
* Goal: remove most of the API (make [Goal.goal] concrete).Gravatar Arnaud Spiwack2014-10-16
* Fix -async-proofs-always-delegate (close 3740)Gravatar Enrico Tassi2014-10-15
* Stm: more precise representation of nested proofsGravatar Enrico Tassi2014-10-13
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 20:55:57 +0000