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

5 files changed, 24 insertions, 39 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  ->
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 :