diff options
| -rw-r--r-- | tactics/tacticals.ml | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 224762e0a7..574e4c9a92 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -389,7 +389,14 @@ module New = struct tactical, we may consider wrapping the first argument with [tclPROGRESS]. It strikes me as a bad idea, but consistency can be considered valuable. *) - let tclOR = Proofview.Notations.(<+>) + let tclOR t1 t2 = + tclINDEPENDENT begin + Proofview.tclOR + t1 + begin fun e -> + catch_failerror e <*> t2 + end + end let tclORELSE0 t1 t2 = tclINDEPENDENT begin |