diff options
Diffstat (limited to 'intf/vernacexpr.ml')
| -rw-r--r-- | intf/vernacexpr.ml | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index c7a9db1cb..a90e5501a 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -315,13 +315,8 @@ type cumulative_inductive_parsing_flag = (** {6 The type of vernacular expressions} *) type vernac_expr = - (* Control *) - | VernacLoad of verbose_flag * string - | VernacTime of vernac_expr located - | VernacRedirect of string * vernac_expr located - | VernacTimeout of int * vernac_expr - | VernacFail of vernac_expr + | VernacLoad of verbose_flag * string (* Syntax *) | VernacSyntaxExtension of bool * (lstring * syntax_modifier list) | VernacOpenCloseScope of bool * scope_name @@ -482,6 +477,14 @@ and vernac_argument_status = { implicit_status : vernac_implicit_status; } +type vernac_control = + | VernacExpr of vernac_expr + (* Control *) + | VernacTime of vernac_control located + | VernacRedirect of string * vernac_control located + | VernacTimeout of int * vernac_control + | VernacFail of vernac_control + (* A vernac classifier provides information about the exectuion of a command: |