diff options
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 34 |
1 files changed, 18 insertions, 16 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index ce05190b6f..ae3679dddb 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 @@ -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 @@ -818,8 +817,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 +853,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 +905,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 |