From 2df88d833767f6a43ac8f08627e1cb9cc0c8b30d Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 5 Jul 2016 17:19:05 +0200 Subject: 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. --- kernel/safe_typing.ml | 3 +++ 1 file changed, 3 insertions(+) (limited to 'kernel/safe_typing.ml') 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 -- cgit v1.2.3