5 files changed, 32 insertions, 10 deletions
diff --git a/doc/sphinx/addendum/canonical-structures.rst b/doc/sphinx/addendum/canonical-structures.rst
index d81dafa4db..b593b0cef1 100644
--- a/doc/sphinx/addendum/canonical-structures.rst
+++ b/doc/sphinx/addendum/canonical-structures.rst
@@ -209,7 +209,7 @@ We need to define a new class that inherits from both ``EQ`` and ``LE``.
                         LE_class : LE.class T;
                         extra : mixin (EQ.Pack T EQ_class) (LE.cmp T LE_class) }.
 
-    Structure type := _Pack { obj : Type; #[not_canonical] class_of : class obj }.
+    Structure type := _Pack { obj : Type; #[canonical(false)] class_of : class obj }.
 
     Arguments Mixin {e le} _.
 
diff --git a/test-suite/success/attribute_syntax.v b/test-suite/success/attribute_syntax.v
index f4f59a3c16..4717759dec 100644
--- a/test-suite/success/attribute_syntax.v
+++ b/test-suite/success/attribute_syntax.v
@@ -20,6 +20,10 @@ Check ι _ ι.
 Fixpoint f (n: nat) {wf lt n} : nat := _.
 Reset f.
 
+#[program(true)]
+Fixpoint f (n: nat) {wf lt n} : nat := _.
+Reset f.
+
 #[deprecated(since="8.9.0")]
 Ltac foo := foo.
 
diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index 31b0b7e49a..1ad5862d5d 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -82,9 +82,12 @@ let assert_empty k v =
   if v <> VernacFlagEmpty
   then user_err Pp.(str "Attribute " ++ str k ++ str " does not accept arguments")
 
+let error_twice ~name : 'a =
+  user_err Pp.(str "Attribute for " ++ str name ++ str " specified twice.")
+
 let assert_once ~name prev =
   if Option.has_some prev then
-    user_err Pp.(str "Attribute for " ++ str name ++ str " specified twice.")
+    error_twice ~name
 
 let attribute_of_list (l:(string * 'a key_parser) list) : 'a option attribute =
   let rec p extra v = function
@@ -107,6 +110,24 @@ let bool_attribute ~name ~on ~off : bool option attribute =
   attribute_of_list [(on, single_key_parser ~name ~key:on true);
                (off, single_key_parser ~name ~key:off false)]
 
+(* Variant of the [bool] attribute with only two values (bool has three). *)
+let get_bool_value ~key ~default =
+  function
+  | VernacFlagEmpty -> default
+  | VernacFlagList [ "true", VernacFlagEmpty ] -> true
+  | VernacFlagList [ "false", VernacFlagEmpty ] -> false
+  | _ -> user_err Pp.(str "Attribute " ++ str key ++ str " only accepts boolean values.")
+
+let enable_attribute ~key ~default : bool attribute =
+  fun atts ->
+  let default = default () in
+  let this, extra = List.partition (fun (k, _) -> String.equal key k) atts in
+  extra,
+  match this with
+  | [] -> default
+  | [ _, value ] -> get_bool_value ~key ~default:true value
+  | _ -> error_twice ~name:key
+
 let qualify_attribute qual (parser:'a attribute) : 'a attribute =
   fun atts ->
     let rec extract extra qualified = function
@@ -139,11 +160,8 @@ let () = let open Goptions in
       optread  = (fun () -> !program_mode);
       optwrite = (fun b -> program_mode:=b) }
 
-let program_opt = bool_attribute ~name:"Program mode" ~on:"program" ~off:"noprogram"
-
-let program = program_opt >>= function
-  | Some b -> return b
-  | None -> return (!program_mode)
+let program =
+  enable_attribute ~key:"program" ~default:(fun () -> !program_mode)
 
 let locality = bool_attribute ~name:"Locality" ~on:"local" ~off:"global"
 
@@ -221,4 +239,4 @@ let vernac_polymorphic_flag = ukey, VernacFlagList ["polymorphic", VernacFlagEmp
 let vernac_monomorphic_flag = ukey, VernacFlagList ["monomorphic", VernacFlagEmpty]
 
 let canonical =
-  bool_attribute ~name:"Canonical projection" ~on:"canonical" ~off:"not_canonical"
+  enable_attribute ~key:"canonical" ~default:(fun () -> true)
diff --git a/vernac/attributes.mli b/vernac/attributes.mli
index 2559941354..44688ddafc 100644
--- a/vernac/attributes.mli
+++ b/vernac/attributes.mli
@@ -52,7 +52,7 @@ val program : bool attribute
 val template : bool option attribute
 val locality : bool option attribute
 val deprecation : deprecation option attribute
-val canonical : bool option attribute
+val canonical : bool attribute
 
 val program_mode_option_name : string list
 (** For internal use when messing with the global option. *)
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index cc74121064..17675a15e1 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -451,7 +451,7 @@ GRAMMAR EXTEND Gram
   [ [ attr = LIST0 quoted_attributes ;
       bd = record_binder; rf_priority = OPT [ "|"; n = natural -> { n } ];
       rf_notation = decl_notation -> {
-      let rf_canonical = attr |> List.flatten |> parse canonical |> Option.default true in
+      let rf_canonical = attr |> List.flatten |> parse canonical in
       let rf_subclass, rf_decl = bd in
       rf_decl, { rf_subclass ; rf_priority ; rf_notation ; rf_canonical } } ] ]
   ;