aboutsummaryrefslogtreecommitdiff
path: root/stm/stm.mli
AgeCommit message (Expand)Author
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
2017-04-27Remove unused [open] statementsGaetan Gilbert
2017-04-25[location] Remove Loc.ghost.Emilio Jesus Gallego Arias
2017-04-12[stm] Port the toplevel to the STM.Emilio Jesus Gallego Arias
2017-04-12[stm] Move main parsing entry point to the STM.Emilio Jesus Gallego Arias
2017-04-12[stm] Remove edit_id.Emilio Jesus Gallego Arias
2017-04-07[stm] remove process_error_hookEmilio Jesus Gallego Arias
2017-04-07[stm] remove tactic_being_run hookEmilio Jesus Gallego Arias
2017-02-15[stm] Remove unused legacy stm interface.Emilio Jesus Gallego Arias
2017-02-15[stm] Reenable Show Script command.Emilio Jesus Gallego Arias
2017-02-15[stm] Break stm/toplevel dependency loop.Emilio Jesus Gallego Arias
2016-10-18[stm] Fix record field name clash.Emilio Jesus Gallego Arias
2016-06-06STM: proof block detection made optional + simple testEnrico Tassi
2016-06-06STM: proof block detection/error resilience APIEnrico Tassi
2016-06-06STM: invalid states are first class citizensEnrico Tassi
2016-06-02Move serialization functions out of StmEmilio Jesus Gallego Arias
2016-05-23typosEnrico Tassi
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-15Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.Maxime Dénès
2016-01-11CLEANUP: removing unnecessary wrapperMatej Kosik
2015-10-30Add a way to get the right fix_exn in external vernacular commandsMatthieu Sozeau
2015-10-09STM: Added functions for saving and restoring the internal stateAlec Faithfull
2015-10-09STM: Pass exception information to unreachable_state_hook functionsAlec Faithfull
2015-10-08STM: for PIDE based UIs, edit_at requires no Reach.known_stateEnrico Tassi
2015-01-07Hook when state arrives on master.Enrico Tassi
2015-01-06rename: vi -> vioEnrico Tassi
2014-12-17STM: simplify state managementEnrico Tassi
2014-12-16Getting rid of Exninfo hacks.Pierre-Marie Pédrot
2014-11-27STM: hook called whenever a state is unreachableEnrico Tassi
2014-11-27AsyncTaskQueue: parsin can also happen in the workers nowEnrico Tassi
2014-11-27STM: new API async_queryEnrico Tassi
2014-11-27STM: put hooks in key events to let plugins customize the feedbackEnrico Tassi
2014-11-03STM: code refactoringEnrico Tassi
2014-10-31Feedback message: hold extra info to help routingEnrico Tassi
2014-10-31STM: new worker for queriesEnrico Tassi
2014-10-13STM: primitives to snapshot a .vi while in interactive modeEnrico Tassi
2014-10-13library/opaqueTables: enable their use in interactive modeEnrico Tassi
2014-09-29XML pretty printing for AST (work by François Poulain, project DoCoq)Enrico Tassi
2014-08-05STM: new "par:" goal selector, like "all:" but in parallelEnrico Tassi
2014-08-05STM: code restructured to reuse task queue for tacticsEnrico Tassi
2014-08-04STM: VtQuery holds the id of the state it refers toCarst Tankink
2014-07-11STM: add optionally takes the id of the new tipEnrico Tassi
2014-07-11STM: export the observe function (useful for pide)Enrico Tassi
2014-06-25all coqide specific files moved into ide/Enrico Tassi
2014-04-25Adding a stm/ folder, as asked during last workgroup. It was essentially movingPierre-Marie Pédrot