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

2 files changed, 14 insertions, 8 deletions

diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 4e847a5590..de020926f6 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -331,7 +331,7 @@ let initialize_named_context_for_proof () =
       let d = if variable_opacity id then NamedDecl.LocalAssum (id, NamedDecl.get_type d) else d in
       Environ.push_named_context_val d signv) sign Environ.empty_named_context_val
 
-let start_proof id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[]) hook =
+let start_proof id ?pl kind sigma ?terminator ?sign c ?(compute_guard=[]) hook =
   let terminator = match terminator with
   | None -> standard_proof_terminator compute_guard hook
   | Some terminator -> terminator compute_guard hook
@@ -341,19 +341,21 @@ let start_proof id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=
     | Some sign -> sign
     | None -> initialize_named_context_for_proof ()
   in
-  Pfedit.start_proof id ?pl kind sigma sign c ?init_tac terminator
+  let goals = [ Global.env_of_context sign , c ] in
+  Proof_global.start_proof sigma id ?pl kind goals terminator
 
-let start_proof_univs id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[]) hook =
+let start_proof_univs id ?pl kind sigma ?terminator ?sign c ?(compute_guard=[]) hook =
   let terminator = match terminator with
   | None -> universe_proof_terminator compute_guard hook
   | Some terminator -> terminator compute_guard hook
   in
-  let sign = 
+  let sign =
     match sign with
     | Some sign -> sign
     | None -> initialize_named_context_for_proof ()
   in
-  Pfedit.start_proof id ?pl kind sigma sign c ?init_tac terminator
+  let goals = [ Global.env_of_context sign , c ] in
+  Proof_global.start_proof sigma id ?pl kind goals terminator
 
 let rec_tac_initializer finite guard thms snl =
   if finite then
@@ -404,7 +406,11 @@ let start_proof_with_initialization kind sigma decl recguard thms snl hook =
         List.iter (fun (strength,ref,imps) ->
 	  maybe_declare_manual_implicits false ref imps;
 	  call_hook (fun exn -> exn) hook strength ref) thms_data in
-      start_proof_univs id ~pl:decl kind sigma t ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard
+      start_proof_univs id ~pl:decl kind sigma t (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard;
+      ignore (Proof_global.with_current_proof (fun _ p ->
+          match init_tac with
+          | None -> p,(true,[])
+          | Some tac -> Proof.run_tactic Global.(env ()) tac p))
 
 let start_proof_com ?inference_hook kind thms hook =
   let env0 = Global.env () in
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 195fcbf4ca..246d8cbe6d 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -18,13 +18,13 @@ val call_hook : Future.fix_exn -> declaration_hook -> Decl_kinds.locality -> Glo
 val start_proof : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map ->
   ?terminator:(Proof_global.lemma_possible_guards -> declaration_hook -> Proof_global.proof_terminator) ->
   ?sign:Environ.named_context_val -> EConstr.types ->
-  ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards ->
+  ?compute_guard:Proof_global.lemma_possible_guards ->
   declaration_hook -> unit
 
 val start_proof_univs : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map ->
   ?terminator:(Proof_global.lemma_possible_guards -> (UState.t option -> declaration_hook) -> Proof_global.proof_terminator) ->
   ?sign:Environ.named_context_val -> EConstr.types ->
-  ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards ->
+  ?compute_guard:Proof_global.lemma_possible_guards ->
   (UState.t option -> declaration_hook) -> unit
 
 val start_proof_com :