From 9a7afc12e0573c74d0bb0943372dddc3c61a03f1 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 16 Feb 2016 11:48:28 +0100 Subject: Tacticals: typo in a comment --- tactics/tacticals.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tactics/tacticals.mli') diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index ffcc71b45..0f926468b 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -147,7 +147,7 @@ val case_on_ba : (branch_assumptions -> tactic) -> branch_args -> tactic semantics as the similarly named tacticals in [Proofview]. The tactical of [Proofview] are used in the definition of the tacticals of [Tacticals.New], but they are more atomic. In - particular [Tacticals.New.tclORELSE] sees like of progress as a + particular [Tacticals.New.tclORELSE] sees lack of progress as a failure, whereas [Proofview.tclORELSE] doesn't. Additionally every tactic which can catch failure ([tclOR], [tclORELSE], [tclTRY], [tclREPEAt], etc…) are run into each goal independently (failures -- cgit v1.2.3