diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-11 14:18:42 -0500 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2016-11-11 14:45:17 -0500 |
| commit | 1f000d19cfd38f3caf942b606203b6740fbcf768 (patch) | |
| tree | db02f1563b2225235a1666fef8f422b81060ebf9 /src/Util/WordUtil.v | |
| parent | 1ce3512d0e1b6761868b1c6234424cbb82a65d22 (diff) | |
Fix for Coq 8.4
Tactic notations in sections are automatically local
Diffstat (limited to 'src/Util/WordUtil.v')
| -rw-r--r-- | src/Util/WordUtil.v | 2 |
1 files changed, 1 insertions, 1 deletions
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); |