From 71d4c435e42c24c21ae43f0ddcc7a71bee1009f5 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 9 May 2016 18:31:01 +0200
Subject: congruence: Restrict refreshing to Set

Because refreshing Prop is not semantics-preserving,
the new universe is >= Set, so cannot be minimized to Prop
afterwards.
---
 kernel/univ.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel')

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
-- 
cgit v1.2.3


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')

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
-- 
cgit v1.2.3