8 files changed, 32 insertions, 21 deletions

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index c1b38b4156..94832726fe 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -61,13 +61,27 @@ type constant_universes =
     of a constant are tracked in their {!constant_body} so that they
     can be displayed to the user. *)
 type typing_flags = {
-  check_guarded : bool; (** If [false] then fixed points and co-fixed
-                            points are assumed to be total. *)
-  check_universes : bool; (** If [false] universe constraints are not checked *)
-  conv_oracle : Conv_oracle.oracle; (** Unfolding strategies for conversion *)
-  share_reduction : bool; (** Use by-need reduction algorithm *)
-  enable_VM : bool; (** If [false], all VM conversions fall back to interpreted ones *)
-  enable_native_compiler : bool; (** If [false], all native conversions fall back to VM ones *)
+  check_guarded : bool;
+  (** If [false] then fixed points and co-fixed points are assumed to
+      be total. *)
+
+  check_universes : bool;
+  (** If [false] universe constraints are not checked *)
+
+  conv_oracle : Conv_oracle.oracle;
+  (** Unfolding strategies for conversion *)
+
+  share_reduction : bool;
+  (** Use by-need reduction algorithm *)
+
+  enable_VM : bool;
+  (** If [false], all VM conversions fall back to interpreted ones *)
+
+  enable_native_compiler : bool;
+  (** If [false], all native conversions fall back to VM ones *)
+
+  indices_matter: bool;
+  (** The universe of an inductive type must be above that of its indices. *)
 }
 
 (* some contraints are in constant_constraints, some other may be in
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 3ed599c538..d1d184df69 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -24,6 +24,7 @@ let safe_flags oracle = {
   share_reduction = true;
   enable_VM = true;
   enable_native_compiler = true;
+  indices_matter = true;
 }
 
 (** {6 Arities } *)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 019c0a6819..7835a807ba 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -241,6 +241,8 @@ let is_impredicative_set env =
 let type_in_type env = not (typing_flags env).check_universes
 let deactivated_guard env = not (typing_flags env).check_guarded
 
+let indices_matter env = env.env_typing_flags.indices_matter
+
 let universes env = env.env_stratification.env_universes
 let named_context env = env.env_named_context.env_named_ctx
 let named_context_val env = env.env_named_context
@@ -389,6 +391,7 @@ let same_flags {
      check_guarded;
      check_universes;
      conv_oracle;
+     indices_matter;
      share_reduction;
      enable_VM;
      enable_native_compiler;
@@ -396,6 +399,7 @@ let same_flags {
   check_guarded == alt.check_guarded &&
   check_universes == alt.check_universes &&
   conv_oracle == alt.conv_oracle &&
+  indices_matter == alt.indices_matter &&
   share_reduction == alt.share_reduction &&
   enable_VM == alt.enable_VM &&
   enable_native_compiler == alt.enable_native_compiler
diff --git a/kernel/environ.mli b/kernel/environ.mli
index c285f907fc..91b28bfcbc 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -96,6 +96,7 @@ val typing_flags    : env -> typing_flags
 val is_impredicative_set : env -> bool
 val type_in_type : env -> bool
 val deactivated_guard : env -> bool
+val indices_matter : env -> bool
 
 (** is the local context empty *)
 val empty_context : env -> bool
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 20c90bc05a..a4a02791b4 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -35,14 +35,6 @@ env_ar_par = env_ar + declaration of parameters
 nmr = ongoing computation of recursive parameters
 *)
 
-(* Tell if indices (aka real arguments) contribute to size of inductive type *)
-(* If yes, this is compatible with the univalent model *)
-
-let indices_matter = ref false
-
-let enforce_indices_matter () = indices_matter := true
-let is_indices_matter () = !indices_matter
-
 (* [weaker_noccur_between env n nvars t] (defined above), checks that
    no de Bruijn indices between [n] and [n+nvars] occur in [t]. If
    some such occurrences are found, then reduction is performed
@@ -303,7 +295,7 @@ let typecheck_inductive env mie =
 	 let inflev = 
 	   (* The level of the inductive includes levels of indices if 
 	      in indices_matter mode *)
-	     if !indices_matter 
+             if indices_matter env
 	     then Some (cumulate_arity_large_levels env_params sign)
 	     else None
 	 in
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index a827c17683..840e23ed69 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -50,8 +50,3 @@ val check_positivity : chkpos:bool ->
 (** The following function does checks on inductive declarations. *)
 
 val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body
-
-(** The following enforces a system compatible with the univalent model *)
-
-val enforce_indices_matter : unit -> unit
-val is_indices_matter : unit -> bool
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 83d890b628..b7f1e93062 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -196,6 +196,9 @@ let set_typing_flags c senv =
   if env == senv.env then senv
   else { senv with env }
 
+let set_indices_matter indices_matter senv =
+  set_typing_flags { (Environ.typing_flags senv.env) with indices_matter } senv
+
 let set_share_reduction b senv =
   let flags = Environ.typing_flags senv.env in
   set_typing_flags { flags with share_reduction = b } senv
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 7af773e3bc..57b01f15e3 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -136,6 +136,7 @@ val add_constraints :
 
 (** Setting the type theory flavor *)
 val set_engagement : Declarations.engagement -> safe_transformer0
+val set_indices_matter : bool -> safe_transformer0
 val set_typing_flags : Declarations.typing_flags -> safe_transformer0
 val set_share_reduction : bool -> safe_transformer0
 val set_VM : bool -> safe_transformer0