diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-02-07 14:03:23 -0500 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-02-07 14:03:23 -0500 |
| commit | 996fe81ecfa5d8dfa89d2d61c1e94fd15fe9a911 (patch) | |
| tree | 129e8fd8f20063e95b6e7e1b86ebdf70b385f287 /src/Specific | |
| parent | 50d521721412c0483e6833707af4c8dc7978aeff (diff) | |
remove a dangling About
Diffstat (limited to 'src/Specific')
| -rw-r--r-- | src/Specific/GF25519.v | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 732779a1a..7ef2f0aaf 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -289,7 +289,6 @@ Proof. cbv [cap Base25Point5_10limbs.base]. intros. rewrite map_length in *. - About map_nth_default. erewrite map_nth_default; [|assumption]. instantiate (2 := 0%Z). (** For the division of maps of (2 ^ _) over lists, replace it with 2 ^ (_ - _) *) |