diff options
| -rw-r--r-- | tactics/tacinterp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index c749e2d720..9d8bc68431 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1243,7 +1243,7 @@ and interp_match_successes lz ist s : typed_generic_argument GTac.t = match peek t with | Nil -> Proofview.tclZERO e | Cons (t1,t') -> - Proofview.tclORELSE + Proofview.tclOR (interp_match_success ist t1) begin fun e -> (* Honors Ltac's failure level. *) |