diff options
| -rw-r--r-- | tactics/rewrite.ml | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 90c635d1eb..ed06f5162b 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -2040,10 +2040,6 @@ let setoid_proof ty fn fallback = fallback begin function | Hipattern.NoEquationFound -> - (* spiwack: [Errors.push] here is unlikely to do what - it's intended to, or anything meaningful for that - matter. *) - let e = Errors.push e in begin match e with | Not_found -> let rel, args = decompose_app_rel env sigma concl in |