aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Tactics
diff options
context:
space:
mode:
Diffstat (limited to 'src/Util/Tactics')
-rw-r--r--src/Util/Tactics/ChangeInAll.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Util/Tactics/ChangeInAll.v b/src/Util/Tactics/ChangeInAll.v
index 865a723da..39a031207 100644
--- a/src/Util/Tactics/ChangeInAll.v
+++ b/src/Util/Tactics/ChangeInAll.v
@@ -1,6 +1,6 @@
(** Work around "Cannot create self-referring hypothesis" coming from
[change x with y in *] *)
-Local Ltac change_in_all from to :=
+Ltac change_in_all from to :=
change from with to;
repeat match goal with
| [ H : _ |- _ ] => progress change from with to in H