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

8 files changed, 36 insertions, 45 deletions

diff --git a/lib/flags.ml b/lib/flags.ml
index c8f19f2f11..582506f3a8 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -103,10 +103,6 @@ let auto_intros = ref true
 let make_auto_intros flag = auto_intros := flag
 let is_auto_intros () = !auto_intros
 
-let universe_polymorphism = ref false
-let make_universe_polymorphism b = universe_polymorphism := b
-let is_universe_polymorphism () = !universe_polymorphism
-
 let polymorphic_inductive_cumulativity = ref false
 let make_polymorphic_inductive_cumulativity b = polymorphic_inductive_cumulativity := b
 let is_polymorphic_inductive_cumulativity () = !polymorphic_inductive_cumulativity
diff --git a/lib/flags.mli b/lib/flags.mli
index 3d9eafde75..b667235678 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -84,10 +84,6 @@ val is_auto_intros : unit -> bool
 val program_mode : bool ref
 val is_program_mode : unit -> bool
 
-(** Global universe polymorphism flag. *)
-val make_universe_polymorphism : bool -> unit
-val is_universe_polymorphism : unit -> bool
-
 (** Global polymorphic inductive cumulativity flag. *)
 val make_polymorphic_inductive_cumulativity : bool -> unit
 val is_polymorphic_inductive_cumulativity : unit -> bool
diff --git a/stm/stm.ml b/stm/stm.ml
index 07049815ef..cfadada104 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2133,7 +2133,7 @@ and Reach : sig
 end = struct (* {{{ *)
 
 let async_policy () =
-  if Flags.is_universe_polymorphism () then false
+  if Attributes.is_universe_polymorphism () then false
   else if VCS.is_interactive () = `Yes then
     (async_proofs_is_master !cur_opt || !cur_opt.async_proofs_mode = APonLazy)
   else
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index f3961327d8..c93487d377 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -50,7 +50,7 @@ let idents_of_name : Names.Name.t -> Names.Id.t list =
 let stm_allow_nested_proofs_option_name = ["Nested";"Proofs";"Allowed"]
 
 let options_affecting_stm_scheduling =
-  [ Vernacentries.universe_polymorphism_option_name;
+  [ Attributes.universe_polymorphism_option_name;
     stm_allow_nested_proofs_option_name ]
 
 let classify_vernac e =
@@ -192,15 +192,15 @@ let classify_vernac e =
         try Vernacentries.get_vernac_classifier s l
         with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".")
   in
-  let rec static_control_classifier ~poly = function
+  let rec static_control_classifier = function
     | VernacExpr (f, e) ->
-      let poly' = Attributes.(parse_drop_extra polymorphic_nowarn f) in
-      static_classifier ~poly:(Option.default poly poly') e
-    | VernacTimeout (_,e) -> static_control_classifier ~poly e
+      let poly = Attributes.(parse_drop_extra polymorphic_nowarn f) in
+      static_classifier ~poly e
+    | VernacTimeout (_,e) -> static_control_classifier e
     | VernacTime (_,{v=e}) | VernacRedirect (_, {v=e}) ->
-       static_control_classifier ~poly e
+       static_control_classifier e
     | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
-        (match static_control_classifier ~poly e with
+        (match static_control_classifier e with
         | ( VtQuery | VtProofStep _ | VtSideff _
           | VtProofMode _ | VtMeta), _ as x -> x
         | VtQed _, _ ->
@@ -208,7 +208,7 @@ let classify_vernac e =
             VtNow
         | (VtStartProof _ | VtUnknown), _ -> VtUnknown, VtNow)
   in
-  static_control_classifier ~poly:(Flags.is_universe_polymorphism ()) e
+  static_control_classifier e
 
 let classify_as_query = VtQuery, VtLater
 let classify_as_sideeff = VtSideff [], VtLater
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