diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/safe_typing.ml | 3 | ||||
| -rw-r--r-- | kernel/univ.ml | 2 |
2 files changed, 4 insertions, 1 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 62753962c8..927278965f 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -859,6 +859,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 + Errors.errorlabstrm "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 diff --git a/kernel/univ.ml b/kernel/univ.ml index 117bc4e5fd..2cc57c38ca 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -754,7 +754,7 @@ let is_set_arc u = Level.is_set u.univ let is_prop_arc u = Level.is_prop u.univ exception AlreadyDeclared - + let add_universe vlev strict g = try let _arcv = UMap.find vlev g in |