[pfedit] Remove `start_proof` stub from `Pfedit`

This way we only have 2 `start_proof` entries, in `Lemmas` and
`Proof_global`; which they should be unified / brought closer in the
future.

3 files changed, 10 insertions, 31 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 78080fa203..81122e6858 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -26,15 +26,6 @@ let _ = Goptions.declare_bool_option {
 
 let use_unification_heuristics () = !use_unification_heuristics_ref
 
-let start_proof (id : Id.t) ?pl str sigma hyps c ?init_tac terminator =
-  let goals = [ (Global.env_of_context hyps , c) ] in
-  Proof_global.start_proof sigma id ?pl str goals terminator;
-  let env = Global.env () in
-  ignore (Proof_global.with_current_proof (fun _ p ->
-    match init_tac with
-    | None -> p,(true,[])
-    | Some tac -> Proof.run_tactic env tac p))
-
 exception NoSuchGoal
 let _ = CErrors.register_handler begin function
   | NoSuchGoal -> CErrors.user_err Pp.(str "No such goal.")
@@ -142,7 +133,8 @@ let next = let n = ref 0 in fun () -> incr n; !n
 let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theorem) typ tac =
   let evd = Evd.from_ctx ctx in
   let terminator = Proof_global.make_terminator (fun _ -> ()) in
-  start_proof id goal_kind evd sign typ terminator;
+  let goals = [ (Global.env_of_context sign , typ) ] in
+  Proof_global.start_proof evd id goal_kind goals terminator;
   try
     let status = by tac in
     let open Proof_global in
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 76be7936b4..155221947a 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -16,19 +16,6 @@ open Environ
 open Decl_kinds
 
 (** {6 ... } *)
-(** [start_proof s str env t hook tac] starts a proof of name [s] and
-    conclusion [t]; [hook] is optionally a function to be applied at
-    proof end (e.g. to declare the built constructions as a coercion
-    or a setoid morphism); init_tac is possibly a tactic to
-    systematically apply at initialization time (e.g. to start the
-    proof of mutually dependent theorems) *)
-
-val start_proof :
-  Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map -> named_context_val -> EConstr.constr ->
-  ?init_tac:unit Proofview.tactic ->
-  Proof_global.proof_terminator -> unit
-
-(** {6 ... } *)
 (** [get_goal_context n] returns the context of the [n]th subgoal of
    the current focused proof or raises a [UserError] if there is no
    focused proof or if there is no more subgoals *)
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 2b04bfab57..e3808bc36d 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -60,14 +60,14 @@ type closed_proof = proof_object * proof_terminator
 val make_terminator : (proof_ending -> unit) -> proof_terminator
 val apply_terminator : proof_terminator -> proof_ending -> unit
 
-(** [start_proof id str pl goals terminator] starts a proof of name [id]
-    with goals [goals] (a list of pairs of environment and
-    conclusion); [str] describes what kind of theorem/definition this
-    is (spiwack: for potential printing, I believe is used only by
-    closing commands and the xml plugin); [terminator] is used at the
-    end of the proof to close the proof. The proof is started in the
-    evar map [sigma] (which can typically contain universe
-    constraints), and with universe bindings pl. *)
+(** [start_proof id str pl goals terminator] starts a proof of name
+   [id] with goals [goals] (a list of pairs of environment and
+   conclusion); [str] describes what kind of theorem/definition this
+   is; [terminator] is used at the end of the proof to close the proof
+   (e.g. to declare the built constructions as a coercion or a setoid
+   morphism). The proof is started in the evar map [sigma] (which can
+   typically contain universe constraints), and with universe bindings
+   pl. *)
 val start_proof :
   Evd.evar_map -> Names.Id.t -> ?pl:UState.universe_decl ->
   Decl_kinds.goal_kind -> (Environ.env * EConstr.types) list  ->