From 07d63bf9af363e4924ca14cb88b723c8ed2ea2dc Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Fri, 31 Jan 2014 15:04:44 +0100 Subject: Typos in comment. --- proofs/proofview.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'proofs') diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 2f215ba94..fed7c1dfd 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -168,11 +168,11 @@ val tclIFCATCH : 'a tactic -> ('a -> 'b tactic) -> (exn -> 'b tactic) -> 'b tact success. *) val tclONCE : 'a tactic -> 'a tactic -(* [tclONCE e t] succeeds as [t] if [t] has exactly one +(* [tclEXACTLY_ONCE e t] succeeds as [t] if [t] has exactly one success. Otherwise it fails. It may behave differently than [t] as there may be extra non-logical effects used to discover that [t] does not have a second success. Moreover the second success may be - conditional on the error recieved: [e] is used. *) + conditional on the error received: [e] is used. *) val tclEXACTLY_ONCE : exn -> 'a tactic -> 'a tactic (* Focuses a tactic at a range of subgoals, found by their indices. -- cgit v1.2.3