From 5562729887f61affeb12c5566f1b26eaf2727893 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Wed, 5 Apr 2017 02:51:16 -0400
Subject: Add Tactics.ChangeInAll

---
 src/Util/Curry.v | 10 ++--------
 1 file changed, 2 insertions(+), 8 deletions(-)

(limited to 'src/Util/Curry.v')

diff --git a/src/Util/Curry.v b/src/Util/Curry.v
index 8a34cb611..d1e3a7b94 100644
--- a/src/Util/Curry.v
+++ b/src/Util/Curry.v
@@ -1,14 +1,8 @@
+Require Import Crypto.Util.Tactics.ChangeInAll.
+
 Definition curry2 {A B C} (f : A -> B -> C) (x : A * B) : C
 := let '(a, b) := x in f a b.
 
-(** Work around "Cannot create self-referring hypothesis" coming from
-    [change x with y in *] *)
-Local Ltac change_in_all from to :=
-  change from with to;
-  repeat match goal with
-         | [ H : _ |- _ ] => progress change from with to in H
-         end.
-
 Ltac change_with_curried f :=
   cbv beta in f; (* work around https://coq.inria.fr/bugs/show_bug.cgi?id=5430 *)
   lazymatch type of f with
-- 
cgit v1.2.3