diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/pfedit.ml | 3 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 1 | ||||
| -rw-r--r-- | proofs/proofview.ml | 17 | ||||
| -rw-r--r-- | proofs/proofview.mli | 2 |
4 files changed, 22 insertions, 1 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 49195aecce..1b0b2f401b 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -94,6 +94,7 @@ let solve ?with_end_tac gi tac pr = | Some etac -> Proofview.tclTHEN tac etac in let tac = match gi with | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i tac + | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id tac | Vernacexpr.SelectAll -> tac | Vernacexpr.SelectAllParallel -> Errors.anomaly(str"SelectAllParallel not handled by Stm") @@ -101,7 +102,7 @@ let solve ?with_end_tac gi tac pr = Proof.run_tactic (Global.env ()) tac pr with | Proof_global.NoCurrentProof -> Errors.error "No focused proof" - | Proofview.IndexOutOfRange -> + | Proofview.IndexOutOfRange -> match gi with | Vernacexpr.SelectNth i -> let msg = str "No such goal: " ++ int i ++ str "." in Errors.errorlabstrm "" msg diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 82e176f970..1994922a97 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -528,6 +528,7 @@ let get_default_goal_selector () = !default_goal_selector let print_goal_selector = function | Vernacexpr.SelectAll -> "all" | Vernacexpr.SelectNth i -> string_of_int i + | Vernacexpr.SelectId id -> Id.to_string id | Vernacexpr.SelectAllParallel -> "par" let parse_goal_selector = function diff --git a/proofs/proofview.ml b/proofs/proofview.ml index a5cb2edb85..bc6ce4fc64 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -330,6 +330,23 @@ let tclFOCUS_gen nosuchgoal i j t = let tclFOCUS i j t = tclFOCUS_gen (tclZERO (NoSuchGoals (j+1-i))) i j t let tclTRYFOCUS i j t = tclFOCUS_gen (tclUNIT ()) i j t +let tclFOCUSID id t = + let (>>=) = Proof.bind in + let (>>) = Proof.seq in + Proof.get >>= fun initial -> + let rec aux n = function + | [] -> tclZERO (NoSuchGoals 1) + | g::l -> + if Names.Id.equal (Goal.goal_ident initial.solution g) id then + let (focused,context) = focus n n initial in + Proof.set focused >> + t >>= fun result -> + Proof.modify (fun next -> unfocus context next) >> + Proof.ret result + else + aux (n+1) l in + aux 1 initial.comb + (* Dispatch tacticals are used to apply a different tactic to each goal under consideration. They come in two flavours: diff --git a/proofs/proofview.mli b/proofs/proofview.mli index b1ff30ee9b..3b2dd7ccd5 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -197,6 +197,8 @@ val tclEXACTLY_ONCE : exn -> 'a tactic -> 'a tactic exception NoSuchGoals of int val tclFOCUS : int -> int -> 'a tactic -> 'a tactic +val tclFOCUSID : Names.Id.t -> 'a tactic -> 'a tactic + (* Focuses a tactic at a range of subgoals, found by their indices. The other goals are restored to the focus when the tactic is done. |