[attributes] Allow boolean, single-value attributes.

Following discussion in https://github.com/coq/coq/pull/12586 , we
extend the syntax `val=string` to support also arbitrary values.

In particular we support boolean ones, or arbitrary key-pair lists.

This complements the current form `val="string"`, and makes more sense
in general.

Current syntax for the boolean version is `attr=yes` or `attr=no`, but
we could be more liberal if desired.

The general new guideline is that `foo(vals)` is reserved for
the case where `vals` is a list, whereas `foo=val` is for attributes
that allow a unique assignment.

This commit only introduces the support, next commits will migrate
some attributes to this new syntax and deprecate the old versions.

1 files changed, 1 insertions, 11 deletions

diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 442269ebda..4cee4f7a47 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -1331,20 +1331,10 @@ let pr_control_flag (p : control_flag) =
 
 let pr_vernac_control flags = Pp.prlist pr_control_flag flags
 
-let rec pr_vernac_flag (k, v) =
-  let k = keyword k in
-  let open Attributes in
-  match v with
-  | VernacFlagEmpty -> k
-  | VernacFlagLeaf v -> k ++ str " = " ++ qs v
-  | VernacFlagList m -> k ++ str "( " ++ pr_vernac_flags m ++ str " )"
-and pr_vernac_flags m =
-  prlist_with_sep (fun () -> str ", ") pr_vernac_flag m
-
 let pr_vernac_attributes =
   function
   | [] -> mt ()
-  | flags ->  str "#[" ++ pr_vernac_flags flags ++ str "]" ++ cut ()
+  | flags ->  str "#[" ++ prlist_with_sep pr_comma Attributes.pr_vernac_flag flags ++ str "]" ++ cut ()
 
 let pr_vernac ({v = {control; attrs; expr}} as v) =
   tag_vernac v