diff options
Diffstat (limited to 'proofs/proofview.ml')
| -rw-r--r-- | proofs/proofview.ml | 31 |
1 files changed, 17 insertions, 14 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index de6d605670..4fc0c164e3 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -384,20 +384,23 @@ let tclTRYFOCUS i j t = tclFOCUS_gen (tclUNIT ()) i j t let tclFOCUSID id t = let open Proof in Pv.get >>= fun initial -> - let rec aux n = function - | [] -> tclZERO (NoSuchGoals 1) - | g::l -> - if Names.Id.equal (Evd.evar_ident g initial.solution) id then - let (focused,context) = focus n n initial in - Pv.set focused >> - t >>= fun result -> - Pv.modify (fun next -> unfocus context next) >> - return result - else - aux (n+1) l in - aux 1 initial.comb - - + try + let ev = Evd.evar_key id initial.solution in + try + let n = CList.index Evar.equal ev initial.comb in + (* goal is already under focus *) + let (focused,context) = focus n n initial in + Pv.set focused >> + t >>= fun result -> + Pv.modify (fun next -> unfocus context next) >> + return result + with Not_found -> + (* otherwise, save current focus and work purely on the shelve *) + Comb.set [ev] >> + t >>= fun result -> + Comb.set initial.comb >> + return result + with Not_found -> tclZERO (NoSuchGoals 1) (** {7 Dispatching on goals} *) |