diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-01-16 13:40:26 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-01-16 13:40:26 +0100 |
| commit | efea3760daed495ae072c6dcb258201d236425cc (patch) | |
| tree | 00540b4ce2de4e270bad11c8a51dd85cfa34a7df /intf | |
| parent | f4da0fe96c4784d89e8544e0273e1175f6a4de41 (diff) | |
| parent | ab8e47207245277cb5b92b80a92ae78ede5bfafe (diff) | |
Merge PR #6499: [vernac] Move the flags/attributes out of vernac_expr
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/vernacexpr.ml | 30 |
1 files changed, 15 insertions, 15 deletions
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index bc7b0585d..8bd2da2f1 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -314,7 +314,16 @@ type cumulative_inductive_parsing_flag = (** {6 The type of vernacular expressions} *) -type vernac_expr = +type vernac_implicit_status = Implicit | MaximallyImplicit | NotImplicit + +type vernac_argument_status = { + name : Name.t; + recarg_like : bool; + notation_scope : string Loc.located option; + implicit_status : vernac_implicit_status; +} + +type nonrec vernac_expr = | VernacLoad of verbose_flag * string (* Syntax *) @@ -463,22 +472,13 @@ type vernac_expr = (* For extension *) | VernacExtend of extend_name * Genarg.raw_generic_argument list - (* Flags *) - | VernacProgram of vernac_expr - | VernacPolymorphic of bool * vernac_expr - | VernacLocal of bool * vernac_expr - -and vernac_implicit_status = Implicit | MaximallyImplicit | NotImplicit - -and vernac_argument_status = { - name : Name.t; - recarg_like : bool; - notation_scope : string Loc.located option; - implicit_status : vernac_implicit_status; -} +type nonrec vernac_flag = + | VernacProgram + | VernacPolymorphic of bool + | VernacLocal of bool type vernac_control = - | VernacExpr of vernac_expr + | VernacExpr of vernac_flag list * vernac_expr (* boolean is true when the `-time` batch-mode command line flag was set. the flag is used to print differently in `-time` vs `Time foo` *) | VernacTime of bool * vernac_control located |