4 files changed, 17 insertions, 12 deletions
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 740e955049..7d917c58fe 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -48,8 +48,6 @@ type rewrite_attributes = { polymorphic : bool; program : bool; global : bool }
 let rewrite_attributes =
   let open Attributes.Notations in
   Attributes.(polymorphic ++ program ++ locality) >>= fun ((polymorphic, program), locality) ->
-  let polymorphic = Option.default (Flags.is_universe_polymorphism()) polymorphic in
-  let program = Option.default (Flags.is_program_mode ()) program in
   let global = not (Locality.make_section_locality locality) in
   Attributes.Notations.return { polymorphic; program; global }
 
diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index 12968cccae..389441356e 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -128,7 +128,11 @@ let qualify_attribute qual (parser:'a attribute) : 'a attribute =
 
 let polymorphic_base = bool_attribute ~name:"Polymorphism" ~on:"polymorphic" ~off:"monomorphic"
 
-let program = bool_attribute ~name:"Program mode" ~on:"program" ~off:"noprogram"
+let program_opt = bool_attribute ~name:"Program mode" ~on:"program" ~off:"noprogram"
+
+let program = program_opt >>= function
+  | Some b -> return b
+  | None -> return (Flags.is_program_mode())
 
 let locality = bool_attribute ~name:"Locality" ~on:"local" ~off:"global"
 
@@ -154,6 +158,10 @@ let polymorphic_nowarn =
   universe_transform ~warn_unqualified:false >>
   qualify_attribute ukey polymorphic_base
 
+let polymorphic_base = polymorphic_base >>= function
+  | Some b -> return b
+  | None -> return (Flags.is_universe_polymorphism())
+
 let universe_poly_template =
   let template = bool_attribute ~name:"Template" ~on:"template" ~off:"notemplate" in
   universe_transform ~warn_unqualified:true >>
@@ -184,15 +192,11 @@ let attributes_of_flags f =
   let ((locality, deprecated), (polymorphic, template)), program =
     parse (locality ++ deprecation ++ universe_poly_template ++ program) f
   in
-  let polymorphic = Option.default (Flags.is_universe_polymorphism()) polymorphic in
-  let program = Option.default (Flags.is_program_mode()) program in
   { polymorphic; program; locality; template; deprecated }
 
 let only_locality atts = parse locality atts
 
-let only_polymorphism atts =
-  let att = parse polymorphic atts in
-  Option.default (Flags.is_universe_polymorphism ()) att
+let only_polymorphism atts = parse polymorphic atts
 
 
 let vernac_polymorphic_flag = ukey, VernacFlagList ["polymorphic", VernacFlagEmpty]
diff --git a/vernac/attributes.mli b/vernac/attributes.mli
index 7bd24a750b..7a75e9d922 100644
--- a/vernac/attributes.mli
+++ b/vernac/attributes.mli
@@ -38,15 +38,18 @@ type deprecation = { since : string option ; note : string option }
 
 val mk_deprecation : ?since: string option -> ?note: string option -> unit -> deprecation
 
-val polymorphic : bool option attribute
-val program : bool option attribute
-val universe_poly_template : (bool option * bool option) attribute
+val polymorphic : bool attribute
+val program : bool attribute
+val universe_poly_template : (bool * bool option) attribute
 val locality : bool option attribute
 val deprecation : deprecation option attribute
 
 val polymorphic_nowarn : bool option attribute
 (** For internal use, avoid warning if not qualified as eg [universes(polymorphic)]. *)
 
+val program_opt : bool option attribute
+(** For internal use when messing with the global option. *)
+
 type t = {
   locality : bool option;
   polymorphic : bool;
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index ac50afcf9b..3bdca0cc9f 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2402,7 +2402,7 @@ let interp ?(verbosely=true) ?proof ~st {CAst.loc;v=c} =
 
     | c ->
       let poly, program = let open Attributes in
-        parse_drop_extra Notations.(polymorphic_nowarn ++ program) atts
+        parse_drop_extra Notations.(polymorphic_nowarn ++ program_opt) atts
       in
       (* NB: we keep polymorphism and program in the attributes, we're
          just parsing them to do our option magic. *)