diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-11-23 11:38:55 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-20 16:52:43 +0100 |
| commit | 28d45c2413ad24c758fca5cfb00ec4ba20935f39 (patch) | |
| tree | 50f60424aac3c9e898bb9f9192416c58f44aa7b6 /dev/base_include | |
| parent | e2d1c676b23a335b4fb8a528c99dfca2b82a1a39 (diff) | |
Separate vernac controls and regular commands.
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.
Diffstat (limited to 'dev/base_include')
| -rw-r--r-- | dev/base_include | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/base_include b/dev/base_include index d7059fe74..4dc9a0bee 100644 --- a/dev/base_include +++ b/dev/base_include @@ -193,7 +193,7 @@ let qid = Libnames.qualid_of_string;; (* parsing of terms *) let parse_constr = Pcoq.parse_string Pcoq.Constr.constr;; -let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac;; +let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac_control;; let parse_tac = API.Pcoq.parse_string Ltac_plugin.Pltac.tactic;; (* build a term of type glob_constr without type-checking or resolution of |