Universe Polymorphism is a normal attribute modulo the stm (no Flags)

4 files changed, 27 insertions, 28 deletions

diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index 14db90c3de..88638b295b 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -126,8 +126,6 @@ let qualify_attribute qual (parser:'a attribute) : 'a attribute =
     let extra = if rem = [] then extra else (qual, VernacFlagList rem) :: extra in
     extra, v
 
-let polymorphic_base = bool_attribute ~name:"Polymorphism" ~on:"polymorphic" ~off:"monomorphic"
-
 let program_opt = bool_attribute ~name:"Program mode" ~on:"program" ~off:"noprogram"
 
 let program = program_opt >>= function
@@ -154,14 +152,28 @@ let universe_transform ~warn_unqualified : unit attribute =
     in
     atts, ()
 
+let universe_polymorphism_option_name = ["Universe"; "Polymorphism"]
+let is_universe_polymorphism =
+  let b = ref false in
+  let _ = let open Goptions in
+    declare_bool_option
+      { optdepr  = false;
+        optname  = "universe polymorphism";
+        optkey   = universe_polymorphism_option_name;
+        optread  = (fun () -> !b);
+        optwrite = ((:=) b) }
+  in
+  fun () -> !b
+
+let polymorphic_base =
+  bool_attribute ~name:"Polymorphism" ~on:"polymorphic" ~off:"monomorphic" >>= function
+  | Some b -> return b
+  | None -> return (is_universe_polymorphism())
+
 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 >>
diff --git a/vernac/attributes.mli b/vernac/attributes.mli
index 27b873bfe0..c81082d5ad 100644
--- a/vernac/attributes.mli
+++ b/vernac/attributes.mli
@@ -47,9 +47,6 @@ 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. *)
 
@@ -127,3 +124,10 @@ val make_attribute : (vernac_flags -> vernac_flags * 'a) -> 'a attribute
 (** Compatibility values for parsing [Polymorphic]. *)
 val vernac_polymorphic_flag : vernac_flag
 val vernac_monomorphic_flag : vernac_flag
+
+(** For the stm, do not use! *)
+
+val polymorphic_nowarn : bool attribute
+(** For internal use, avoid warning if not qualified as eg [universes(polymorphic)]. *)
+val universe_polymorphism_option_name : string list
+val is_universe_polymorphism : unit -> bool
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 98ac4f1518..0970b6d0fb 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1491,16 +1491,6 @@ let _ =
       optread  = (fun () -> !Flags.program_mode);
       optwrite = (fun b -> Flags.program_mode:=b) }
 
-let universe_polymorphism_option_name = ["Universe"; "Polymorphism"]
-
-let _ =
-  declare_bool_option
-    { optdepr  = false;
-      optname  = "universe polymorphism";
-      optkey   = universe_polymorphism_option_name;
-      optread  = Flags.is_universe_polymorphism;
-      optwrite = Flags.make_universe_polymorphism }
-
 let _ =
   declare_bool_option
     { optdepr  = false;
@@ -2346,7 +2336,6 @@ let with_fail st b f =
   end
 
 let interp ?(verbosely=true) ?proof ~st {CAst.loc;v=c} =
-  let orig_univ_poly = Flags.is_universe_polymorphism () in
   let orig_program_mode = Flags.is_program_mode () in
   let rec control = function
   | VernacExpr (atts, v) ->
@@ -2368,12 +2357,11 @@ let interp ?(verbosely=true) ?proof ~st {CAst.loc;v=c} =
       vernac_load control fname
 
     | c ->
-      let poly, program = let open Attributes in
-        parse_drop_extra Notations.(polymorphic_nowarn ++ program_opt) atts
+      let program = let open Attributes in
+        parse_drop_extra program_opt atts
       in
       (* NB: we keep polymorphism and program in the attributes, we're
          just parsing them to do our option magic. *)
-      Option.iter Flags.make_universe_polymorphism poly;
       Option.iter Obligations.set_program_mode program;
       try
         vernac_timeout begin fun () ->
@@ -2384,8 +2372,6 @@ let interp ?(verbosely=true) ?proof ~st {CAst.loc;v=c} =
              we should not restore the previous state of the flag... *)
           if Option.has_some program then
             Flags.program_mode := orig_program_mode;
-          if Option.has_some poly then
-            Flags.make_universe_polymorphism orig_univ_poly;
           end
         with
         | reraise when
@@ -2396,7 +2382,6 @@ let interp ?(verbosely=true) ?proof ~st {CAst.loc;v=c} =
             let e = CErrors.push reraise in
             let e = locate_if_not_already ?loc e in
             let () = restore_timeout () in
-            Flags.make_universe_polymorphism orig_univ_poly;
             Flags.program_mode := orig_program_mode;
             iraise e
   in
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 3aa4ec12c0..8ccd121b8f 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -37,8 +37,6 @@ val command_focus : unit Proof.focus_kind
 val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr ->
   Evd.evar_map * Redexpr.red_expr) Hook.t
 
-val universe_polymorphism_option_name : string list
-
 (** {5 VERNAC EXTEND} *)
 
 type classifier = Genarg.raw_generic_argument list -> Vernacexpr.vernac_classification