[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, 2 insertions, 65 deletions

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