diff options
Diffstat (limited to 'proofs/proofview.ml')
| -rw-r--r-- | proofs/proofview.ml | 51 |
1 files changed, 21 insertions, 30 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 6f626341..4fc0c164 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} *) @@ -648,7 +651,7 @@ let goodmod p m = let cycle n = let open Proof in - InfoL.leaf (Info.Tactic (fun () -> Pp.(str"cycle"++spc()++int n))) >> + InfoL.leaf (Info.Tactic (fun () -> Pp.(str"cycle "++int n))) >> Comb.modify begin fun initial -> let l = CList.length initial in let n' = goodmod n l in @@ -658,7 +661,7 @@ let cycle n = let swap i j = let open Proof in - InfoL.leaf (Info.Tactic (fun () -> Pp.(str"swap"++spc()++int i++spc()++int j))) >> + InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"swap"++spc()++int i++spc()++int j)))) >> Comb.modify begin fun initial -> let l = CList.length initial in let i = if i>0 then i-1 else i and j = if j>0 then j-1 else j in @@ -722,19 +725,7 @@ let give_up = module Progress = struct - (** equality function up to evar instantiation in heterogeneous - contexts. *) - (* spiwack (2015-02-19): In the previous version of progress an - equality which considers two universes equal when it is consistent - tu unify them ([Evd.eq_constr_univs_test]) was used. Maybe this - behaviour has to be restored as well. This has to be established by - practice. *) - - let rec eq_constr sigma1 sigma2 t1 t2 = - Constr.equal_with - (fun t -> Evarutil.kind_of_term_upto sigma1 t) - (fun t -> Evarutil.kind_of_term_upto sigma2 t) - t1 t2 + let eq_constr = Evarutil.eq_constr_univs_test (** equality function on hypothesis contexts *) let eq_named_context_val sigma1 sigma2 ctx1 ctx2 = @@ -1069,7 +1060,7 @@ struct let comb = undefined sigma (CList.rev evs) in let sigma = CList.fold_left Unsafe.mark_as_goal_evm sigma comb in let open Proof in - InfoL.leaf (Info.Tactic (fun () -> Pp.(str"refine"++spc()++ Hook.get pr_constrv env sigma c))) >> + InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"refine"++spc()++ Hook.get pr_constrv env sigma c)))) >> Pv.set { solution = sigma; comb; } end |