diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2015-12-16 12:20:47 +0100 |
|---|---|---|
| committer | Matej Kosik <m4tej.kosik@gmail.com> | 2015-12-18 15:57:32 +0100 |
| commit | e181c9b043e64342c1e51763f4fe88c78bc4736d (patch) | |
| tree | 9dc9faf13b837b6be6704aee7a9241b0abcf5ba9 /intf/vernacexpr.mli | |
| 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 'intf/vernacexpr.mli')
| -rw-r--r-- | intf/vernacexpr.mli | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 99264dbe0..32c0f2975 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -287,8 +287,8 @@ type module_binder = bool option * lident list * module_ast_inl type vernac_expr = (* Control *) | VernacLoad of verbose_flag * string - | VernacTime of vernac_list - | VernacRedirect of string * vernac_list + | VernacTime of located_vernac_expr + | VernacRedirect of string * located_vernac_expr | VernacTimeout of int * vernac_expr | VernacFail of vernac_expr | VernacError of exn (* always fails *) @@ -386,8 +386,7 @@ type vernac_expr = | VernacBackTo of int (* Commands *) - | VernacDeclareTacticDefinition of - (rec_flag * (reference * bool * raw_tactic_expr) list) + | VernacDeclareTacticDefinition of (reference * bool * raw_tactic_expr) list | VernacCreateHintDb of string * bool | VernacRemoveHints of string list * reference list | VernacHints of obsolete_locality * string list * hints_expr @@ -455,8 +454,6 @@ type vernac_expr = | VernacPolymorphic of bool * vernac_expr | VernacLocal of bool * vernac_expr -and vernac_list = located_vernac_expr list - and located_vernac_expr = Loc.t * vernac_expr (* A vernac classifier has to tell if a command: |