Cleanup API for registering universe binders.

- Regularly declared for for polymorphic constants
- Declared globally for monomorphic constants.

  E.g mono@{i} := Type@{i} is printed as
  mono@{mono.i} := Type@{mono.i}.

  There can be a name clash if there's a module and a constant of the
  same name. It is detected and is an error if the constant is first
  but is not detected and the name for the constant not
  registered (??) if the constant comes second.

Accept VarRef when registering universe binders

Fix two problems found by Gaëtan where binders were not registered properly

Simplify API substantially by not passing around a substructure of an
already carrier-around structure in interpretation/declaration code of
constants and proofs

Fix an issue of the stronger restrict universe context + no evd leak

This is uncovered by not having an evd leak in interp_definition, and
the stronger restrict_universe_context. This patch could be backported
to 8.7, it could also be triggered by the previous restrict_context I
think.

3 files changed, 87 insertions, 20 deletions

diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index f69379a57..d6d410d1a 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -44,26 +44,45 @@ bar@{u} = nat
 bar is universe polymorphic
 foo@{u Top.17 v} = 
 Type@{Top.17} -> Type@{v} -> Type@{u}
-     : Type@{max(u+1, Top.17+1, v+1)}
+     : Type@{max(u+1,Top.17+1,v+1)}
 (* u Top.17 v |=  *)
 
 foo is universe polymorphic
-Monomorphic mono = Type@{u}
-     : Type@{u+1}
-(* {u} |=  *)
+Monomorphic mono = Type@{mono.u}
+     : Type@{mono.u+1}
+(* {mono.u} |=  *)
 
 mono is not universe polymorphic
+mono
+     : Type@{mono.u+1}
+Type@{mono.u}
+     : Type@{mono.u+1}
+The command has indeed failed with message:
+Universe u already exists.
+monomono
+     : Type@{MONOU+1}
+mono.monomono
+     : Type@{mono.MONOU+1}
+monomono
+     : Type@{MONOU+1}
+mono
+     : Type@{mono.u+1}
+The command has indeed failed with message:
+Universe u already exists.
+bobmorane = 
+let tt := Type@{tt.v} in let ff := Type@{ff.v} in tt -> ff
+     : Type@{max(tt.u,ff.u)}
 The command has indeed failed with message:
 Universe u already bound.
 foo@{E M N} = 
 Type@{M} -> Type@{N} -> Type@{E}
-     : Type@{max(E+1, M+1, N+1)}
+     : Type@{max(E+1,M+1,N+1)}
 (* E M N |=  *)
 
 foo is universe polymorphic
 foo@{Top.16 Top.17 Top.18} = 
 Type@{Top.17} -> Type@{Top.18} -> Type@{Top.16}
-     : Type@{max(Top.16+1, Top.17+1, Top.18+1)}
+     : Type@{max(Top.16+1,Top.17+1,Top.18+1)}
 (* Top.16 Top.17 Top.18 |=  *)
 
 foo is universe polymorphic
@@ -88,9 +107,10 @@ The command has indeed failed with message:
 This object does not support universe names.
 The command has indeed failed with message:
 Cannot enforce v < u because u < gU < gV < v
-Monomorphic bind_univs.mono = Type@{u}
-     : Type@{u+1}
-(* {u} |=  *)
+Monomorphic bind_univs.mono = 
+Type@{bind_univs.mono.u}
+     : Type@{bind_univs.mono.u+1}
+(* {bind_univs.mono.u} |=  *)
 
 bind_univs.mono is not universe polymorphic
 bind_univs.poly@{u} = Type@{u}
@@ -99,12 +119,12 @@ bind_univs.poly@{u} = Type@{u}
 
 bind_univs.poly is universe polymorphic
 insec@{v} = Type@{u} -> Type@{v}
-     : Type@{max(u+1, v+1)}
+     : Type@{max(u+1,v+1)}
 (* v |=  *)
 
 insec is universe polymorphic
 insec@{u v} = Type@{u} -> Type@{v}
-     : Type@{max(u+1, v+1)}
+     : Type@{max(u+1,v+1)}
 (* u v |=  *)
 
 insec is universe polymorphic
@@ -125,28 +145,28 @@ inmod@{u} = Type@{u}
 inmod is universe polymorphic
 Applied.infunct@{u v} = 
 inmod@{u} -> Type@{v}
-     : Type@{max(u+1, v+1)}
+     : Type@{max(u+1,v+1)}
 (* u v |=  *)
 
 Applied.infunct is universe polymorphic
-axfoo@{i Top.33 Top.34} : Type@{Top.33} -> Type@{i}
-(* i Top.33 Top.34 |=  *)
+axfoo@{i Top.41 Top.42} : Type@{Top.41} -> Type@{i}
+(* i Top.41 Top.42 |=  *)
 
 axfoo is universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant Top.axfoo
-axbar@{i Top.33 Top.34} : Type@{Top.34} -> Type@{i}
-(* i Top.33 Top.34 |=  *)
+axbar@{i Top.41 Top.42} : Type@{Top.42} -> Type@{i}
+(* i Top.41 Top.42 |=  *)
 
 axbar is universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant Top.axbar
-axfoo' : Type@{Top.36} -> Type@{i}
+axfoo' : Type@{Top.44} -> Type@{axbar'.i}
 
 axfoo' is not universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant Top.axfoo'
-axbar' : Type@{Top.36} -> Type@{i}
+axbar' : Type@{Top.44} -> Type@{axbar'.i}
 
 axbar' is not universe polymorphic
 Argument scope is [type_scope]
diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v
index 116d5e5e9..266d94ad9 100644
--- a/test-suite/output/UnivBinders.v
+++ b/test-suite/output/UnivBinders.v
@@ -1,6 +1,6 @@
 Set Universe Polymorphism.
 Set Printing Universes.
-Unset Strict Universe Declaration.
+(* Unset Strict Universe Declaration. *)
 
 (* universe binders on inductive types and record projections *)
 Inductive Empty@{u} : Type@{u} := .
@@ -25,14 +25,59 @@ Print wrap.
 Instance bar@{u} : Wrap@{u} Set. Proof. exact nat. Qed.
 Print bar.
 
+Unset Strict Universe Declaration.
 (* The universes in the binder come first, then the extra universes in
    order of appearance. *)
 Definition foo@{u +} := Type -> Type@{v} -> Type@{u}.
 Print foo.
+Set Strict Universe Declaration.
 
 (* Binders even work with monomorphic definitions! *)
 Monomorphic Definition mono@{u} := Type@{u}.
 Print mono.
+Check mono.
+Check Type@{mono.u}.
+
+Module mono.
+  Fail Monomorphic Universe u.
+  Monomorphic Universe MONOU.
+
+  Monomorphic Definition monomono := Type@{MONOU}.
+  Check monomono.
+End mono.
+Check mono.monomono. (* qualified MONOU *)
+Import mono.
+Check monomono. (* unqualified MONOU *)
+Check mono. (* still qualified mono.u *)
+
+Monomorphic Constraint Set < Top.mono.u.
+
+Module mono2.
+  Monomorphic Universe u.
+End mono2.
+
+Fail Monomorphic Definition mono2@{u} := Type@{u}.
+
+Module SecLet.
+  Unset Universe Polymorphism.
+  Section foo.
+    (* 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 *)
+    Definition bobmorane := tt -> ff.
+  End foo.
+  Print bobmorane. (*
+                     bobmorane@{Top.15 Top.16 ff.u ff.v} =
+                     let tt := Type@{Top.16} in let ff := Type@{ff.v} in tt -> ff
+                     : Type@{max(Top.15,ff.u)}
+                     (* Top.15 Top.16 ff.u ff.v |= Top.16 < Top.15
+                     ff.v < ff.u
+                    *)
+
+                    bobmorane is universe polymorphic
+                    *)
+End SecLet.
 
 (* fun x x => foo is nonsense with local binders *)
 Fail Definition fo@{u u} := Type@{u}.
@@ -61,7 +106,7 @@ Monomorphic Universes gU gV. Monomorphic Constraint gU < gV.
 Fail Lemma foo@{u v|u < gU, gV < v, v < u} : nat.
 
 (* Universe binders survive through compilation, sections and modules. *)
-Require bind_univs.
+Require TestSuite.bind_univs.
 Print bind_univs.mono.
 Print bind_univs.poly.
 
diff --git a/test-suite/prerequisite/bind_univs.v b/test-suite/prerequisite/bind_univs.v
index f17c00e9d..e834fde11 100644
--- a/test-suite/prerequisite/bind_univs.v
+++ b/test-suite/prerequisite/bind_univs.v
@@ -3,3 +3,5 @@
 Monomorphic Definition mono@{u} := Type@{u}.
 
 Polymorphic Definition poly@{u} := Type@{u}.
+
+Monomorphic Universe reqU.