diff options
Diffstat (limited to 'src/SpecificGen/GF25519_64Reflective/Common.v')
| -rw-r--r-- | src/SpecificGen/GF25519_64Reflective/Common.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/SpecificGen/GF25519_64Reflective/Common.v b/src/SpecificGen/GF25519_64Reflective/Common.v index f639aa0b6..c7b1a69fb 100644 --- a/src/SpecificGen/GF25519_64Reflective/Common.v +++ b/src/SpecificGen/GF25519_64Reflective/Common.v @@ -327,8 +327,8 @@ Ltac assoc_right_tuple x so_far := Local Ltac make_args x := let x' := fresh "x'" in compute in x |- *; - let t := match type of x with @expr _ _ _ _ (Tflat _ ?t) => t end in - let t' := match goal with |- @expr _ _ _ _ (Tflat _ ?t) => t end in + let t := match type of x with @expr _ _ _ _ (Tflat ?t) => t end in + let t' := match goal with |- @expr _ _ _ _ (Tflat ?t) => t end in refine (LetIn (UnReturn x) _); let x'' := fresh "x''" in intro x''; |