diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2015-10-26 00:54:22 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2015-10-28 21:36:21 -0400 |
| commit | 2cb694b68c8d28b2049936f1c20349200eb121c2 (patch) | |
| tree | 212c95a537700b0503a7785330d2274f71662229 /src/Curves | |
| parent | a7a2d882691af1cddd729f1f871c467900b9ac4e (diff) | |
remove resolved todo
Diffstat (limited to 'src/Curves')
| -rw-r--r-- | src/Curves/PointFormats.v | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/src/Curves/PointFormats.v b/src/Curves/PointFormats.v index baa6bd2a7..8ab81e0a8 100644 --- a/src/Curves/PointFormats.v +++ b/src/Curves/PointFormats.v @@ -66,8 +66,6 @@ Module PointFormats. Parameter projY : point -> GF. Parameter unifiedAdd : point -> point -> point. - (* TODO: split module here? *) - Parameter rep : point -> Spec.point -> Prop. Local Notation "P '~=' rP" := (rep P rP) (at level 70). Axiom mkPoint_rep: forall x y, mkPoint x y ~= Spec.mkPoint x y. |