diff --git a/third_party/fiat/curve25519.c b/third_party/fiat/curve25519.c
index 1374a77..2e56450 100644
--- a/third_party/fiat/curve25519.c
+++ b/third_party/fiat/curve25519.c
@@ -281,13 +281,6 @@
 
 // h = f + g
 // Can overlap h with f or g.
-//
-// Preconditions:
-//    |f| bounded by 1.1*2^25,1.1*2^24,1.1*2^25,1.1*2^24,etc.
-//    |g| bounded by 1.1*2^25,1.1*2^24,1.1*2^25,1.1*2^24,etc.
-//
-// Postconditions:
-//    |h| bounded by 1.1*2^26,1.1*2^25,1.1*2^26,1.1*2^25,etc.
 static void fe_add(fe_loose *h, const fe *f, const fe *g) {
   assert_fe(f->v);
   assert_fe(g->v);
@@ -331,13 +324,6 @@
 
 // h = f - g
 // Can overlap h with f or g.
-//
-// Preconditions:
-//    |f| bounded by 1.1*2^25,1.1*2^24,1.1*2^25,1.1*2^24,etc.
-//    |g| bounded by 1.1*2^25,1.1*2^24,1.1*2^25,1.1*2^24,etc.
-//
-// Postconditions:
-//    |h| bounded by 1.1*2^26,1.1*2^25,1.1*2^26,1.1*2^25,etc.
 static void fe_sub(fe_loose *h, const fe *f, const fe *g) {
   assert_fe(f->v);
   assert_fe(g->v);
@@ -766,12 +752,6 @@
 }
 
 // h = -f
-//
-// Preconditions:
-//    |f| bounded by 1.1*2^25,1.1*2^24,1.1*2^25,1.1*2^24,etc.
-//
-// Postconditions:
-//    |h| bounded by 1.1*2^25,1.1*2^24,1.1*2^25,1.1*2^24,etc.
 static void fe_neg(fe_loose *h, const fe *f) {
   assert_fe(f->v);
   fe_neg_impl(h->v, f->v);
@@ -794,9 +774,6 @@
 
 // return 0 if f == 0
 // return 1 if f != 0
-//
-// Preconditions:
-//    |f| bounded by 1.1*2^26,1.1*2^25,1.1*2^26,1.1*2^25,etc.
 static int fe_isnonzero(const fe_loose *f) {
   uint8_t s[32];
   fe_loose_tobytes(s, f);
@@ -807,9 +784,6 @@
 
 // return 1 if f is in {1,3,5,...,q-2}
 // return 0 if f is in {0,2,4,...,q-1}
-//
-// Preconditions:
-//    |f| bounded by 1.1*2^26,1.1*2^25,1.1*2^26,1.1*2^25,etc.
 static int fe_isnegative(const fe *f) {
   uint8_t s[32];
   fe_tobytes(s, f);
diff --git a/third_party/fiat/internal.h b/third_party/fiat/internal.h
index 54a93a5..0533d27 100644
--- a/third_party/fiat/internal.h
+++ b/third_party/fiat/internal.h
@@ -56,17 +56,17 @@
 // Addition and subtraction produce fe_loose from (fe, fe).
 typedef struct fe_loose { uint32_t v[10]; } fe_loose;
 
-/* ge means group element.
-
- * Here the group is the set of pairs (x,y) of field elements (see fe.h)
- * satisfying -x^2 + y^2 = 1 + d x^2y^2
- * where d = -121665/121666.
- *
- * Representations:
- *   ge_p2 (projective): (X:Y:Z) satisfying x=X/Z, y=Y/Z
- *   ge_p3 (extended): (X:Y:Z:T) satisfying x=X/Z, y=Y/Z, XY=ZT
- *   ge_p1p1 (completed): ((X:Z),(Y:T)) satisfying x=X/Z, y=Y/T
- *   ge_precomp (Duif): (y+x,y-x,2dxy) */
+// ge means group element.
+//
+// Here the group is the set of pairs (x,y) of field elements (see fe.h)
+// satisfying -x^2 + y^2 = 1 + d x^2y^2
+// where d = -121665/121666.
+//
+// Representations:
+//   ge_p2 (projective): (X:Y:Z) satisfying x=X/Z, y=Y/Z
+//   ge_p3 (extended): (X:Y:Z:T) satisfying x=X/Z, y=Y/Z, XY=ZT
+//   ge_p1p1 (completed): ((X:Z),(Y:T)) satisfying x=X/Z, y=Y/T
+//   ge_precomp (Duif): (y+x,y-x,2dxy)
 
 typedef struct {
   fe X;