diff --git a/src/field_5x52_int128_impl.h b/src/field_5x52_int128_impl.h
index e288617aa2..10095964a2 100644
--- a/src/field_5x52_int128_impl.h
+++ b/src/field_5x52_int128_impl.h
@@ -6,22 +6,6 @@
 #include "int128.h"
 #include "util.h"
 
-/* Autogenerated: 'src/ExtractionOCaml/dettman_multiplication' --inline --static
- * --use-value-barrier secp256k1_dettman 64 5 48 2 '2^256 - 4294968273' mul
- * square */
-/* curve description: secp256k1_dettman */
-/* machine_wordsize = 64 (from "64") */
-/* requested operations: mul, square */
-/* n = 5 (from "5") */
-/* last_limb_width = 48 (from "48") */
-/* last_reduction = 2 (from "2") */
-/* s-c = 2^256 - [(1, 4294968273)] (from "2^256 - 4294968273") */
-/* inbounds_multiplier: None (from "") */
-/*  */
-/* Computed values: */
-/*  */
-/*  */
-
 #if defined(__GNUC__) || defined(__clang__)
 #  define FIAT_SECP256K1_DETTMAN_FIAT_EXTENSION __extension__
 #  define FIAT_SECP256K1_DETTMAN_FIAT_INLINE __inline__
@@ -30,16 +14,6 @@
 #  define FIAT_SECP256K1_DETTMAN_FIAT_INLINE
 #endif
 
-FIAT_SECP256K1_DETTMAN_FIAT_EXTENSION typedef secp256k1_uint128
-    fiat_secp256k1_dettman_uint128;
-
-#define secp256k1_fe_sqr_inner fiat_secp256k1_dettman_square
-#define secp256k1_fe_mul_inner fiat_secp256k1_dettman_mul
-
-#if (-1 & 3) != 3
-#error "This code only works on a two's complement system"
-#endif
-
 static FIAT_SECP256K1_DETTMAN_FIAT_INLINE secp256k1_uint128 u128_mul_u64_u64(uint64_t a, uint64_t b) {
   secp256k1_uint128 r;
   secp256k1_u128_mul(&r, a, b);
@@ -68,6 +42,28 @@ static FIAT_SECP256K1_DETTMAN_FIAT_INLINE secp256k1_uint128 u128_add_u64_u128(ui
   secp256k1_u128_accum_u64(&r, a);
   return r;
 }
+
+/* Autogenerated: 'src/ExtractionOCaml/dettman_multiplication' --inline --static -use-value-barrier secp256k1_dettman 64 5 48 2 '2^256 - 4294968273' mul square
+ * curve description: secp256k1_dettman
+ * machine_wordsize = 64 (from "64")
+ * requested operations: mul, square
+ * n = 5 (from "5")
+ * last_limb_width = 48 (from "48")
+ * last_reduction = 2 (from "2")
+ * s-c = 2^256 - [(1, 4294968273)] (from "2^256 - 4294968273")
+ * inbounds_multiplier: None (from "")
+ */
+
+
+FIAT_SECP256K1_DETTMAN_FIAT_EXTENSION typedef secp256k1_uint128 fiat_secp256k1_dettman_uint128;
+
+#define secp256k1_fe_sqr_inner fiat_secp256k1_dettman_square
+#define secp256k1_fe_mul_inner fiat_secp256k1_dettman_mul
+
+#if (-1 & 3) != 3
+#error "This code only works on a two's complement system"
+#endif
+
 /*
  * The function fiat_secp256k1_dettman_mul multiplies two field elements.
  *