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 /printing | |
| 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 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 15 |
1 files changed, 5 insertions, 10 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index d79fb45618..0f065e251b 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -635,10 +635,10 @@ module Make else spc() ++ qs s ) - | VernacTime v -> - return (keyword "Time" ++ spc() ++ pr_vernac_list v) - | VernacRedirect (s, v) -> - return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_list v) + | VernacTime (_,v) -> + return (keyword "Time" ++ spc() ++ pr_vernac v) + | VernacRedirect (s, (_,v)) -> + return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac v) | VernacTimeout(n,v) -> return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac v) | VernacFail v -> @@ -1030,7 +1030,7 @@ module Make return (keyword "Cd" ++ pr_opt qs s) (* Commands *) - | VernacDeclareTacticDefinition (rc,l) -> + | VernacDeclareTacticDefinition l -> let pr_tac_body (id, redef, body) = let idl, body = match body with @@ -1262,11 +1262,6 @@ module Make | VernacEndSubproof -> return (str "}") - and pr_vernac_list l = - hov 2 (str"[" ++ spc() ++ - prlist (fun v -> pr_located pr_vernac v ++ sep_end (snd v) ++ fnl()) l - ++ spc() ++ str"]") - and pr_extend s cl = let pr_arg a = try pr_gen a |