From 1f000d19cfd38f3caf942b606203b6740fbcf768 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 11 Nov 2016 14:18:42 -0500 Subject: Fix for Coq 8.4 Tactic notations in sections are automatically local --- src/Util/WordUtil.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/Util/WordUtil.v') diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v index 58917dff5..745dde17c 100644 --- a/src/Util/WordUtil.v +++ b/src/Util/WordUtil.v @@ -473,7 +473,7 @@ Section WordToN. reflexivity. Qed. - Local Tactic Notation "replaceAt1" constr(x) "with" constr(y) "by" tactic(tac) := + Tactic Notation "replaceAt1" constr(x) "with" constr(y) "by" tactic(tac) := let tmp := fresh in set (tmp := x) at 1; replace tmp with y by (unfold tmp; tac); -- cgit v1.2.3