[proof] Remove redundant universe declaration information.

This was already in the base proof object however not forwarded by
`close_proof`. thus it had to be stored twice.

There are more cases like this, like `poly`, all are covered by
subsequent commits.

5 files changed, 43 insertions, 42 deletions

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index dfd54594eb..2f7e5d618a 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -36,12 +36,13 @@ type 'a proof_entry = {
   proof_entry_inline_code : bool;
 }
 
-type proof_object = {
-  id : Names.Id.t;
-  entries : Evd.side_effects proof_entry list;
-  persistence : Decl_kinds.goal_kind;
-  universes: UState.t;
-}
+type proof_object =
+  { id : Names.Id.t
+  ; entries : Evd.side_effects proof_entry list
+  ; persistence : Decl_kinds.goal_kind
+  ; universes: UState.t
+  ; udecl : UState.universe_decl
+  }
 
 type opacity_flag = Opaque | Transparent
 
@@ -49,7 +50,7 @@ type t =
   { endline_tactic : Genarg.glob_generic_argument option
   ; section_vars : Constr.named_context option
   ; proof : Proof.t
-  ; universe_decl: UState.universe_decl
+  ; udecl: UState.universe_decl
   ; strength : Decl_kinds.goal_kind
   }
 
@@ -95,7 +96,7 @@ let start_proof sigma name udecl kind goals =
   { proof = Proof.start ~name ~poly:(pi2 kind) sigma goals
   ; endline_tactic = None
   ; section_vars = None
-  ; universe_decl = udecl
+  ; udecl
   ; strength = kind
   }
 
@@ -103,12 +104,12 @@ let start_dependent_proof name udecl kind goals =
   { proof = Proof.dependent_start ~name ~poly:(pi2 kind) goals
   ; endline_tactic = None
   ; section_vars = None
-  ; universe_decl = udecl
+  ; udecl
   ; strength = kind
   }
 
 let get_used_variables pf = pf.section_vars
-let get_universe_decl pf = pf.universe_decl
+let get_universe_decl pf = pf.udecl
 
 let set_used_variables ps l =
   let open Context.Named.Declaration in
@@ -159,7 +160,7 @@ let private_poly_univs =
 
 let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
                 (fpl : closed_proof_output Future.computation) ps =
-  let { section_vars; proof; universe_decl; strength } = ps in
+  let { section_vars; proof; udecl; strength } = ps in
   let Proof.{ name; poly; entry; initial_euctx } = Proof.data proof in
   let opaque = match opaque with Opaque -> true | Transparent -> false in
   let constrain_variables ctx =
@@ -194,13 +195,13 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
              the body.  So we keep the two sets distinct. *)
           let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
           let ctx_body = UState.restrict ctx used_univs in
-          let univs = UState.check_mono_univ_decl ctx_body universe_decl in
+          let univs = UState.check_mono_univ_decl ctx_body udecl in
           (initunivs, typ), ((body, univs), eff)
         else if poly && opaque && private_poly_univs () then
           let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
           let universes = UState.restrict universes used_univs in
           let typus = UState.restrict universes used_univs_typ in
-          let udecl = UState.check_univ_decl ~poly typus universe_decl in
+          let udecl = UState.check_univ_decl ~poly typus udecl in
           let ubody = Univ.ContextSet.diff
               (UState.context_set universes)
               (UState.context_set typus)
@@ -214,7 +215,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
              TODO: check if restrict is really necessary now. *)
           let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
           let ctx = UState.restrict universes used_univs in
-          let univs = UState.check_univ_decl ~poly ctx universe_decl in
+          let univs = UState.check_univ_decl ~poly ctx udecl in
           (univs, typ), ((body, Univ.ContextSet.empty), eff)
       in 
        fun t p -> Future.split2 (Future.chain p (make_body t))
@@ -236,7 +237,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
               (Vars.universes_of_constr pt)
           in
           let univs = UState.restrict univs used_univs in
-          let univs = UState.check_mono_univ_decl univs universe_decl in
+          let univs = UState.check_mono_univ_decl univs udecl in
           (pt,univs),eff)
   in
   let entry_fn p (_, t) =
@@ -253,8 +254,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
       proof_entry_universes = univs; }
   in
   let entries = Future.map2 entry_fn fpl Proofview.(initial_goals entry) in
-  { id = name; entries = entries; persistence = strength;
-    universes }
+  { id = name; entries = entries; persistence = strength; universes; udecl }
 
 let return_proof ?(allow_partial=false) ps =
  let { proof } = ps in
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 17f5c73560..3baa58084d 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -43,12 +43,13 @@ type 'a proof_entry = {
   proof_entry_inline_code : bool;
 }
 
-type proof_object = {
-  id : Names.Id.t;
-  entries : Evd.side_effects proof_entry list;
-  persistence : Decl_kinds.goal_kind;
-  universes: UState.t;
-}
+type proof_object =
+  { id : Names.Id.t
+  ; entries : Evd.side_effects proof_entry list
+  ; persistence : Decl_kinds.goal_kind
+  ; universes: UState.t
+  ; udecl : UState.universe_decl
+  }
 
 type opacity_flag = Opaque | Transparent
 
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 51fddf1563..37af8e1f55 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -375,8 +375,8 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids t
   let sigma = Evd.reset_future_goals sigma in
   let kind = Decl_kinds.(Global ImportDefaultBehavior, poly, DefinitionBody Instance) in
   let hook = DeclareDef.Hook.make (fun _ _ _ -> instance_hook pri global imps ?hook) in
-  let info = Lemmas.Info.make ~udecl ~hook () in
-  let lemma = Lemmas.start_lemma ~name:id ~kind ~info sigma (EConstr.of_constr termtype) in
+  let info = Lemmas.Info.make ~hook () in
+  let lemma = Lemmas.start_lemma ~name:id ~kind ~udecl ~info sigma (EConstr.of_constr termtype) in
   (* spiwack: I don't know what to do with the status here. *)
   let lemma =
     if not (Option.is_empty term) then
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index f1d5412850..c3dfdd1c0f 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -71,19 +71,15 @@ module Info = struct
     { hook : DeclareDef.Hook.t option
     ; compute_guard : lemma_possible_guards
     ; impargs : Impargs.manual_implicits
-    ; udecl : UState.universe_decl
-    (* ^ This is sadly not available on the save_proof path so we
-       duplicate it here *)
     ; proof_ending : Proof_ending.t CEphemeron.key
     (* This could be improved and the CEphemeron removed *)
     ; other_thms : Recthm.t list
     }
 
-  let make ?hook ?(udecl=UState.default_univ_decl) ?(proof_ending=Proof_ending.Regular) () =
+  let make ?hook ?(proof_ending=Proof_ending.Regular) () =
     { hook
     ; compute_guard = []
     ; impargs = []
-    ; udecl
     ; proof_ending = CEphemeron.create proof_ending
     ; other_thms = []
     }
@@ -342,14 +338,19 @@ module Stack = struct
 end
 
 (* Starting a goal *)
-let start_lemma ~name ~kind ?(sign=initialize_named_context_for_proof())
-    ?(info=Info.make ()) sigma  c =
+let start_lemma ~name ~kind
+    ?(udecl=UState.default_univ_decl)
+    ?(sign=initialize_named_context_for_proof())
+    ?(info=Info.make ())
+    sigma c =
   let goals = [ Global.env_of_context sign , c ] in
-  let proof = Proof_global.start_proof sigma name info.Info.udecl kind goals in
+  let proof = Proof_global.start_proof sigma name udecl kind goals in
   { proof ; info }
 
-let start_dependent_lemma ~name ~kind ?(info=Info.make ()) telescope =
-  let proof = Proof_global.start_dependent_proof name info.Info.udecl kind telescope in
+let start_dependent_lemma ~name ~kind
+    ?(udecl=UState.default_univ_decl)
+    ?(info=Info.make ()) telescope =
+  let proof = Proof_global.start_dependent_proof name udecl kind telescope in
   { proof; info }
 
 let rec_tac_initializer finite guard thms snl =
@@ -386,13 +387,12 @@ let start_lemma_with_initialization ?hook ~kind ~udecl sigma recguard thms snl =
   | { Recthm.name; typ; impargs; _}::other_thms ->
     let info =
       Info.{ hook
-           ; udecl
            ; impargs
            ; compute_guard
            ; other_thms
            ; proof_ending = CEphemeron.create Proof_ending.Regular
            } in
-    let lemma = start_lemma ~name ~kind ~info sigma typ in
+    let lemma = start_lemma ~name ~kind ~udecl ~info sigma typ in
     pf_map (Proof_global.map_proof (fun p ->
         match init_tac with
         | None -> p
@@ -486,7 +486,7 @@ let save_lemma_admitted ?proof ~(lemma : t) =
     let open Proof_global in
     let env = Global.env () in
     match proof with
-    | Some ({ id; entries; persistence = k; universes }, { Info.hook; impargs; udecl; other_thms; _} ) ->
+    | Some ({ id; entries; persistence = k; universes; udecl }, { Info.hook; impargs; other_thms; _} ) ->
       if List.length entries <> 1 then
         user_err Pp.(str "Admitted does not support multiple statements");
       let { proof_entry_secctx; proof_entry_type } = List.hd entries in
@@ -534,9 +534,9 @@ let save_lemma_admitted ?proof ~(lemma : t) =
 
 let finish_proved env sigma opaque idopt po info =
   let open Proof_global in
-  let { Info.hook; compute_guard; udecl; impargs; other_thms } = info in
+  let { Info.hook; compute_guard; impargs; other_thms } = info in
   match po with
-  | { id; entries=[const]; persistence=locality,poly,kind; universes } ->
+  | { id; entries=[const]; persistence=locality,poly,kind; universes; udecl } ->
     let is_opaque = match opaque with
       | Transparent -> false
       | Opaque      -> true
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index c1a034c30f..28b9c38072 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -83,8 +83,6 @@ module Info : sig
   val make
     :  ?hook: DeclareDef.Hook.t
     (** Callback to be executed at the end of the proof *)
-    -> ?udecl : UState.universe_decl
-    (** Universe declaration *)
     -> ?proof_ending : Proof_ending.t
     (** Info for special constants *)
     -> unit
@@ -96,6 +94,7 @@ end
 val start_lemma
   :  name:Id.t
   -> kind:goal_kind
+  -> ?udecl:UState.universe_decl
   -> ?sign:Environ.named_context_val
   -> ?info:Info.t
   -> Evd.evar_map
@@ -105,6 +104,7 @@ val start_lemma
 val start_dependent_lemma
   :  name:Id.t
   -> kind:goal_kind
+  -> ?udecl:UState.universe_decl
   -> ?info:Info.t
   -> Proofview.telescope
   -> t