[attributes] Deprecate `attr(true)` syntax in favor of booelan attributes.

We introduce a warning so boolean attributes are expected to be of the
form `attr={yes,no}` or just `attr` (for `yes`).

We update the documentation, test-suite, and changelog.

3 files changed, 50 insertions, 19 deletions

diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index fd4fe3d47d..04b1f128d3 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -156,12 +156,20 @@ let legacy_bool_attribute ~name ~on ~off : bool option attribute =
      (off, single_key_parser ~name ~key:off false)]
 
 (* important note: we use on as the default for the new bool_attribute ! *)
+let deprecated_bool_attribute_warning =
+  CWarnings.create
+    ~name:"deprecated-attribute-syntax"
+    ~category:"parsing"
+    ~default:CWarnings.Enabled
+    (fun name ->
+       Pp.(str "Syntax for switching off boolean attributes has been updated, use " ++ str name ++ str "=no instead."))
+
 let deprecated_bool_attribute ~name ~on ~off : bool option attribute =
   bool_attribute ~name:on ++ legacy_bool_attribute ~name ~on ~off |> map (function
       | None, None ->
         None
       | None, Some v ->
-        (* Will insert deprecation warning *)
+        deprecated_bool_attribute_warning name;
         Some v
       | Some v, None -> Some v
       | Some v1, Some v2 ->
@@ -174,8 +182,16 @@ let deprecated_bool_attribute ~name ~on ~off : bool option attribute =
 let get_bool_value ~key ~default =
   function
   | VernacFlagEmpty -> default
-  | VernacFlagList [ "true", VernacFlagEmpty ] -> true
-  | VernacFlagList [ "false", VernacFlagEmpty ] -> false
+  | VernacFlagList [ "true", VernacFlagEmpty ] ->
+    deprecated_bool_attribute_warning key;
+    true
+  | VernacFlagList [ "false", VernacFlagEmpty ] ->
+    deprecated_bool_attribute_warning key;
+    false
+  | VernacFlagLeaf (FlagIdent "yes") ->
+    true
+  | VernacFlagLeaf (FlagIdent "no") ->
+    false
   | _ -> user_err Pp.(str "Attribute " ++ str key ++ str " only accepts boolean values.")
 
 let enable_attribute ~key ~default : bool attribute =
@@ -222,21 +238,37 @@ let () = let open Goptions in
 let program =
   enable_attribute ~key:"program" ~default:(fun () -> !program_mode)
 
-let locality =
-  deprecated_bool_attribute
-    ~name:"Locality"
-    ~on:"local" ~off:"global"
-
-let option_locality =
+(* This is a bit complex as the grammar in g_vernac.mlg doesn't
+   distingish between the boolean and ternary case.*)
+let option_locality_parser =
   let name = "Locality" in
   attribute_of_list [
-    ("local", single_key_parser ~name ~key:"local" Goptions.OptLocal);
-    ("global", single_key_parser ~name ~key:"global" Goptions.OptGlobal);
-    ("export", single_key_parser ~name ~key:"export" Goptions.OptExport);
-  ] >>= function
+    ("local", single_key_parser ~name ~key:"local" Goptions.OptLocal)
+  ; ("global", single_key_parser ~name ~key:"global" Goptions.OptGlobal)
+  ; ("export", single_key_parser ~name ~key:"export" Goptions.OptExport)
+  ]
+
+let option_locality =
+  option_locality_parser >>= function
   | None -> return Goptions.OptDefault
   | Some l -> return l
 
+(* locality is supposed to be true when local, false when global *)
+let locality =
+  let locality_to_bool =
+    function
+    | Goptions.OptLocal ->
+      true
+    | Goptions.OptGlobal ->
+      false
+    | Goptions.OptExport ->
+      CErrors.user_err Pp.(str "export attribute not supported here")
+    | Goptions.OptDefault ->
+      CErrors.user_err Pp.(str "default attribute not supported here")
+  in
+  option_locality_parser >>= function l ->
+    return (Option.map locality_to_bool l)
+
 let ukey = "universes"
 
 let universe_polymorphism_option_name = ["Universe"; "Polymorphism"]
@@ -287,7 +319,7 @@ let only_polymorphism atts = parse polymorphic atts
 
 
 let vernac_polymorphic_flag = ukey, VernacFlagList ["polymorphic", VernacFlagEmpty]
-let vernac_monomorphic_flag = ukey, VernacFlagList ["monomorphic", VernacFlagEmpty]
+let vernac_monomorphic_flag = ukey, VernacFlagList ["polymorphic", VernacFlagLeaf (FlagIdent "no")]
 
 let canonical_field =
   enable_attribute ~key:"canonical" ~default:(fun () -> true)
diff --git a/vernac/attributes.mli b/vernac/attributes.mli
index 60195fe790..03a14a03ff 100644
--- a/vernac/attributes.mli
+++ b/vernac/attributes.mli
@@ -88,7 +88,7 @@ val attribute_of_list : (string * 'a key_parser) list -> 'a option attribute
 (** Make an attribute from a list of key parsers together with their
    associated key. *)
 
-(** Define boolean attribute [name], of the form [name={on,off}]. The
+(** Define boolean attribute [name], of the form [name={yes,no}]. The
    attribute may only be set once for a command. *)
 val bool_attribute : name:string -> bool option attribute
 
@@ -99,9 +99,8 @@ val deprecated_bool_attribute
   -> bool option attribute
 (** Define boolean attribute [name] with will be set when [on] is
    provided and unset when [off] is provided. The attribute may only
-   be set once for a command; this attribute both accepts the old
-   [name(on)] [name(off)] and new attribute syntax, with [on] taken as
-   the key. *)
+   be set once for a command; this attribute both accepts the old [on]
+   [off] syntax and new attribute syntax [on=yes] [on=no] *)
 
 val qualify_attribute : string -> 'a attribute -> 'a attribute
 (** [qualified_attribute qual att] treats [#[qual(atts)]] like [att]
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index d9b664e243..116cfc6413 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -137,7 +137,7 @@ GRAMMAR EXTEND Gram
       | IDENT "Cumulative" ->
         { ("universes", VernacFlagList ["cumulative", VernacFlagEmpty]) }
       | IDENT "NonCumulative" ->
-        { ("universes", VernacFlagList ["noncumulative", VernacFlagEmpty]) }
+        { ("universes", VernacFlagList ["cumulative", VernacFlagLeaf (FlagIdent "no")]) }
       | IDENT "Private" ->
         { ("private", VernacFlagList ["matching", VernacFlagEmpty]) }
       | IDENT "Program" ->