diff options
Diffstat (limited to 'tactics/rewrite.ml')
| -rw-r--r-- | tactics/rewrite.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 1245e7c29..9d9847ea5 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -2011,15 +2011,15 @@ let setoid_proof ty fn fallback = | e -> Proofview.tclORELSE fallback - begin function + begin function (e', info) -> match e' with | Hipattern.NoEquationFound -> begin match e with - | Not_found -> + | (Not_found, _) -> let rel, _, _ = decompose_app_rel env sigma concl in not_declared env ty rel - | _ -> Proofview.tclZERO e + | (e, info) -> Proofview.tclZERO ~info e end - | e' -> Proofview.tclZERO e' + | e' -> Proofview.tclZERO ~info e' end end end |