diff options
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 43 |
1 files changed, 24 insertions, 19 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index ce05190b6f..e4b3fcbf1a 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -62,6 +62,8 @@ open Names open Declarations open Context.Named.Declaration +module NamedDecl = Context.Named.Declaration + (** {6 Safe environments } Fields of [safe_environment] : @@ -180,20 +182,17 @@ let set_engagement c senv = env = Environ.set_engagement c senv.env; engagement = Some c } +let set_typing_flags c senv = + { senv with env = Environ.set_typing_flags c senv.env } + (** Check that the engagement [c] expected by a library matches the current (initial) one *) -let check_engagement env (expected_impredicative_set,expected_type_in_type) = - let impredicative_set,type_in_type = Environ.engagement env in +let check_engagement env expected_impredicative_set = + let impredicative_set = Environ.engagement env in begin match impredicative_set, expected_impredicative_set with | PredicativeSet, ImpredicativeSet -> - Errors.error "Needs option -impredicative-set." - | _ -> () - end; - begin - match type_in_type, expected_type_in_type with - | StratifiedType, TypeInType -> - Errors.error "Needs option -type-in-type." + CErrors.error "Needs option -impredicative-set." | _ -> () end @@ -216,8 +215,8 @@ type private_constant_role = Term_typing.side_effect_role = | Schema of inductive * string let empty_private_constants = [] -let add_private x xs = x :: xs -let concat_private xs ys = xs @ ys +let add_private x xs = if List.mem_f Term_typing.equal_eff x xs then xs else x :: xs +let concat_private xs ys = List.fold_right add_private xs ys let mk_pure_proof = Term_typing.mk_pure_proof let inline_private_constants_in_constr = Term_typing.inline_side_effects let inline_private_constants_in_definition_entry = Term_typing.inline_entry_side_effects @@ -347,10 +346,10 @@ let check_required current_libs needed = try let actual = DPMap.find id current_libs in if not(digest_match ~actual ~required) then - Errors.error + CErrors.error ("Inconsistent assumptions over module "^(DirPath.to_string id)^".") with Not_found -> - Errors.error ("Reference to unknown module "^(DirPath.to_string id)^".") + CErrors.error ("Reference to unknown module "^(DirPath.to_string id)^".") in Array.iter check needed @@ -364,11 +363,11 @@ let check_required current_libs needed = cost too much. *) let safe_push_named d env = - let id = get_id d in + let id = NamedDecl.get_id d in let _ = try let _ = Environ.lookup_named id env in - Errors.error ("Identifier "^Id.to_string id^" already defined.") + CErrors.error ("Identifier "^Id.to_string id^" already defined.") with Not_found -> () in Environ.push_named d env @@ -797,7 +796,10 @@ type compiled_library = { type native_library = Nativecode.global list let get_library_native_symbols senv dir = - DPMap.find dir senv.native_symbols + try DPMap.find dir senv.native_symbols + with Not_found -> CErrors.user_err ~hdr:"get_library_native_symbols" + Pp.((str "Linker error in the native compiler. Are you using Require inside a nested Module declaration?") ++ fnl () ++ + (str "This use case is not supported, but disabling the native compiler may help.")) (** FIXME: MS: remove?*) let current_modpath senv = senv.modpath @@ -818,8 +820,8 @@ let export ?except senv dir = let senv = try join_safe_environment ?except senv with e -> - let e = Errors.push e in - Errors.errorlabstrm "export" (Errors.iprint e) + let e = CErrors.push e in + CErrors.user_err ~hdr:"export" (CErrors.iprint e) in assert(senv.future_cst = []); let () = check_current_library dir senv in @@ -854,6 +856,9 @@ let export ?except senv dir = let import lib cst vodigest senv = check_required senv.required lib.comp_deps; check_engagement senv.env lib.comp_enga; + if DirPath.equal (ModPath.dp senv.modpath) lib.comp_name then + CErrors.user_err ~hdr:"Safe_typing.import" + (Pp.strbrk "Cannot load a library with the same name as the current one."); let mp = MPfile lib.comp_name in let mb = lib.comp_mod in let env = Environ.push_context_set ~strict:true @@ -903,7 +908,7 @@ let register_inline kn senv = let open Environ in let open Pre_env in if not (evaluable_constant kn senv.env) then - Errors.error "Register inline: an evaluable constant is expected"; + CErrors.error "Register inline: an evaluable constant is expected"; let env = pre_env senv.env in let (cb,r) = Cmap_env.find kn env.env_globals.env_constants in let cb = {cb with const_inline_code = true} in |