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 /plugins/nsatz | |
| 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 'plugins/nsatz')
0 files changed, 0 insertions, 0 deletions