diff options
Diffstat (limited to 'proofs/proof.ml')
| -rw-r--r-- | proofs/proof.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml index 5f07cc1acc..2ee006631a 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 @@ -412,7 +412,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; } |