From 7a3b6b644f85489dced02b33712ad21afe0df47d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 18 Oct 2018 13:59:38 +0200
Subject: Don't declare universe binders for variables.

Otherwise
~~~
Unset Strict Universe Declaration.
Section bar.

  Let baz := Type@{u}.

  Definition k := baz.
End bar.

Section bar.

  Let baz := Type@{u}.

  Definition k' := baz.
End bar.
~~~
is broken (and has been since we stopped checking for repeated section names).
---
 interp/declare.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/declare.ml b/interp/declare.ml
index fe8fc7c969..005334abe4 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -525,7 +525,7 @@ let declare_univ_binders gr pl =
     let l = match gr with
       | ConstRef c -> Label.to_id @@ Constant.label c
       | IndRef (c, _) -> Label.to_id @@ MutInd.label c
-      | VarRef id -> id
+      | VarRef id -> anomaly ~label:"declare_univ_binders" Pp.(str "declare_univ_binders on variable " ++ Id.print id ++ str".")
       | ConstructRef _ ->
         anomaly ~label:"declare_univ_binders"
           Pp.(str "declare_univ_binders on an constructor reference")
-- 
cgit v1.2.3


From a44b97e3e7f4a302a5255ca9fc57ea0b81a36b7e Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 18 Oct 2018 13:04:32 +0200
Subject: Do not qualify universe names by section path.

---
 interp/declare.ml | 25 +++++++++++--------------
 1 file changed, 11 insertions(+), 14 deletions(-)

(limited to 'interp')

diff --git a/interp/declare.ml b/interp/declare.ml
index 005334abe4..a9bfe8cabb 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -473,36 +473,33 @@ type universe_source =
 type universe_name_decl = universe_source * (Id.t * Nametab.universe_id) list
 
 let check_exists sp =
-  let depth = sections_depth () in
-  let sp = Libnames.make_path (pop_dirpath_n depth (dirpath sp)) (basename sp) in
   if Nametab.exists_universe sp then
     alreadydeclared (str "Universe " ++ Id.print (basename sp) ++ str " already exists")
   else ()
 
-let qualify_univ i sp src id =
-  let open Libnames in
+let qualify_univ i dp src id =
   match src with
   | BoundUniv | UnqualifiedUniv ->
-    let sp = dirpath sp in
-    i, make_path sp id
+    i,  Libnames.make_path dp id
   | QualifiedUniv l ->
-    let sp = dirpath sp in
-    let sp = DirPath.repr sp in
-    Nametab.map_visibility succ i, make_path (DirPath.make (l::sp)) id
+    let dp = DirPath.repr dp in
+    Nametab.map_visibility succ i, Libnames.make_path (DirPath.make (l::dp)) id
 
-let do_univ_name ~check i sp src (id,univ) =
-  let i, sp = qualify_univ i sp src id in
+let do_univ_name ~check i dp src (id,univ) =
+  let i, sp = qualify_univ i dp src id in
   if check then check_exists sp;
   Nametab.push_universe i sp univ
 
 let cache_univ_names ((sp, _), (src, univs)) =
-  List.iter (do_univ_name ~check:true (Nametab.Until 1) sp src) univs
+  let depth = sections_depth () in
+  let dp = pop_dirpath_n depth (dirpath sp) in
+  List.iter (do_univ_name ~check:true (Nametab.Until 1) dp src) univs
 
 let load_univ_names i ((sp, _), (src, univs)) =
-  List.iter (do_univ_name ~check:false (Nametab.Until i) sp src) univs
+  List.iter (do_univ_name ~check:false (Nametab.Until i) (dirpath sp) src) univs
 
 let open_univ_names i ((sp, _), (src, univs)) =
-  List.iter (do_univ_name ~check:false (Nametab.Exactly i) sp src) univs
+  List.iter (do_univ_name ~check:false (Nametab.Exactly i) (dirpath sp) src) univs
 
 let discharge_univ_names = function
   | _, (BoundUniv, _) -> None
-- 
cgit v1.2.3