diff options
| author | Maxime Dénès | 2017-12-22 15:55:01 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-12-22 15:55:01 +0100 |
| commit | 3e8ad7726320de5b954675026a4ae429c6c324a8 (patch) | |
| tree | 448ab6903267de8cd8bbc68cb3a35693561ec191 /intf | |
| parent | 2a056809bcd025ab59791e4f839c91c8361b77c4 (diff) | |
| parent | 28d45c2413ad24c758fca5cfb00ec4ba20935f39 (diff) | |
Merge PR #6318: Separate vernac controls and regular commands.
Diffstat (limited to 'intf')
| -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 c7a9db1cbc..a90e5501a5 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: |