index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
stm
/
stm.mli
Age
Commit message (
Expand
)
Author
2017-05-24
Merge branch 'trunk' into located_switch
Emilio Jesus Gallego Arias
2017-04-27
Remove unused [open] statements
Gaetan 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_hook
Emilio Jesus Gallego Arias
2017-04-07
[stm] remove tactic_being_run hook
Emilio 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-06
STM: proof block detection made optional + simple test
Enrico Tassi
2016-06-06
STM: proof block detection/error resilience API
Enrico Tassi
2016-06-06
STM: invalid states are first class citizens
Enrico Tassi
2016-06-02
Move serialization functions out of Stm
Emilio Jesus Gallego Arias
2016-05-23
typos
Enrico Tassi
2016-01-21
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-15
Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.
Maxime Dénès
2016-01-11
CLEANUP: removing unnecessary wrapper
Matej Kosik
2015-10-30
Add a way to get the right fix_exn in external vernacular commands
Matthieu Sozeau
2015-10-09
STM: Added functions for saving and restoring the internal state
Alec Faithfull
2015-10-09
STM: Pass exception information to unreachable_state_hook functions
Alec Faithfull
2015-10-08
STM: for PIDE based UIs, edit_at requires no Reach.known_state
Enrico Tassi
2015-01-07
Hook when state arrives on master.
Enrico Tassi
2015-01-06
rename: vi -> vio
Enrico Tassi
2014-12-17
STM: simplify state management
Enrico Tassi
2014-12-16
Getting rid of Exninfo hacks.
Pierre-Marie Pédrot
2014-11-27
STM: hook called whenever a state is unreachable
Enrico Tassi
2014-11-27
AsyncTaskQueue: parsin can also happen in the workers now
Enrico Tassi
2014-11-27
STM: new API async_query
Enrico Tassi
2014-11-27
STM: put hooks in key events to let plugins customize the feedback
Enrico Tassi
2014-11-03
STM: code refactoring
Enrico Tassi
2014-10-31
Feedback message: hold extra info to help routing
Enrico Tassi
2014-10-31
STM: new worker for queries
Enrico Tassi
2014-10-13
STM: primitives to snapshot a .vi while in interactive mode
Enrico Tassi
2014-10-13
library/opaqueTables: enable their use in interactive mode
Enrico Tassi
2014-09-29
XML pretty printing for AST (work by François Poulain, project DoCoq)
Enrico Tassi
2014-08-05
STM: new "par:" goal selector, like "all:" but in parallel
Enrico Tassi
2014-08-05
STM: code restructured to reuse task queue for tactics
Enrico Tassi
2014-08-04
STM: VtQuery holds the id of the state it refers to
Carst Tankink
2014-07-11
STM: add optionally takes the id of the new tip
Enrico Tassi
2014-07-11
STM: export the observe function (useful for pide)
Enrico Tassi
2014-06-25
all coqide specific files moved into ide/
Enrico Tassi
2014-04-25
Adding a stm/ folder, as asked during last workgroup. It was essentially moving
Pierre-Marie Pédrot
[prev]