diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-06-11 16:45:22 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-06-11 16:45:22 -0400 |
| commit | 656f38ab96e18740df46868f31ac20814ffd6658 (patch) | |
| tree | c1c019a6712157492714994227b4f4449fd6450e | |
| parent | d8cc9e17811795caf47f7a5ab5030801a699170b (diff) | |
Another fix for an anomaly in 8.4pl2
| -rw-r--r-- | src/Specific/Ed25519.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v index 3b90b5cdf..377fb9592 100644 --- a/src/Specific/Ed25519.v +++ b/src/Specific/Ed25519.v @@ -245,7 +245,7 @@ Section Ed25519Frep. Local Ltac Let_In_unRep := match goal with | [ |- appcontext G[Let_In (unRep ?x) ?f] ] - => change (Let_In (unRep x) f) with (Let_In x (fun y => f (unRep y))); cbv beta + => let G' := context G[Let_In x (fun y => f (unRep y))] in change G'; cbv beta end. @@ -578,4 +578,4 @@ Section Ed25519Frep. reflexivity. } Unfocus. reflexivity. Defined. -End Ed25519Frep.
\ No newline at end of file +End Ed25519Frep. |