diff options
-rw-r--r-- | API/API.mli | 2 | ||||
-rw-r--r-- | intf/vernacexpr.ml | 2 | ||||
-rw-r--r-- | parsing/g_vernac.ml4 | 2 | ||||
-rw-r--r-- | printing/ppvernac.ml | 2 | ||||
-rw-r--r-- | stm/stm.ml | 2 | ||||
-rw-r--r-- | stm/vernac_classifier.ml | 2 | ||||
-rw-r--r-- | vernac/vernacentries.ml | 10 |
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 () |