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.

1 files changed, 3 insertions, 4 deletions

diff --git a/API/API.mli b/API/API.mli
index 9d1585d602..6227f17c65 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -4847,17 +4847,16 @@ sig
       set : unit -> unit ;
       reset : unit -> unit
     }
-  type proof_universes = UState.t * Universes.universe_binders option
   type proof_object = {
     id : Names.Id.t;
     entries : Safe_typing.private_constants Entries.definition_entry list;
     persistence : Decl_kinds.goal_kind;
-    universes: proof_universes;
+    universes: UState.t;
   }
 
   type proof_ending =
   | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry *
-                  proof_universes
+                  UState.t
   | Proved of Vernacexpr.opacity_flag *
               Vernacexpr.lident option *
               proof_object
@@ -5011,7 +5010,7 @@ sig
       Vernacexpr.goal_selector -> int option -> unit Proofview.tactic ->
       Proof.t -> Proof.t * bool
   val cook_proof :
-    unit -> (Names.Id.t * (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * Decl_kinds.goal_kind))
+    unit -> (Names.Id.t * (Safe_typing.private_constants Entries.definition_entry * UState.t * Decl_kinds.goal_kind))
 
   val get_current_context : unit -> Evd.evar_map * Environ.env
   val current_proof_statement : unit -> Names.Id.t * Decl_kinds.goal_kind * EConstr.types