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).
---
 vernac/declareDef.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'vernac/declareDef.ml')

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