diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-21 19:03:14 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-21 19:03:14 +0200 |
| commit | a30a8f484a478e04a7a42526cd6994310c59521d (patch) | |
| tree | 11bc0fc3d6dd50f6de8343df0986f0ace1cb85fc | |
| parent | e8726550e01e51ef3ccf8602f2ecbe2b3737cca3 (diff) | |
Removing a nonsensical Errors.push.
| -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 90c635d1e..ed06f5162 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 |