[declare] Remove Lemmas module

The module is now a stub. We choose to be explicit on the parameters
for now, this will improve in next commits with the refactoring of
proof / constant information.

5 files changed, 20 insertions, 8 deletions

diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index 633d5dfe3b..c4f7638fb9 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 = Lemmas.start_dependent_lemma ~name ~poly ~info goals in
+  let lemma = Declare.start_dependent_proof ~name ~poly ~info ~udecl:UState.default_univ_decl 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 652f942cb9..c0d7c1e8e6 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -853,8 +853,10 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
 
   (*i The next call to mk_equation_id is valid since we are
      constructing the lemma Ensures by: obvious i*)
+  let info = Declare.Info.make () in
   let lemma =
-    Lemmas.start_lemma ~name:(mk_equation_id f_id) ~poly:false evd lemma_type
+    Declare.start_proof ~name:(mk_equation_id f_id) ~poly:false ~info
+      ~impargs:[] ~udecl:UState.default_univ_decl 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 2336689a66..30069c9914 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -1518,7 +1518,11 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
             i*)
           let lem_id = mk_correct_id f_id in
           let typ, _ = lemmas_types_infos.(i) in
-          let lemma = Lemmas.start_lemma ~name:lem_id ~poly:false !evd typ 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
+          in
           let lemma =
             fst @@ Declare.by (Proofview.V82.tactic (proving_tac i)) lemma
           in
@@ -1580,8 +1584,10 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
               Ensures by: obvious
             i*)
           let lem_id = mk_complete_id f_id in
+          let info = Declare.Info.make () in
           let lemma =
-            Lemmas.start_lemma ~name:lem_id ~poly:false sigma
+            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 f92d4c6a72..58ed3864bb 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1492,7 +1492,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 =
-    Lemmas.start_lemma ~name:na ~poly:false (* FIXME *) ~info sigma gls_type
+    Declare.start_proof ~name:na ~poly:false (* FIXME *) ~info ~impargs:[]
+      ~udecl:UState.default_univ_decl sigma gls_type
   in
   let lemma =
     if Indfun_common.is_strict_tcc () then
@@ -1530,7 +1531,8 @@ let com_terminate interactive_proof tcc_lemma_name tcc_lemma_ref is_mes
   let start_proof env ctx tac_start tac_end =
     let info = Declare.Info.make ~hook () in
     let lemma =
-      Lemmas.start_lemma ~name:thm_name ~poly:false (*FIXME*) ~info ctx
+      Declare.start_proof ~name:thm_name ~poly:false (*FIXME*) ~info ctx
+        ~impargs:[] ~udecl:UState.default_univ_decl
         (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref))
     in
     let lemma =
@@ -1601,8 +1603,10 @@ let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref
   let evd = Evd.from_ctx uctx in
   let f_constr = constr_of_monomorphic_global f_ref in
   let equation_lemma_type = subst1 f_constr equation_lemma_type in
+  let info = Declare.Info.make () in
   let lemma =
-    Lemmas.start_lemma ~name:eq_name ~poly:false evd
+    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 e784d6e682..914dc96648 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1999,7 +1999,7 @@ let add_morphism_interactive atts m n : Declare.Proof.t =
   let info = Declare.Info.make ~hook ~kind () in
   Flags.silently
     (fun () ->
-       let lemma = Lemmas.start_lemma ~name:instance_id ~poly ~info evd morph in
+       let lemma = Declare.start_proof ~name:instance_id ~poly ~info ~impargs:[] ~udecl:UState.default_univ_decl evd morph in
        fst (Declare.by (Tacinterp.interp tac) lemma)) ()
 
 let add_morphism atts binders m s n =