diff options
| author | Vincent Laporte | 2017-12-11 16:17:39 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2017-12-29 14:10:58 +0000 |
| commit | 4cdb838ef260c12f59cb91915c78dc975bd4c157 (patch) | |
| tree | 808712b015eb26cdb88bde357aa4b677afd64d47 | |
| parent | 2d6e395dead61a49ede6208bc40e16b4b8e68ce4 (diff) | |
[vernac] Define types in order
| -rw-r--r-- | intf/vernacexpr.ml | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index 5106e513b9..ba8dd41826 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -314,6 +314,15 @@ type cumulative_inductive_parsing_flag = (** {6 The type of vernacular expressions} *) +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 vernac_expr = | VernacLoad of verbose_flag * string @@ -468,15 +477,6 @@ type 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 vernac_control = | VernacExpr of vernac_expr (* boolean is true when the `-time` batch-mode command line flag was set. |