Add flag Uniform Inductive Parameters

1 files changed, 14 insertions, 1 deletions

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index e76921d1d..5fda1a0da 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -537,7 +537,12 @@ 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 should_treat_as_uniform () = ComInductive.NonUniformParameters (* TODO: Add a flag *)
+let uniform_inductive_parameters = ref false
+
+let should_treat_as_uniform () =
+  if !uniform_inductive_parameters
+  then ComInductive.UniformParameters
+  else ComInductive.NonUniformParameters
 
 let vernac_record cum k poly finite records =
   let is_cumulative = should_treat_as_cumulative cum poly in
@@ -1474,6 +1479,14 @@ 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";