diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-07-05 17:19:05 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-07-05 18:31:28 +0200 |
| commit | 2df88d833767f6a43ac8f08627e1cb9cc0c8b30d (patch) | |
| tree | 4fd9683e9e91b0e28bd99cb02743786f2ed67bc6 /kernel/safe_typing.ml | |
| parent | 57021d22fabb33b281af4de8f3946cb4424c6422 (diff) | |
Prevent unsafe overwriting of Required modules by toplevel library.
In coqtop, one could do for instance:
Require Import Top. (* Where Top contains a Definition b := true *)
Lemma bE : b = true. Proof. reflexivity. Qed.
Definition b := false.
Lemma bad : False. Proof. generalize bE; compute; discriminate. Qed.
That proof could however not be saved because of the circular dependency check.
Safe_typing now checks that we are not requiring (Safe_typing.import) a library
with the same logical name as the current one.
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 62753962c..927278965 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 |