From e181c9b043e64342c1e51763f4fe88c78bc4736d Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Wed, 16 Dec 2015 12:20:47 +0100 Subject: 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. --- intf/vernacexpr.mli | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) (limited to 'intf/vernacexpr.mli') 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: -- cgit v1.2.3