From a30a8f484a478e04a7a42526cd6994310c59521d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 21 Sep 2014 19:03:14 +0200
Subject: Removing a nonsensical Errors.push.

---
 tactics/rewrite.ml | 4 ----
 1 file changed, 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
-- 
cgit v1.2.3