[declare] Move udecl to Info structure.

9 files changed, 27 insertions, 30 deletions

diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index c4f7638fb9..7779e4f4c7 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -41,6 +41,6 @@ let start_deriving f suchthat name : Declare.Proof.t =
   in
 
   let info = Declare.Info.make ~proof_ending:(Declare.Proof_ending.(End_derive {f; name})) ~kind () in
-  let lemma = Declare.start_dependent_proof ~name ~poly ~info ~udecl:UState.default_univ_decl goals in
+  let lemma = Declare.start_dependent_proof ~name ~poly ~info goals in
   Declare.Proof.map lemma ~f:(fun p ->
       Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p)
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 6ec12db952..2c85ae079f 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -856,7 +856,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
   let info = Declare.Info.make () in
   let lemma =
     Declare.start_proof ~name:(mk_equation_id f_id) ~poly:false ~info
-      ~impargs:[] ~udecl:UState.default_univ_decl evd lemma_type
+      ~impargs:[] evd lemma_type
   in
   let lemma, _ = Declare.by (Proofview.V82.tactic prove_replacement) lemma in
   let () =
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 8a07c2109e..a914cef6e4 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -1520,8 +1520,8 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
           let typ, _ = lemmas_types_infos.(i) in
           let info = Declare.Info.make () in
           let lemma =
-            Declare.start_proof ~name:lem_id ~poly:false ~info ~impargs:[]
-              ~udecl:UState.default_univ_decl !evd typ
+            Declare.start_proof ~name:lem_id ~poly:false ~info ~impargs:[] !evd
+              typ
           in
           let lemma =
             fst @@ Declare.by (Proofview.V82.tactic (proving_tac i)) lemma
@@ -1587,7 +1587,6 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
           let info = Declare.Info.make () in
           let lemma =
             Declare.start_proof ~name:lem_id ~poly:false sigma ~info ~impargs:[]
-              ~udecl:UState.default_univ_decl
               (fst lemmas_types_infos.(i))
           in
           let lemma =
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 853a54592d..9f36eada45 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1494,8 +1494,8 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name
   in
   let info = Declare.Info.make ~hook:(Declare.Hook.make hook) () in
   let lemma =
-    Declare.start_proof ~name:na ~poly:false (* FIXME *) ~info ~impargs:[]
-      ~udecl:UState.default_univ_decl sigma gls_type
+    Declare.start_proof ~name:na ~poly:false (* FIXME *) ~info ~impargs:[] sigma
+      gls_type
   in
   let lemma =
     if Indfun_common.is_strict_tcc () then
@@ -1534,7 +1534,7 @@ let com_terminate interactive_proof tcc_lemma_name tcc_lemma_ref is_mes
     let info = Declare.Info.make ~hook () in
     let lemma =
       Declare.start_proof ~name:thm_name ~poly:false (*FIXME*) ~info ctx
-        ~impargs:[] ~udecl:UState.default_univ_decl
+        ~impargs:[]
         (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref))
     in
     let lemma =
@@ -1608,7 +1608,6 @@ let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref
   let info = Declare.Info.make () in
   let lemma =
     Declare.start_proof ~name:eq_name ~poly:false evd ~info ~impargs:[]
-      ~udecl:UState.default_univ_decl
       (EConstr.of_constr equation_lemma_type)
   in
   let lemma =
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 0bf97fefa6..0c1c763b64 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -2000,7 +2000,7 @@ let add_morphism_interactive atts m n : Declare.Proof.t =
   let info = Declare.Info.make ~hook ~kind () in
   Flags.silently
     (fun () ->
-       let lemma = Declare.start_proof ~name:instance_id ~poly ~info ~impargs:[] ~udecl:UState.default_univ_decl evd morph in
+       let lemma = Declare.start_proof ~name:instance_id ~poly ~info ~impargs:[] evd morph in
        fst (Declare.by (Tacinterp.interp tac) lemma)) ()
 
 let add_morphism atts binders m s n =
diff --git a/vernac/classes.ml b/vernac/classes.ml
index b36a6fa3a6..1397746dd9 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -359,11 +359,11 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri impargs udecl id
   let sigma = Evd.reset_future_goals sigma in
   let kind = Decls.(IsDefinition Instance) in
   let hook = Declare.Hook.(make (fun { S.dref ; _ } -> instance_hook pri global ?hook dref)) in
-  let info = Declare.Info.make ~hook ~kind () in
+  let info = Declare.Info.make ~hook ~kind ~udecl () in
   (* XXX: We need to normalize the type, otherwise Admitted / Qed will fails!
      This is due to a bug in proof_global :( *)
   let termtype = Evarutil.nf_evar sigma termtype in
-  let lemma = Declare.start_proof ~name:id ~poly ~udecl ~info ~impargs sigma termtype in
+  let lemma = Declare.start_proof ~name:id ~poly ~info ~impargs sigma termtype in
   (* spiwack: I don't know what to do with the status here. *)
   let lemma =
     match term with
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 430639b637..29f2713192 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -89,19 +89,23 @@ module Info = struct
     (* This could be improved and the CEphemeron removed *)
     ; scope : Locality.locality
     ; kind : Decls.logical_kind
-    (* thms and compute guard are specific only to start_lemma_with_initialization + regular terminator *)
+    ; udecl: UState.universe_decl
+    (** Initial universe declarations *)
     ; thms : Recthm.t list
     ; compute_guard : lemma_possible_guards
+    (** thms and compute guard are specific only to
+       start_lemma_with_initialization + regular terminator *)
     }
 
   let make ?hook ?(proof_ending=Proof_ending.Regular) ?(scope=Locality.Global Locality.ImportDefaultBehavior)
-      ?(kind=Decls.(IsProof Lemma)) () =
+      ?(kind=Decls.(IsProof Lemma)) ?(udecl=UState.default_univ_decl) () =
     { hook
     ; compute_guard = []
     ; proof_ending = CEphemeron.create proof_ending
     ; thms = []
     ; scope
     ; kind
+    ; udecl
     }
 
   (* This is used due to a deficiency on the API, should fix *)
@@ -120,8 +124,6 @@ type t =
   { endline_tactic : Genarg.glob_generic_argument option
   ; section_vars : Id.Set.t option
   ; proof : Proof.t
-  ; udecl: UState.universe_decl
-  (** Initial universe declarations *)
   ; initial_euctx : UState.t
   (** The initial universe context (for the statement) *)
   ; info : Info.t
@@ -131,7 +133,6 @@ type t =
 
 let get_proof ps = ps.proof
 let get_proof_name ps = (Proof.data ps.proof).Proof.name
-
 let get_initial_euctx ps = ps.initial_euctx
 
 let fold_proof f p = f p.proof
@@ -173,7 +174,7 @@ let initialize_named_context_for_proof () =
    conclusion). The proof is started in the evar map [sigma] (which
    can typically contain universe constraints), and with universe
    bindings [udecl]. *)
-let start_proof_core ~name ~udecl ~poly ?(impargs=[]) ?(sign=initialize_named_context_for_proof ()) ~info sigma typ =
+let start_proof_core ~name ~poly ?(impargs=[]) ?(sign=initialize_named_context_for_proof ()) ~info sigma typ =
   (* In ?sign, we remove the bodies of variables in the named context
      marked "opaque", this is a hack tho, see #10446, and
      build_constant_by_tactic uses a different method that would break
@@ -185,20 +186,18 @@ let start_proof_core ~name ~udecl ~poly ?(impargs=[]) ?(sign=initialize_named_co
   { proof
   ; endline_tactic = None
   ; section_vars = None
-  ; udecl
   ; initial_euctx
   ; info
   }
 
 let start_proof = start_proof_core ?sign:None
 
-let start_dependent_proof ~name ~udecl ~poly ~info goals =
+let start_dependent_proof ~name ~poly ~info goals =
   let proof = Proof.dependent_start ~name ~poly goals in
   let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in
   { proof
   ; endline_tactic = None
   ; section_vars = None
-  ; udecl
   ; initial_euctx
   ; info
   }
@@ -239,16 +238,16 @@ let start_proof_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recgua
   match thms with
   | [] -> CErrors.anomaly (Pp.str "No proof to start.")
   | { Recthm.name; typ; impargs; _} :: thms ->
-    let info = Info.make ?hook ~scope ~kind () in
+    let info = Info.make ?hook ~scope ~kind ~udecl () in
     let info = { info with Info.compute_guard; thms } in
     (* start_lemma has the responsibility to add (name, impargs, typ)
        to thms, once Info.t is more refined this won't be necessary *)
-    let lemma = start_proof ~name ~impargs ~poly ~udecl ~info sigma (EConstr.of_constr typ) in
+    let lemma = start_proof ~name ~impargs ~poly ~info sigma (EConstr.of_constr typ) in
     map_proof (fun p ->
         pi1 @@ Proof.run_tactic Global.(env ()) init_tac p) lemma
 
 let get_used_variables pf = pf.section_vars
-let get_universe_decl pf = pf.udecl
+let get_universe_decl pf = pf.info.Info.udecl
 
 let set_used_variables ps l =
   let open Context.Named.Declaration in
@@ -401,7 +400,7 @@ let make_univs ~poly ~uctx ~udecl (used_univs_typ, typ) (used_univs_body, body)
 
 let close_proof ~opaque ~keep_body_ucst_separate ps =
 
-  let { section_vars; proof; udecl; initial_euctx } = ps in
+  let { section_vars; proof; initial_euctx; info = { Info.udecl } } = ps in
   let { Proof.name; poly } = Proof.data proof in
   let unsafe_typ = keep_body_ucst_separate && not poly in
   let elist, uctx = prepare_proof ~unsafe_typ ps in
@@ -851,7 +850,7 @@ end
 type closed_proof_output = (Constr.t * Evd.side_effects) list * UState.t
 
 let close_proof_delayed ~feedback_id ps (fpl : closed_proof_output Future.computation) =
-  let { section_vars; proof; udecl; initial_euctx } = ps in
+  let { section_vars; proof; initial_euctx; info = { Info.udecl } } = ps in
   let { Proof.name; poly; entry; sigma } = Proof.data proof in
 
   (* We don't allow poly = true in this path *)
@@ -922,7 +921,7 @@ let by tac = map_fold_proof (Proof.solve (Goal_select.SelectNth 1) None tac)
 let build_constant_by_tactic ~name ?(opaque=Vernacexpr.Transparent) ~uctx ~sign ~poly typ tac =
   let evd = Evd.from_ctx uctx in
   let info = Info.make () in
-  let pf = start_proof_core ~name ~poly ~sign ~udecl:UState.default_univ_decl ~impargs:[] ~info evd typ in
+  let pf = start_proof_core ~name ~poly ~sign ~impargs:[] ~info evd typ in
   let pf, status = by tac pf in
   let { entries; uctx } = close_proof ~opaque ~keep_body_ucst_separate:false pf in
   match entries with
diff --git a/vernac/declare.mli b/vernac/declare.mli
index 67389d2966..25a4d80f49 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -121,6 +121,8 @@ module Info : sig
     (** locality  *)
     -> ?kind:Decls.logical_kind
     (** Theorem, etc... *)
+    -> ?udecl:UState.universe_decl
+    (** Universe declaration *)
     -> unit
     -> t
 
@@ -170,7 +172,6 @@ end
    bindings [udecl]. *)
 val start_proof
   :  name:Names.Id.t
-  -> udecl:UState.universe_decl
   -> poly:bool
   -> ?impargs:Impargs.manual_implicits
   -> info:Info.t
@@ -182,7 +183,6 @@ val start_proof
     initial goals. *)
 val start_dependent_proof
   :  name:Names.Id.t
-  -> udecl:UState.universe_decl
   -> poly:bool
   -> info:Info.t
   -> Proofview.telescope
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index c0105224bf..86cad967b9 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -146,7 +146,7 @@ let rec solve_obligation prg num tac =
   in
   let info = Declare.Info.make ~proof_ending ~scope ~kind () in
   let poly = Internal.get_poly prg in
-  let lemma = Declare.start_proof ~name:obl.obl_name ~poly ~impargs:[] ~udecl:UState.default_univ_decl ~info evd (EConstr.of_constr obl.obl_type) in
+  let lemma = Declare.start_proof ~name:obl.obl_name ~poly ~impargs:[] ~info evd (EConstr.of_constr obl.obl_type) in
   let lemma = fst @@ Declare.by !default_tactic lemma in
   let lemma = Option.cata (fun tac -> Declare.Proof.set_endline_tactic tac lemma) lemma tac in
   lemma