Put -indices-matter in typing_flags

16 files changed, 51 insertions, 29 deletions

diff --git a/checker/checker.ml b/checker/checker.ml
index 346ae5fffb..da6a61de1c 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -138,13 +138,16 @@ let set_debug () = Flags.debug := true
 
 let impredicative_set = ref Declarations.PredicativeSet
 let set_impredicative_set () = impredicative_set := Declarations.ImpredicativeSet
-let engage = Safe_typing.set_engagement (!impredicative_set)
 
-let disable_compilers senv =
+let indices_matter = ref false
+
+let make_senv () =
+  let senv = Safe_typing.empty_environment in
+  let senv = Safe_typing.set_engagement !impredicative_set senv in
+  let senv = Safe_typing.set_indices_matter !indices_matter senv in
   let senv = Safe_typing.set_VM false senv in
   Safe_typing.set_native_compiler false senv
 
-
 let admit_list = ref ([] : object_file list)
 let add_admit s =
   admit_list := path_of_string s :: !admit_list
@@ -318,6 +321,9 @@ let parse_args argv =
     | "-impredicative-set" :: rem ->
       set_impredicative_set (); parse rem
 
+    | "-indices-matter" :: rem ->
+      indices_matter:=true; parse rem
+
     | "-coqlib" :: s :: rem ->
       if not (exists_dir s) then 
 	fatal_error (str "Directory '" ++ str s ++ str "' does not exist") false;
@@ -377,8 +383,7 @@ let init_with_argv argv =
     Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x));
     Flags.if_verbose print_header ();
     init_load_path ();
-    let senv = Safe_typing.empty_environment in
-    disable_compilers (engage senv)
+    make_senv ()
   with e ->
     fatal_error (str "Error during initialization :" ++ (explain_exn e)) (is_anomaly e)
 
diff --git a/checker/values.ml b/checker/values.ml
index 0de8a3e03f..628089433a 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -217,7 +217,7 @@ let v_cst_def =
     [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]|]
 
 let v_typing_flags =
-  v_tuple "typing_flags" [|v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool|]
+  v_tuple "typing_flags" [|v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool|]
 
 let v_const_univs = v_sum "constant_universes" 0 [|[|v_context_set|]; [|v_abs_context|]|]
 
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
diff --git a/library/global.ml b/library/global.ml
index 4ea5969a6f..67b00cf411 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -88,6 +88,7 @@ let add_constraints c = globalize0 (Safe_typing.add_constraints c)
 let push_context_set b c = globalize0 (Safe_typing.push_context_set b c)
 
 let set_engagement c = globalize0 (Safe_typing.set_engagement c)
+let set_indices_matter b = globalize0 (Safe_typing.set_indices_matter b)
 let set_typing_flags c = globalize0 (Safe_typing.set_typing_flags c)
 let typing_flags () = Environ.typing_flags (env ())
 let export_private_constants ~in_section cd = globalize (Safe_typing.export_private_constants ~in_section cd)
diff --git a/library/global.mli b/library/global.mli
index 01ee695c49..40962e21af 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -29,6 +29,7 @@ val named_context : unit -> Constr.named_context
 
 (** Changing the (im)predicativity of the system *)
 val set_engagement : Declarations.engagement -> unit
+val set_indices_matter : bool -> unit
 val set_typing_flags : Declarations.typing_flags -> unit
 val typing_flags : unit -> Declarations.typing_flags
 
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 15411d55d0..4d2b657b3c 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -64,6 +64,7 @@ type coq_cmdopts = {
   color : color;
 
   impredicative_set : Declarations.set_predicativity;
+  indices_matter : bool;
   enable_VM : bool;
   enable_native_compiler : bool;
   stm_flags   : Stm.AsyncOpts.stm_opt;
@@ -118,6 +119,7 @@ let init_args = {
   color = `AUTO;
 
   impredicative_set = Declarations.PredicativeSet;
+  indices_matter = false;
   enable_VM = true;
   enable_native_compiler = Coq_config.native_compiler;
   stm_flags    = Stm.AsyncOpts.default_opts;
@@ -565,7 +567,7 @@ let parse_args arglist : coq_cmdopts * string list =
     |"-filteropts" -> { oval with filter_opts = true }
     |"-impredicative-set" ->
       { oval with impredicative_set = Declarations.ImpredicativeSet }
-    |"-indices-matter" -> Indtypes.enforce_indices_matter (); oval
+    |"-indices-matter" -> { oval with indices_matter = true }
     |"-m"|"--memory" -> { oval with memory_stat = true }
     |"-noinit"|"-nois" -> { oval with load_init = false }
     |"-no-glob"|"-noglob" -> Dumpglob.noglob (); { oval with glob_opt = true }
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
index b709788dde..18ab6c3153 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -43,6 +43,7 @@ type coq_cmdopts = {
   color : color;
 
   impredicative_set : Declarations.set_predicativity;
+  indices_matter : bool;
   enable_VM : bool;
   enable_native_compiler : bool;
   stm_flags   : Stm.AsyncOpts.stm_opt;
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 66af7f7cdf..1b72a9554e 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -435,6 +435,7 @@ let init_toplevel custom_init arglist =
       Flags.if_verbose print_header ();
       Mltop.init_known_plugins ();
       Global.set_engagement opts.impredicative_set;
+      Global.set_indices_matter opts.indices_matter;
       Global.set_VM opts.enable_VM;
       Global.set_native_compiler opts.enable_native_compiler;
 
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index fbfa997555..8507ee6e2c 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -266,7 +266,7 @@ let inductive_levels env evd poly arities inds =
         in
         let minlev =
           (** Indices contribute. *)
-          if Indtypes.is_indices_matter () && List.length ctx > 0 then (
+          if indices_matter env && List.length ctx > 0 then (
             let ilev = sign_level env evd ctx in
               Univ.sup ilev minlev)
           else minlev