diff options
Diffstat (limited to 'proofs/proof.ml')
| -rw-r--r-- | proofs/proof.ml | 17 |
1 files changed, 6 insertions, 11 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml index 5f07cc1acc..e9f93d0c8f 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -19,7 +19,7 @@ - Focus: a proof has a focus stack: the top of the stack contains the context in which to unfocus the current view to a view focused with the rest of the stack. - In addition, this contains, for each of the focus context, a + In addition, this contains, for each of the focus context, a "focus kind" and a "focus condition" (in practice, and for modularity, the focus kind is actually stored inside the condition). To unfocus, one needs to know the focus kind, and the condition (for instance "no condition" or @@ -179,7 +179,7 @@ let cond_of_focus pr = | (cond,_,_)::_ -> cond | _ -> raise FullyUnfocused -(* An auxiliary function to pop and read the last {!Proofview.focus_context} +(* An auxiliary function to pop and read the last {!Proofview.focus_context} on the focus stack. *) let pop_focus pr = match pr.focus_stack with @@ -202,7 +202,7 @@ let _unfocus pr = { pr with proofview = Proofview.unfocus fc pr.proofview } (* Focus command (focuses on the [i]th subgoal) *) -(* spiwack: there could also, easily be a focus-on-a-range tactic, is there +(* spiwack: there could also, easily be a focus-on-a-range tactic, is there a need for it? *) let focus cond inf i pr = try _focus cond (Obj.repr inf) i i pr @@ -250,7 +250,7 @@ let rec unfocus kind pr () = | Loose -> begin try let pr = _unfocus pr in - unfocus kind pr () + unfocus kind pr () with FullyUnfocused -> raise CannotUnfocusThisWay end @@ -386,12 +386,7 @@ let run_tactic env tac pr = let sigma = Proofview.return proofview in let to_shelve = undef sigma to_shelve in let shelf = (undef sigma pr.shelf)@retrieved@to_shelve in - let proofview = - List.fold_left - Proofview.Unsafe.mark_as_unresolvable - proofview - to_shelve - in + let proofview = Proofview.Unsafe.mark_as_unresolvables proofview to_shelve in let given_up = pr.given_up@give_up in let proofview = Proofview.Unsafe.reset_future_goals proofview in { pr with proofview ; shelf ; given_up },(status,info_trace),result @@ -412,7 +407,7 @@ module V82 = struct let top_goal p = let { Evd.it=gls ; sigma=sigma; } = - Proofview.V82.top_goals p.entry p.proofview + Proofview.V82.top_goals p.entry p.proofview in { Evd.it=List.hd gls ; sigma=sigma; } |