aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm
Commit message (Expand)AuthorAge
* Inlining Spawn.kill_if in the one place were it was actually used, thusGravatar Pierre-Marie Pédrot2014-12-25
* STM: cleanup code for AdmittedGravatar Enrico Tassi2014-12-23
* Vi2vo: fix handling of univ constraints coming from the bodyGravatar Enrico Tassi2014-12-23
* Proof using: New vernacular to name sets of section variablesGravatar Enrico Tassi2014-12-18
* Fix compilation with ocaml 4.0.0Gravatar Enrico Tassi2014-12-17
* STM: resilient on errors in non delegated proofsGravatar Enrico Tassi2014-12-17
* CoqIDE: cleanup jobs window on worker deathGravatar Enrico Tassi2014-12-17
* STM: rename and simplify flagsGravatar Enrico Tassi2014-12-17
* STM: simplify state managementGravatar Enrico Tassi2014-12-17
* AsyncTaskQueue: simpler model (no parking area, continuation tasks)Gravatar Enrico Tassi2014-12-17
* WorkerPool: simpler fuctor and no more parking areaGravatar Enrico Tassi2014-12-17
* TQueue: a way to unblock threads begin destroyed waiting on popGravatar Enrico Tassi2014-12-17
* Spawn: fix request of Gc statisticsGravatar Enrico Tassi2014-12-17
* CThread: use a different type for thread friendly in_channelsGravatar 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
* AsyncTaskQueue: API to park a workerGravatar Enrico Tassi2014-11-27
* WorkerPool: API to move a worker from an active pool to a parking oneGravatar Enrico Tassi2014-11-27
* TQueue: let reader be picky when popping an itemGravatar 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
* new: Optimize Proof, Optimize HeapGravatar Enrico Tassi2014-11-09
* vernac_classifier: VernacDeclareTacticDefinition does not alter the parserGravatar Enrico Tassi2014-11-03
* 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
* Fix backtracking issue in Defined (Close 3780)Gravatar Enrico Tassi2014-10-30
* Fixes for PG (Close 3763, 3770)Gravatar Enrico Tassi2014-10-27
* This commit introduces changes in induction and destruct.Gravatar Hugo Herbelin2014-10-25
* Goal printing made uniform: always done in STM (close 3585)Gravatar Enrico Tassi2014-10-22
* Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.Gravatar Arnaud Spiwack2014-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
* STM: primitives to snapshot a .vi while in interactive modeGravatar Enrico Tassi2014-10-13
* TQueue: new primitive to take a snapshot of the queueGravatar Enrico Tassi2014-10-13
* STM: simplify how the term part of a side effect is retrievedGravatar Enrico Tassi2014-10-13
* library/opaqueTables: enable their use in interactive modeGravatar Enrico Tassi2014-10-13
* STM: report the (structured) goals as XMLGravatar Carst Tankink2014-10-01
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 17:43:23 +0000