From ec209ea02cb8fa86f09aff88d0464c865ed7b8a5 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 13 Nov 2018 16:02:03 +0100
Subject: Put -indices-matter in typing_flags

---
 checker/checker.ml | 15 ++++++++++-----
 checker/values.ml  |  2 +-
 2 files changed, 11 insertions(+), 6 deletions(-)

(limited to 'checker')

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|]|]
 
-- 
cgit v1.2.3