From 4371ff2357c11d913b163dde193255f538f3565f Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Mon, 25 Jun 2018 09:35:25 +0000 Subject: [vernac] Generic syntax for flags/attributes --- vernac/vernacexpr.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'vernac/vernacexpr.ml') 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 -- cgit v1.2.3