diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-01-19 14:05:54 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-01-19 14:05:54 -0500 |
| commit | cded6731f79a66018d3660017bda7a284aedf50c (patch) | |
| tree | 1311ed7d6d0bf9a06a5ad86531a708de4e95e19d /src/SpecificGen/GF25519_32Reflective | |
| parent | cb98e6d8a45b68e29546732a0eed969c724a0274 (diff) | |
Split out Reflection.Equality, change Tflat implicit argument
Diffstat (limited to 'src/SpecificGen/GF25519_32Reflective')
| -rw-r--r-- | src/SpecificGen/GF25519_32Reflective/Common.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/SpecificGen/GF25519_32Reflective/Common.v b/src/SpecificGen/GF25519_32Reflective/Common.v index aad67f032..644ed7c92 100644 --- a/src/SpecificGen/GF25519_32Reflective/Common.v +++ b/src/SpecificGen/GF25519_32Reflective/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''; |