index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
stm
/
stm.mli
Commit message (
Expand
)
Author
Age
*
Separate vernac controls and regular commands.
Maxime Dénès
2017-12-20
*
[flags] [stm] Reorganize flags.
Emilio Jesus Gallego Arias
2017-12-11
*
[plugins] Prepare plugin API for functional handling of state.
Emilio Jesus Gallego Arias
2017-11-19
*
[stm] Move interpretation state to Vernacentries
Emilio Jesus Gallego Arias
2017-10-17
*
[stm] [toplevel] Move delicate state initialization to the STM (BZ#5556)
Emilio Jesus Gallego Arias
2017-10-11
*
[stm] Switch to a functional API
Emilio Jesus Gallego Arias
2017-10-06
*
[stm] [flags] Move document mode flags to the STM.
Emilio Jesus Gallego Arias
2017-10-06
*
Add XML protocol support for Wait.
Maxime Dénès
2017-09-19
*
[ide] Add route_id parameter to query call.
Emilio Jesus Gallego Arias
2017-06-18
*
Merge branch 'trunk' into located_switch
Emilio Jesus Gallego Arias
2017-05-24
|
\
|
*
Remove unused [open] statements
Gaetan Gilbert
2017-04-27
*
|
[location] Remove Loc.ghost.
Emilio Jesus Gallego Arias
2017-04-25
|
/
*
[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-12
*
[stm] remove process_error_hook
Emilio Jesus Gallego Arias
2017-04-07
*
[stm] remove tactic_being_run hook
Emilio Jesus Gallego Arias
2017-04-07
*
[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
2017-02-15
*
[stm] Fix record field name clash.
Emilio Jesus Gallego Arias
2016-10-18
*
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-06
*
Move serialization functions out of Stm
Emilio Jesus Gallego Arias
2016-06-02
*
typos
Enrico Tassi
2016-05-23
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
*
Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.
Maxime Dénès
2016-01-15
*
|
CLEANUP: removing unnecessary wrapper
Matej Kosik
2016-01-11
|
/
*
Add a way to get the right fix_exn in external vernacular commands
Matthieu Sozeau
2015-10-30
*
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-09
*
STM: for PIDE based UIs, edit_at requires no Reach.known_state
Enrico Tassi
2015-10-08
*
Hook when state arrives on master.
Enrico Tassi
2015-01-07
*
rename: vi -> vio
Enrico Tassi
2015-01-06
*
STM: simplify state management
Enrico Tassi
2014-12-17
*
Getting rid of Exninfo hacks.
Pierre-Marie Pédrot
2014-12-16
*
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-27
*
STM: code refactoring
Enrico Tassi
2014-11-03
*
Feedback message: hold extra info to help routing
Enrico Tassi
2014-10-31
*
STM: new worker for queries
Enrico Tassi
2014-10-31
*
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-10-13
*
XML pretty printing for AST (work by François Poulain, project DoCoq)
Enrico Tassi
2014-09-29
*
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-05
*
STM: VtQuery holds the id of the state it refers to
Carst Tankink
2014-08-04
[next]