aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/stm.mli
Commit message (Expand)AuthorAge
* Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\
| * Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
* | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
|/
* [stm] Port the toplevel to the STM.Gravatar Emilio Jesus Gallego Arias2017-04-12
* [stm] Move main parsing entry point to the STM.Gravatar Emilio Jesus Gallego Arias2017-04-12
* [stm] Remove edit_id.Gravatar Emilio Jesus Gallego Arias2017-04-12
* [stm] remove process_error_hookGravatar Emilio Jesus Gallego Arias2017-04-07
* [stm] remove tactic_being_run hookGravatar Emilio Jesus Gallego Arias2017-04-07
* [stm] Remove unused legacy stm interface.Gravatar Emilio Jesus Gallego Arias2017-02-15
* [stm] Reenable Show Script command.Gravatar Emilio Jesus Gallego Arias2017-02-15
* [stm] Break stm/toplevel dependency loop.Gravatar Emilio Jesus Gallego Arias2017-02-15
* [stm] Fix record field name clash.Gravatar Emilio Jesus Gallego Arias2016-10-18
* STM: proof block detection made optional + simple testGravatar Enrico Tassi2016-06-06
* STM: proof block detection/error resilience APIGravatar Enrico Tassi2016-06-06
* STM: invalid states are first class citizensGravatar Enrico Tassi2016-06-06
* Move serialization functions out of StmGravatar Emilio Jesus Gallego Arias2016-06-02
* typosGravatar Enrico Tassi2016-05-23
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.Gravatar Maxime Dénès2016-01-15
* | CLEANUP: removing unnecessary wrapperGravatar Matej Kosik2016-01-11
|/
* Add a way to get the right fix_exn in external vernacular commandsGravatar Matthieu Sozeau2015-10-30
* STM: Added functions for saving and restoring the internal stateGravatar Alec Faithfull2015-10-09
* STM: Pass exception information to unreachable_state_hook functionsGravatar Alec Faithfull2015-10-09
* STM: for PIDE based UIs, edit_at requires no Reach.known_stateGravatar Enrico Tassi2015-10-08
* Hook when state arrives on master.Gravatar Enrico Tassi2015-01-07
* rename: vi -> vioGravatar Enrico Tassi2015-01-06
* STM: simplify state managementGravatar Enrico Tassi2014-12-17
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
* STM: hook called whenever a state is unreachableGravatar 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
* STM: code refactoringGravatar Enrico Tassi2014-11-03
* Feedback message: hold extra info to help routingGravatar Enrico Tassi2014-10-31
* STM: new worker for queriesGravatar Enrico Tassi2014-10-31
* STM: primitives to snapshot a .vi while in interactive modeGravatar Enrico Tassi2014-10-13
* library/opaqueTables: enable their use in interactive modeGravatar Enrico Tassi2014-10-13
* XML pretty printing for AST (work by François Poulain, project DoCoq)Gravatar Enrico Tassi2014-09-29
* STM: new "par:" goal selector, like "all:" but in parallelGravatar Enrico Tassi2014-08-05
* STM: code restructured to reuse task queue for tacticsGravatar Enrico Tassi2014-08-05
* STM: VtQuery holds the id of the state it refers toGravatar Carst Tankink2014-08-04
* STM: add optionally takes the id of the new tipGravatar Enrico Tassi2014-07-11
* STM: export the observe function (useful for pide)Gravatar Enrico Tassi2014-07-11
* all coqide specific files moved into ide/Gravatar Enrico Tassi2014-06-25
* Adding a stm/ folder, as asked during last workgroup. It was essentially movingGravatar Pierre-Marie Pédrot2014-04-25
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 17:32:54 +0000