Simplify use of polymorphism/program globals in attributes

1 files changed, 10 insertions, 6 deletions

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]