diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:35:43 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:35:43 +0000 |
| commit | 386d36deb6efb755cdd16ad216361e01e0b7662e (patch) | |
| tree | ad4a3063b901c508d759f9a9b9660a1e04dc1c3d /proofs/pfedit.ml | |
| parent | e6404437c1f6ae451f4253cd3450f75513b395c3 (diff) | |
Adds a new goal selector "all:".
all:tac applies tac to all the focused subgoals.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16982 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/pfedit.ml')
| -rw-r--r-- | proofs/pfedit.ml | 18 |
1 files changed, 12 insertions, 6 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 6c0ddfc11..5d053e4c8 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -90,19 +90,25 @@ let current_proof_statement () = | (id,([concl],strength,hook)) -> id,strength,concl,hook | _ -> Errors.anomaly ~label:"Pfedit.current_proof_statement" (Pp.str "more than one statement") -let solve_nth ?with_end_tac gi tac pr = +let solve ?with_end_tac gi tac pr = try let tac = match with_end_tac with | None -> tac | Some etac -> Proofview.tclTHEN tac etac in - Proof.run_tactic (Global.env ()) (Proofview.tclFOCUS gi gi tac) pr + let tac = match gi with + | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i tac + | Vernacexpr.SelectAll -> tac + in + Proof.run_tactic (Global.env ()) tac pr with | Proof_global.NoCurrentProof -> Errors.error "No focused proof" - | Proofview.IndexOutOfRange -> - let msg = str "No such goal: " ++ int gi ++ str "." in - Errors.errorlabstrm "" msg + | Proofview.IndexOutOfRange -> + match gi with + | Vernacexpr.SelectNth i -> let msg = str "No such goal: " ++ int i ++ str "." in + Errors.errorlabstrm "" msg + | _ -> assert false -let by tac = Proof_global.with_current_proof (fun _ -> solve_nth 1 tac) +let by tac = Proof_global.with_current_proof (fun _ -> solve (Vernacexpr.SelectNth 1) tac) let instantiate_nth_evar_com n com = Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.instantiate_evar n com p) |