diff options
| author | Matej Kosik | 2015-12-16 12:20:47 +0100 |
|---|---|---|
| committer | Matej Kosik | 2015-12-18 15:57:32 +0100 |
| commit | e181c9b043e64342c1e51763f4fe88c78bc4736d (patch) | |
| tree | 9dc9faf13b837b6be6704aee7a9241b0abcf5ba9 /parsing | |
| parent | 75d74cd7d124f244882b9c4ed200eac144dcbc43 (diff) | |
CLEANUP: Vernacexpr.vernac_expr
Originally, "VernacTime" and "VernacRedirect" were defined like this:
type vernac_expr =
...
| VernacTime of vernac_list
| VernacRedirect of string * vernac_list
...
where
type vernac_list = located_vernac_expr list
Currently, that list always contained one and only one element.
So I propose changing the definition of these two variants in the following way:
| VernacTime of located_vernac_expr
| VernacRedirect of string * located_vernac_expr
which covers all our current needs and enforces the invariant
related to the number of commands that are part of the
"VernacTime" and "VernacRedirect" variants.
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 1f9f57f698..975dee934f 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -89,8 +89,8 @@ let default_command_entry = GEXTEND Gram GLOBAL: vernac gallina_ext tactic_mode noedit_mode subprf subgoal_command; vernac: FIRST - [ [ IDENT "Time"; l = vernac_list -> VernacTime l - | IDENT "Redirect"; s = ne_string; l = vernac_list -> VernacRedirect (s, l) + [ [ IDENT "Time"; c = located_vernac -> VernacTime c + | IDENT "Redirect"; s = ne_string; c = located_vernac -> VernacRedirect (s, c) | IDENT "Timeout"; n = natural; v = vernac -> VernacTimeout(n,v) | IDENT "Fail"; v = vernac -> VernacFail v @@ -128,9 +128,6 @@ GEXTEND Gram | c = subprf -> c ] ] ; - vernac_list: - [ [ c = located_vernac -> [c] ] ] - ; vernac_aux: LAST [ [ prfcom = default_command_entry -> prfcom ] ] ; @@ -806,7 +803,7 @@ GEXTEND Gram command: [ [ IDENT "Ltac"; l = LIST1 tacdef_body SEP "with" -> - VernacDeclareTacticDefinition (true, l) + VernacDeclareTacticDefinition l | IDENT "Comments"; l = LIST0 comment -> VernacComments l |