diff options
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/check.ml | 33 | ||||
| -rw-r--r-- | checker/checker.ml | 15 | ||||
| -rw-r--r-- | checker/mod_checking.ml | 8 | ||||
| -rw-r--r-- | checker/values.ml | 3 |
4 files changed, 22 insertions, 37 deletions
diff --git a/checker/check.ml b/checker/check.ml index e3a4bda8ec..30437e8bd0 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -136,36 +136,9 @@ type logical_path = DirPath.t let load_paths = ref ([],[] : CUnix.physical_path list * logical_path list) -(* Hints to partially detects if two paths refer to the same repertory *) -let rec remove_path_dot p = - let curdir = Filename.concat Filename.current_dir_name "" in (* Unix: "./" *) - let n = String.length curdir in - if String.length p > n && String.sub p 0 n = curdir then - remove_path_dot (String.sub p n (String.length p - n)) - else - p - -let strip_path p = - let cwd = Filename.concat (Sys.getcwd ()) "" in (* Unix: "`pwd`/" *) - let n = String.length cwd in - if String.length p > n && String.sub p 0 n = cwd then - remove_path_dot (String.sub p n (String.length p - n)) - else - remove_path_dot p - -let canonical_path_name p = - let current = Sys.getcwd () in - try - Sys.chdir p; - let p' = Sys.getcwd () in - Sys.chdir current; - p' - with Sys_error _ -> - (* We give up to find a canonical name and just simplify it... *) - strip_path p let find_logical_path phys_dir = - let phys_dir = canonical_path_name phys_dir in + let phys_dir = CUnix.canonical_path_name phys_dir in let physical, logical = !load_paths in match List.filter2 (fun p d -> p = phys_dir) physical logical with | _,[dir] -> dir @@ -180,14 +153,14 @@ let add_load_path (phys_path,coq_path) = if !Flags.debug then Feedback.msg_notice (str "path: " ++ pr_dirpath coq_path ++ str " ->" ++ spc() ++ str phys_path); - let phys_path = canonical_path_name phys_path in + let phys_path = CUnix.canonical_path_name phys_path in let physical, logical = !load_paths in match List.filter2 (fun p d -> p = phys_path) physical logical with | _,[dir] -> if coq_path <> dir (* If this is not the default -I . to coqtop *) && not - (phys_path = canonical_path_name Filename.current_dir_name + (phys_path = CUnix.canonical_path_name Filename.current_dir_name && coq_path = default_root_prefix) then begin 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/mod_checking.ml b/checker/mod_checking.ml index 77f4cea0c6..b83fe831bb 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -19,7 +19,13 @@ let check_constant_declaration env kn cb = | Monomorphic_const ctx -> false, push_context_set ~strict:true ctx env | Polymorphic_const auctx -> let ctx = Univ.AUContext.repr auctx in - true, push_context ~strict:false ctx env + let env = push_context ~strict:false ctx env in + true, env + in + let env' = match cb.const_private_poly_univs, (cb.const_body, poly) with + | None, _ -> env' + | Some local, (OpaqueDef _, true) -> push_subgraph local env' + | Some _, _ -> assert false in let ty = cb.const_type in let _ = infer_type env' ty in diff --git a/checker/values.ml b/checker/values.ml index 0de8a3e03f..dcb2bca81a 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|]|] @@ -227,6 +227,7 @@ let v_cb = v_tuple "constant_body" v_constr; Any; v_const_univs; + Opt v_context_set; v_bool; v_typing_flags|] |