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

5 files changed, 13 insertions, 18 deletions

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")
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 178116c580..2501ce4f26 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -79,8 +79,9 @@ mono
 The command has indeed failed with message:
 Universe u already exists.
 Monomorphic bobmorane = 
-let tt := Type@{tt.v} in let ff := Type@{ff.v} in tt -> ff
-     : Type@{max(tt.u,ff.u)}
+let tt := Type@{UnivBinders.32} in
+let ff := Type@{UnivBinders.34} in tt -> ff
+     : Type@{max(UnivBinders.31,UnivBinders.33)}
 
 bobmorane is not universe polymorphic
 The command has indeed failed with message:
diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v
index 19d241d35d..ee3574341f 100644
--- a/test-suite/output/UnivBinders.v
+++ b/test-suite/output/UnivBinders.v
@@ -73,19 +73,10 @@ Module SecLet.
     (* Fail Let foo@{} := Type@{u}. (* doesn't parse: Let foo@{...} doesn't exist *) *)
     Unset Strict Universe Declaration.
     Let tt : Type@{u} := Type@{v}. (* names disappear in the ether *)
-    Let ff : Type@{u}. Proof. exact Type@{v}. Qed. (* if Set Universe Polymorphism: universes are named ff.u and ff.v. Otherwise names disappear into space *)
+    Let ff : Type@{u}. Proof. exact Type@{v}. Qed. (* names disappear into space *)
     Definition bobmorane := tt -> ff.
   End foo.
-  Print bobmorane. (*
-                     bobmorane@{UnivBinders.15 UnivBinders.16 ff.u ff.v} =
-                     let tt := Type@{UnivBinders.16} in let ff := Type@{ff.v} in tt -> ff
-                     : Type@{max(UnivBinders.15,ff.u)}
-                     (* UnivBinders.15 UnivBinders.16 ff.u ff.v |= UnivBinders.16 < UnivBinders.15
-                     ff.v < ff.u
-                    *)
-
-                    bobmorane is universe polymorphic
-                    *)
+  Print bobmorane.
 End SecLet.
 
 (* fun x x => foo is nonsense with local binders *)
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 35fb18e292..2fe03a8ec5 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -43,9 +43,11 @@ let declare_definition ident (local, p, k) ce pl imps hook =
   | Discharge | Local | Global ->
       let local = get_locality ident ~kind:"definition" local in
       let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in
-      ConstRef kn in
+      let gr = ConstRef kn in
+      let () = Declare.declare_univ_binders gr pl in
+      gr
+  in
   let () = maybe_declare_manual_implicits false gr imps in
-  let () = Declare.declare_univ_binders gr pl in
   let () = definition_message ident in
   Lemmas.call_hook fix_exn hook local gr; gr
 
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 150f2c6ee9..3b041b7065 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -197,10 +197,11 @@ let save ?export_seff id const uctx do_guard (locality,poly,kind) hook =
           let () = if should_suggest
             then Proof_using.suggest_constant (Global.env ()) kn
           in
-          ConstRef kn
+          let gr = ConstRef kn in
+          Declare.declare_univ_binders gr (UState.universe_binders uctx);
+          gr
     in
     definition_message id;
-    Declare.declare_univ_binders r (UState.universe_binders uctx);
     call_hook (fun exn -> exn) hook locality r
   with e when CErrors.noncritical e ->
     let e = CErrors.push e in