diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-10-22 14:16:48 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-10-22 14:16:48 -0400 |
| commit | f0bf0cec1aa88998fe9af99a0d9ea9311fffa703 (patch) | |
| tree | 9e7f8cadf68779684a2dac2e9def28553cb1ae2d /src/Specific/GF25519.v | |
| parent | e3b4c19f5983e277b53253fe305c3db8d1cef02b (diff) | |
final touches/fixes for freeze restructuring
Diffstat (limited to 'src/Specific/GF25519.v')
| -rw-r--r-- | src/Specific/GF25519.v | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 3ea794435..e89615dde 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -460,7 +460,6 @@ Proof. + reflexivity. Qed. -(* Definition ge_modulus_sig (f : fe25519) : { b : Z | b = ge_modulus_opt (to_list 10 f) }. Proof. @@ -485,7 +484,6 @@ Proof. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. assumption. Defined. -*) Definition freeze_sig (f : fe25519) : { f' : fe25519 | f' = from_list_default 0 10 (freeze_opt (int_width := int_width) c_ (to_list 10 f)) }. |