[vernac] Remove stale bool parameter from `VernacStartTheoremProof`

`VernacStartTheoremProof` contained a stale bool parameter from 15
years ago, which is unused today.

7 files changed, 9 insertions, 13 deletions

diff --git a/API/API.mli b/API/API.mli
index 1e078bb77..9f13f51fc 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -2407,7 +2407,7 @@ sig
   | VernacNotationAddFormat of string * string * string
   | VernacDefinition of
       (Decl_kinds.locality option * Decl_kinds.definition_object_kind) * plident * definition_expr
-  | VernacStartTheoremProof of Decl_kinds.theorem_kind * proof_expr list * bool
+  | VernacStartTheoremProof of Decl_kinds.theorem_kind * proof_expr list
   | VernacEndProof of proof_end
   | VernacExactProof of Constrexpr.constr_expr
   | VernacAssumption of (Decl_kinds.locality option * Decl_kinds.assumption_object_kind) *
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index 7c12f9df5..31ec44470 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -331,7 +331,7 @@ type vernac_expr =
   (* Gallina *)
   | VernacDefinition of
       (locality option * definition_object_kind) * plident * definition_expr
-  | VernacStartTheoremProof of theorem_kind * proof_expr list * bool
+  | VernacStartTheoremProof of theorem_kind * proof_expr list
   | VernacEndProof of proof_end
   | VernacExactProof of constr_expr
   | VernacAssumption of (locality option * assumption_object_kind) *
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index dbd2fc401..fe8f517a7 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -151,7 +151,7 @@ GEXTEND Gram
         l = LIST0
           [ "with"; id = pidentref; bl = binders; ":"; c = lconstr ->
           (Some id,(bl,c)) ] ->
-          VernacStartTheoremProof (thm, (Some id,(bl,c))::l, false)
+          VernacStartTheoremProof (thm, (Some id,(bl,c))::l)
       | stre = assumption_token; nl = inline; bl = assum_list ->
 	  VernacAssumption (stre, nl, bl)
       | (kwd,stre) = assumptions_token; nl = inline; bl = assum_list ->
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 4a5cfe630..d0536a174 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -698,7 +698,7 @@ open Decl_kinds
               | Some cc -> str" :=" ++ spc() ++ cc))
         )
 
-      | VernacStartTheoremProof (ki,l,_) ->
+      | VernacStartTheoremProof (ki,l) ->
         return (
           hov 1 (pr_statement (pr_thm_token ki) (List.hd l) ++
                    prlist (pr_statement (spc () ++ keyword "with")) (List.tl l))
diff --git a/stm/stm.ml b/stm/stm.ml
index 071d2edf9..81bac6a1f 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -476,7 +476,7 @@ end = struct (* {{{ *)
   let mk_branch_name { expr = x } = Branch.make
     (let rec aux x = match x with
     | VernacDefinition (_,((_,i),_),_) -> Names.string_of_id i
-    | VernacStartTheoremProof (_,[Some ((_,i),_),_],_) -> Names.string_of_id i
+    | VernacStartTheoremProof (_,[Some ((_,i),_),_]) -> Names.string_of_id i
     | VernacTime (_, e)
     | VernacTimeout (_, e) -> aux e
     | _ -> "branch" in aux x)
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 1234e15af..50e68852f 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -115,7 +115,7 @@ let rec classify_vernac e =
         VtStartProof(default_proof_mode (),Doesn'tGuaranteeOpacity,[i]), VtLater
     | VernacDefinition (_,((_,i),_),ProveBody _) ->
         VtStartProof(default_proof_mode (),GuaranteesOpacity,[i]), VtLater
-    | VernacStartTheoremProof (_,l,_) ->
+    | VernacStartTheoremProof (_,l) ->
         let ids = 
           CList.map_filter (function (Some ((_,i),pl), _) -> Some i | _ -> None) l in
         VtStartProof (default_proof_mode (),GuaranteesOpacity,ids), VtLater
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 21f053fb9..acd218536 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -490,17 +490,13 @@ let vernac_definition locality p (local,k) ((loc,id as lid),pl) def =
  		Some (snd (Hook.get f_interp_redexp env evc r)) in
 	do_definition id (local,p,k) pl bl red_option c typ_opt hook)
 
-let vernac_start_proof locality p kind l lettop =
+let vernac_start_proof locality p kind l =
   let local = enforce_locality_exp locality None in
   if Dumpglob.dump () then
     List.iter (fun (id, _) ->
       match id with
 	| Some (lid,_) -> Dumpglob.dump_definition lid false "prf"
 	| None -> ()) l;
-  if not(Proof_global.there_are_pending_proofs ()) then
-    if lettop then
-      user_err ~hdr:"Vernacentries.StartProof"
-	(str "Let declarations can only be used in proof editing mode.");
   start_proof_and_print (local, p, Proof kind) l no_hook
 
 let vernac_end_proof ?proof = function
@@ -1937,7 +1933,7 @@ let interp ?proof ?loc locality poly c =
 
   (* Gallina *)
   | VernacDefinition (k,lid,d) -> vernac_definition locality poly k lid d
-  | VernacStartTheoremProof (k,l,top) -> vernac_start_proof locality poly k l top
+  | VernacStartTheoremProof (k,l) -> vernac_start_proof locality poly k l
   | VernacEndProof e -> vernac_end_proof ?proof e
   | VernacExactProof c -> vernac_exact_proof c
   | VernacAssumption (stre,nl,l) -> vernac_assumption locality poly stre l nl
@@ -2025,7 +2021,7 @@ let interp ?proof ?loc locality poly c =
   | VernacComments l -> if_verbose Feedback.msg_info (str "Comments ok\n")
 
   (* Proof management *)
-  | VernacGoal t -> vernac_start_proof locality poly Theorem [None,([],t)] false
+  | VernacGoal t -> vernac_start_proof locality poly Theorem [None,([],t)]
   | VernacFocus n -> vernac_focus n
   | VernacUnfocus -> vernac_unfocus ()
   | VernacUnfocused -> vernac_unfocused ()