diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-07-09 22:16:10 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-07-09 22:16:10 +0200 |
| commit | a4909dd5f8d5df773a361a7cbacefc392b7cfebd (patch) | |
| tree | 7f16c4018bad54d9c1bf7c9e9d4aefacd83b2e40 /vernac/vernacexpr.ml | |
| parent | c1d4dc68ace54f9ff9fd8f6466add38098ef0495 (diff) | |
| parent | 420b38cba7aedfcfeac5671a7db0c02c4bb14a0c (diff) | |
Merge PR #7920: Generic syntax for attributes
Diffstat (limited to 'vernac/vernacexpr.ml')
| -rw-r--r-- | vernac/vernacexpr.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index f5f37339c..e97cac818 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -459,13 +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 +type vernac_flags = (string * 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 |