diff options
| -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. |