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.

4 files changed, 8 insertions, 11 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index c526ae000a..31a73db04f 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -140,7 +140,7 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo
     let status = by tac in
     let _,(const,univs,_) = cook_proof () in
     Proof_global.discard_current ();
-    const, status, fst univs
+    const, status, univs
   with reraise ->
     let reraise = CErrors.push reraise in
     Proof_global.discard_current ();
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 2acb678d7f..5a317a956d 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -35,11 +35,11 @@ val start_proof :
 val cook_this_proof :
     Proof_global.proof_object ->
   (Id.t *
-    (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * goal_kind))
+    (Safe_typing.private_constants Entries.definition_entry * UState.t * goal_kind))
 
 val cook_proof : unit ->
   (Id.t *
-    (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * goal_kind))
+    (Safe_typing.private_constants Entries.definition_entry * UState.t * goal_kind))
 
 (** {6 ... } *)
 (** [get_goal_context n] returns the context of the [n]th subgoal of
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index c1e1c2edad..535ef2013d 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -68,17 +68,16 @@ let _ =
 
 (* Extra info on proofs. *)
 type lemma_possible_guards = int list list
-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
+  | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t
   | Proved of Vernacexpr.opacity_flag *
               Vernacexpr.lident option *
               proof_object
@@ -333,7 +332,6 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
   in
   let fpl, univs = Future.split2 fpl in
   let universes = if poly || now then Future.force univs else initial_euctx in
-  let binders = if poly then Some (UState.universe_binders universes) else None in
   (* Because of dependent subgoals at the beginning of proofs, we could
      have existential variables in the initial types of goals, we need to
      normalise them for the kernel. *)
@@ -409,7 +407,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
   in
   let entries = Future.map2 entry_fn fpl initial_goals in
   { id = pid; entries = entries; persistence = strength;
-    universes = (universes, binders) },
+    universes },
   fun pr_ending -> CEphemeron.get terminator pr_ending
 
 let return_proof ?(allow_partial=false) () =
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 059459042b..27e99f218b 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -37,18 +37,17 @@ val compact_the_proof : unit -> unit
     (i.e. an proof ending command) and registers the appropriate
     values. *)
 type lemma_possible_guards = int list list
-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