aboutsummaryrefslogtreecommitdiff
path: root/stm
AgeCommit message (Expand)Author
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
2014-11-27STM: put hooks in key events to let plugins customize the feedbackEnrico Tassi
2014-11-27Feedback: API cleaned up, documented and made user extensibleEnrico Tassi
2014-11-09new: Optimize Proof, Optimize HeapEnrico Tassi
2014-11-03vernac_classifier: VernacDeclareTacticDefinition does not alter the parserEnrico Tassi
2014-11-03STM: code refactoringEnrico Tassi
2014-11-03STM: fix printing of goals when on a tty interfaceEnrico Tassi
2014-11-03Fix error reporting id on VtUnknown commandsEnrico Tassi
2014-11-01Add [Info] command.Arnaud Spiwack
2014-10-31Feedback message: hold extra info to help routingEnrico Tassi
2014-10-31STM: new worker for queriesEnrico Tassi
2014-10-31STM: reorganize code and file namesEnrico Tassi
2014-10-30Fix backtracking issue in Defined (Close 3780)Enrico Tassi
2014-10-27Fixes for PG (Close 3763, 3770)Enrico Tassi
2014-10-25This commit introduces changes in induction and destruct.Hugo Herbelin
2014-10-22Goal printing made uniform: always done in STM (close 3585)Enrico Tassi
2014-10-22Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.Arnaud Spiwack
2014-10-16Goal: remove most of the API (make [Goal.goal] concrete).Arnaud Spiwack
2014-10-15Fix -async-proofs-always-delegate (close 3740)Enrico Tassi
2014-10-13Stm: more precise representation of nested proofsEnrico Tassi
2014-10-13STM: primitives to snapshot a .vi while in interactive modeEnrico Tassi
2014-10-13TQueue: new primitive to take a snapshot of the queueEnrico Tassi
2014-10-13STM: simplify how the term part of a side effect is retrievedEnrico Tassi
2014-10-13library/opaqueTables: enable their use in interactive modeEnrico Tassi
2014-10-01STM: report the (structured) goals as XMLCarst Tankink
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 17:10:25 +0000