diff options
| author |  Vincent Laporte <Vincent.Laporte@gmail.com> | 2018-06-25 09:35:25 +0000 |
|---|---|---|
| committer | Vincent Laporte <Vincent.Laporte@gmail.com> | 2018-07-03 16:06:00 +0000 |
| commit | 4371ff2357c11d913b163dde193255f538f3565f (patch) | |
| tree | 8ea3560c5d1010729cb1f51e01eabc36a22ce36d /vernac/vernacexpr.ml | |
| parent | 3c83ca8b3ea9ec3ea6656dc7f726c46a21729541 (diff) | |
[vernac] Generic syntax for flags/attributes
Diffstat (limited to 'vernac/vernacexpr.ml')
| -rw-r--r-- | vernac/vernacexpr.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 57ccb6006..2287630c7 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -459,14 +459,14 @@ type nonrec vernac_expr = (* For extension *) | VernacExtend of extend_name * Genarg.raw_generic_argument list -type nonrec vernac_flag = - | VernacProgram - | VernacPolymorphic of bool - | VernacLocal of bool - | VernacDeprecated of string * string (* Since, Note *) +type vernac_flags = (Names.Id.t * vernac_flag_value) list +and vernac_flag_value = + | VernacFlagEmpty + | VernacFlagLeaf of string + | VernacFlagList of vernac_flags type vernac_control = - | VernacExpr of vernac_flag list * vernac_expr + | VernacExpr of vernac_flags * 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 CAst.t |