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