From 032398fb5e2bc88e911f60ddfc4982a3826b55cd Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 19 Feb 2019 13:04:09 +0100
Subject: Make inductive cumulativity flag local to vernacentries

---
 vernac/vernacentries.ml | 15 ++++++---------
 1 file changed, 6 insertions(+), 9 deletions(-)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 6c4b0acd52..d511bcd4fd 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -609,6 +609,11 @@ let vernac_assumption ~atts discharge kind l nl =
   let status = ComAssumption.do_assumptions ~program_mode:atts.program kind nl l in
   if not status then Feedback.feedback Feedback.AddedAxiom
 
+let is_polymorphic_inductive_cumulativity =
+  declare_bool_option_and_ref ~depr:false ~value:false
+    ~name:"Polymorphic inductive cumulativity"
+    ~key:["Polymorphic"; "Inductive"; "Cumulativity"]
+
 let should_treat_as_cumulative cum poly =
   match cum with
   | Some VernacCumulative ->
@@ -617,7 +622,7 @@ let should_treat_as_cumulative cum poly =
   | Some VernacNonCumulative ->
     if poly then false
     else user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.")
-  | None -> poly && Flags.is_polymorphic_inductive_cumulativity ()
+  | None -> poly && is_polymorphic_inductive_cumulativity ()
 
 let get_uniform_inductive_parameters =
   Goptions.declare_bool_option_and_ref
@@ -1563,14 +1568,6 @@ let () =
       optread  = (fun () -> !Flags.raw_print);
       optwrite = (fun b -> Flags.raw_print := b) }
 
-let () =
-  declare_bool_option
-    { optdepr  = false;
-      optname  = "Polymorphic inductive cumulativity";
-      optkey   = ["Polymorphic"; "Inductive"; "Cumulativity"];
-      optread  = Flags.is_polymorphic_inductive_cumulativity;
-      optwrite = Flags.make_polymorphic_inductive_cumulativity }
-
 let () =
   declare_int_option
     { optdepr  = false;
-- 
cgit v1.2.3