diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-09-06 11:20:42 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-09-06 11:20:59 -0400 |
| commit | e79aa03ae5575cf37065894c198a8b3ca8372cea (patch) | |
| tree | 98fc38af585af75539251a0d8171a880880e6f11 /src/Specific/GF25519.v | |
| parent | de58a46d929f334fc20ae0a63ddbdf867d3fb9fc (diff) | |
make 8.4 happier
Diffstat (limited to 'src/Specific/GF25519.v')
| -rw-r--r-- | src/Specific/GF25519.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 2816a07cc..74d722c57 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -370,7 +370,7 @@ Proof. rewrite !modulus_digits_subst. cbv - [from_list_default]. rewrite Let_In_push. - repeat (erewrite Let_In_ext; [ | + do 20 (erewrite Let_In_ext; [ | repeat match goal with | |- _ => progress intros; try apply Let_In_ext | |- _ = from_list_default _ _ (Let_In _ _) => etransitivity; try (rewrite Let_In_push; reflexivity) |