| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
| |
since it affects scheduling (actually the error the option lets one
silence)
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
| |
Virtually all classifications of vernacular commands (the STM
classifier, "filtered commands", "navigation commands", etc.) were
broken in presence of control vernaculars like Time, Timeout, Fail.
Funny examples of bugs include Time Abort All in coqtop or Time Set Ltac
Debug in CoqIDE.
This change introduces a type separation between vernacular controls and
vernacular commands, together with an "under_control" combinator.
|
| |
|
|
|
|
|
|
|
|
| |
The vernacular classifier has a current special case for "Undo" like
commands, as it needs access to the document structure in order to
produce the proper "VtBack" classification, however the classifier is
defined before the document is.
We introduce a new delegation status `VtMeta` that allows us to
interpreted such commands outside the classifier itself.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
| |
- drops all Defined entries from the evar map (applying the subst to the
initial evar and the undefined evars types).
- call Gc.compact
Now the question is: where should these two commands be documented?
|
| | |
|
|
|
files around. A bunch of files from lib/ that were only used in the STM were
moved, as well as part of toplevel/ related to the STM.
|
Enrico Tassi
Théo Zimmermann
Maxime Dénès
Emilio Jesus Gallego Arias
Pierre-Marie Pédrot