diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-02-16 11:48:28 +0100 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-02-16 11:48:28 +0100 |
| commit | 9a7afc12e0573c74d0bb0943372dddc3c61a03f1 (patch) | |
| tree | 3ffc24d32f7f355fc0095376adb93bddcef58bb8 /tactics/tacticals.mli | |
| parent | 3960836e255e3738cabcd559cc1c133c5f30137a (diff) | |
Tacticals: typo in a comment
Diffstat (limited to 'tactics/tacticals.mli')
| -rw-r--r-- | tactics/tacticals.mli | 2 |
1 files changed, 1 insertions, 1 deletions
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 |