diff options
| author | Maxime Dénès | 2018-11-27 11:06:18 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-11-27 11:06:18 +0100 |
| commit | 31a1fa82bfc747df0c71c93346f689def876794a (patch) | |
| tree | fac54469054681647ab0659bdfeddcdb74eda4f9 /checker | |
| parent | 5fcf1b7dcd9b20ea7c5ad317ce2bfe4fbb5452d9 (diff) | |
| parent | ec209ea02cb8fa86f09aff88d0464c865ed7b8a5 (diff) | |
Merge PR #8986: Put -indices-matter in typing_flags
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/checker.ml | 15 | ||||
| -rw-r--r-- | checker/values.ml | 2 |
2 files changed, 11 insertions, 6 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|]|] |