[declare] Move udecl to Info structure.

5 files changed, 8 insertions, 10 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 =