index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
vernac
/
vernacstate.ml
Age
Commit message (
Expand
)
Author
2019-06-04
coqpp: add new ![] specifiers for structured proof interaction
Gaëtan Gilbert
2019-06-04
Proof_global: pass only 1 pstate when we don't want the proof stack
Gaëtan Gilbert
2019-03-27
[vernac] [stm] Tweak `with_fail` and hopefully fix the semantics.
Emilio Jesus Gallego Arias
2019-03-27
[vernac] Adapt to removal of imperative proof state.
Emilio Jesus Gallego Arias
2019-01-24
[STM] explicit handling of parsing states
Enrico Tassi
2018-12-21
Fix shallow flag in vernac state
Maxime Dénès
2018-12-13
Move shallow state logic to the function preparing state for workers
Maxime Dénès
2018-02-27
Update headers following #6543.
Théo Zimmermann
2017-12-04
[vernac] Couple of tweaks missing from previous PRs.
Emilio Jesus Gallego Arias
2017-11-29
[proof] [api] Rename proof types in preparation for functionalization.
Emilio Jesus Gallego Arias
2017-11-22
[plugin] Encapsulate modifiers to vernac commands.
Emilio Jesus Gallego Arias
2017-11-19
[plugins] Prepare plugin API for functional handling of state.
Emilio Jesus Gallego Arias
