diff options
| author |  Vincent Laporte <Vincent.Laporte@gmail.com> | 2017-12-12 15:32:59 +0000 |
|---|---|---|
| committer | Vincent Laporte <Vincent.Laporte@gmail.com> | 2018-01-08 13:33:23 +0000 |
| commit | ab8e47207245277cb5b92b80a92ae78ede5bfafe (patch) | |
| tree | ec968b32532e3e8d67f9b7886853a288a43aac19 /intf | |
| parent | 557f017f2decd056cb04a6b87719a9d82c80a425 (diff) | |
[vernac] vernac_expr no longer recursive
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/vernacexpr.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index ba8dd4182..f35eab47f 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -323,7 +323,7 @@ type vernac_argument_status = { implicit_status : vernac_implicit_status; } -type vernac_expr = +type nonrec vernac_expr = | VernacLoad of verbose_flag * string (* Syntax *) @@ -472,13 +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 +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 |