[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.

10 files changed, 22 insertions, 73 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 =
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 973c6f8e7c..f7d8a4b42f 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -362,7 +362,7 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri impargs udecl id
   (* 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 = Lemmas.start_lemma ~name:id ~poly ~udecl ~info ~impargs sigma termtype in
+  let lemma = Declare.start_proof ~name:id ~poly ~udecl ~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/lemmas.ml b/vernac/lemmas.ml
deleted file mode 100644
index 6fe9b7c257..0000000000
--- a/vernac/lemmas.ml
+++ /dev/null
@@ -1,30 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *         Copyright INRIA, CNRS and contributors             *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(* Created by Hugo Herbelin from contents related to lemma proofs in
-   file command.ml, Aug 2009 *)
-
-(************************************************************************)
-(* Creating a lemma-like constant                                       *)
-(************************************************************************)
-
-(* Starting a goal *)
-let start_lemma ~name ~poly
-    ?(udecl=UState.default_univ_decl)
-    ?(info=Declare.Info.make ()) ?(impargs=[]) sigma c =
-  Declare.start_proof sigma ~name ~udecl ~poly ~impargs ~info c
-
-(* Note that proofs opened by start_dependent lemma cannot be closed
-   by the regular terminators, thus we don't need to update the [thms]
-   field. We will capture this invariant by typing in the future *)
-let start_dependent_lemma ~name ~poly
-    ?(udecl=UState.default_univ_decl)
-    ?(info=Declare.Info.make ()) telescope =
-  Declare.start_dependent_proof ~name ~udecl ~poly ~info telescope
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
deleted file mode 100644
index ef89b9e1ee..0000000000
--- a/vernac/lemmas.mli
+++ /dev/null
@@ -1,32 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *         Copyright INRIA, CNRS and contributors             *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Names
-
-(** {4 Proofs attached to a constant} *)
-
-(** Starts the proof of a constant *)
-val start_lemma
-  :  name:Id.t
-  -> poly:bool
-  -> ?udecl:UState.universe_decl
-  -> ?info:Declare.Info.t
-  -> ?impargs:Impargs.manual_implicits
-  -> Evd.evar_map
-  -> EConstr.types
-  -> Declare.Proof.t
-
-val start_dependent_lemma
-  :  name:Id.t
-  -> poly:bool
-  -> ?udecl:UState.universe_decl
-  -> ?info:Declare.Info.t
-  -> Proofview.telescope
-  -> Declare.Proof.t
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 05edb55760..62fdbf50ad 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 = prg.prg_poly in
-  let lemma = Lemmas.start_lemma ~name:obl.obl_name ~poly ~info evd (EConstr.of_constr obl.obl_type) 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 = fst @@ Declare.by !default_tactic lemma in
   let lemma = Option.cata (fun tac -> Declare.Proof.set_endline_tactic tac lemma) lemma tac in
   lemma
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index 1cad052bce..c30703d734 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -20,7 +20,6 @@ ComHints
 Canonical
 RecLemmas
 Library
-Lemmas
 ComCoercion
 Auto_ind_decl
 Indschemes