diff options
author | 2016-01-05 18:46:38 -0500 | |
---|---|---|
committer | 2016-01-05 18:46:38 -0500 | |
commit | 71553f59573301744c7d34aeec6a371ee50a65cf (patch) | |
tree | 6bb930f9ac3c1be4613114bc9c70f8095e6af4b9 /src/Specific/GF25519.v | |
parent | d4a2d4a57bb691e0129c1697e09e91c9aafe7d1c (diff) | |
parent | 67c5d4150007e268ce7b314af1981d4a00079f07 (diff) |
Merge branch 'master' of github.mit.edu:plv/fiat-crypto
Diffstat (limited to 'src/Specific/GF25519.v')
-rw-r--r-- | src/Specific/GF25519.v | 31 |
1 files changed, 0 insertions, 31 deletions
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index d30d1f7fe..235c34a9b 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -304,37 +304,6 @@ Section GF25519Base25Point5Formula. clear HmulRef Hh Hf Hg. existsFromEquations r. split; auto; congruence. - - (* Here's the tactic code I added at this point at the end of the old version. - * Erase after reading, since it isn't needed anymore. - - replace ([r0; r1; r2; r3; r4; r5; r6; r7; r8; r9]) with r; unfold rep; auto. - - subst r. - - Ltac rsubstBoth := repeat (match goal with [ |- ?a = ?b] => subst a; subst b; repeat progress f_equal || reflexivity end). - Ltac t := f_equal; abstract rsubstBoth || (try t). - - Time t. - - - (* But there's a nicer way! *) - Undo 2. - - (* This tactic finds an [x := e] hypothesis and adds a matching [x = e] hypothesis. *) - Ltac letToEquality := - match goal with - | [ x := ?e |- _ ] => - match goal with - | [ _ : x = e |- _ ] => fail 1 (* To avoid infinite loop, make sure we didn't already do this one! *) - | _ => assert (x = e) by reflexivity - end - end. - - (* Repeated introduction of those equalities enables [congruence] to solve the goal. *) - Ltac smarter_congruence := repeat letToEquality; congruence. - - Time smarter_congruence.*) Defined. End GF25519Base25Point5Formula. |