1 files changed, 7 insertions, 10 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index fa1082473e..a157e01fc1 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -582,10 +582,15 @@ let should_treat_as_cumulative cum poly =
     else user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.")
   | None -> poly && Flags.is_polymorphic_inductive_cumulativity ()
 
-let uniform_inductive_parameters = ref false
+let get_uniform_inductive_parameters =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~name:"Uniform inductive parameters"
+    ~key:["Uniform"; "Inductive"; "Parameters"]
+    ~value:false
 
 let should_treat_as_uniform () =
-  if !uniform_inductive_parameters
+  if get_uniform_inductive_parameters ()
   then ComInductive.UniformParameters
   else ComInductive.NonUniformParameters
 
@@ -1538,14 +1543,6 @@ let () =
       optwrite = Flags.make_polymorphic_inductive_cumulativity }
 
 let () =
-  declare_bool_option
-    { optdepr  = false;
-      optname  = "Uniform inductive parameters";
-      optkey   = ["Uniform"; "Inductive"; "Parameters"];
-      optread  = (fun () -> !uniform_inductive_parameters);
-      optwrite = (fun b -> uniform_inductive_parameters := b) }
-
-let () =
   declare_int_option
     { optdepr  = false;
       optname  = "the level of inlining during functor application";