diff --git a/fiat-rust/src/curve25519_32.rs b/fiat-rust/src/curve25519_32.rs
index 13c4f90326..88239dce2e 100644
--- a/fiat-rust/src/curve25519_32.rs
+++ b/fiat-rust/src/curve25519_32.rs
@@ -20,8 +20,8 @@ pub type fiat_25519_i1 = i8;
 pub type fiat_25519_u2 = u8;
 pub type fiat_25519_i2 = i8;
 
-/* The type fiat_25519_loose_field_element is a field element with loose bounds. */
-/* Bounds: [[0x0 ~> 0xc000000], [0x0 ~> 0x6000000], [0x0 ~> 0xc000000], [0x0 ~> 0x6000000], [0x0 ~> 0xc000000], [0x0 ~> 0x6000000], [0x0 ~> 0xc000000], [0x0 ~> 0x6000000], [0x0 ~> 0xc000000], [0x0 ~> 0x6000000]] */
+/** The type fiat_25519_loose_field_element is a field element with loose bounds. */
+/** Bounds: [[0x0 ~> 0xc000000], [0x0 ~> 0x6000000], [0x0 ~> 0xc000000], [0x0 ~> 0x6000000], [0x0 ~> 0xc000000], [0x0 ~> 0x6000000], [0x0 ~> 0xc000000], [0x0 ~> 0x6000000], [0x0 ~> 0xc000000], [0x0 ~> 0x6000000]] */
 #[derive(Clone, Copy)]
 pub struct fiat_25519_loose_field_element(pub [u32; 10]);
 
@@ -40,8 +40,8 @@ impl core::ops::IndexMut<usize> for fiat_25519_loose_field_element {
     }
 }
 
-/* The type fiat_25519_tight_field_element is a field element with tight bounds. */
-/* Bounds: [[0x0 ~> 0x4000000], [0x0 ~> 0x2000000], [0x0 ~> 0x4000000], [0x0 ~> 0x2000000], [0x0 ~> 0x4000000], [0x0 ~> 0x2000000], [0x0 ~> 0x4000000], [0x0 ~> 0x2000000], [0x0 ~> 0x4000000], [0x0 ~> 0x2000000]] */
+/** The type fiat_25519_tight_field_element is a field element with tight bounds. */
+/** Bounds: [[0x0 ~> 0x4000000], [0x0 ~> 0x2000000], [0x0 ~> 0x4000000], [0x0 ~> 0x2000000], [0x0 ~> 0x4000000], [0x0 ~> 0x2000000], [0x0 ~> 0x4000000], [0x0 ~> 0x2000000], [0x0 ~> 0x4000000], [0x0 ~> 0x2000000]] */
 #[derive(Clone, Copy)]
 pub struct fiat_25519_tight_field_element(pub [u32; 10]);
 
diff --git a/fiat-rust/src/curve25519_64.rs b/fiat-rust/src/curve25519_64.rs
index 97960326ae..4622b7f3ba 100644
--- a/fiat-rust/src/curve25519_64.rs
+++ b/fiat-rust/src/curve25519_64.rs
@@ -20,8 +20,8 @@ pub type fiat_25519_i1 = i8;
 pub type fiat_25519_u2 = u8;
 pub type fiat_25519_i2 = i8;
 
-/* The type fiat_25519_loose_field_element is a field element with loose bounds. */
-/* Bounds: [[0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000]] */
+/** The type fiat_25519_loose_field_element is a field element with loose bounds. */
+/** Bounds: [[0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000]] */
 #[derive(Clone, Copy)]
 pub struct fiat_25519_loose_field_element(pub [u64; 5]);
 
@@ -40,8 +40,8 @@ impl core::ops::IndexMut<usize> for fiat_25519_loose_field_element {
     }
 }
 
-/* The type fiat_25519_tight_field_element is a field element with tight bounds. */
-/* Bounds: [[0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000]] */
+/** The type fiat_25519_tight_field_element is a field element with tight bounds. */
+/** Bounds: [[0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000]] */
 #[derive(Clone, Copy)]
 pub struct fiat_25519_tight_field_element(pub [u64; 5]);
 
diff --git a/fiat-rust/src/curve25519_scalar_32.rs b/fiat-rust/src/curve25519_scalar_32.rs
index 23d65a5532..368b481d70 100644
--- a/fiat-rust/src/curve25519_scalar_32.rs
+++ b/fiat-rust/src/curve25519_scalar_32.rs
@@ -25,8 +25,8 @@ pub type fiat_25519_scalar_i1 = i8;
 pub type fiat_25519_scalar_u2 = u8;
 pub type fiat_25519_scalar_i2 = i8;
 
-/* The type fiat_25519_scalar_montgomery_domain_field_element is a field element in the Montgomery domain. */
-/* Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */
+/** The type fiat_25519_scalar_montgomery_domain_field_element is a field element in the Montgomery domain. */
+/** Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */
 #[derive(Clone, Copy)]
 pub struct fiat_25519_scalar_montgomery_domain_field_element(pub [u32; 8]);
 
@@ -45,8 +45,8 @@ impl core::ops::IndexMut<usize> for fiat_25519_scalar_montgomery_domain_field_el
     }
 }
 
-/* The type fiat_25519_scalar_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */
-/* Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */
+/** The type fiat_25519_scalar_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */
+/** Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */
 #[derive(Clone, Copy)]
 pub struct fiat_25519_scalar_non_montgomery_domain_field_element(pub [u32; 8]);
 
diff --git a/fiat-rust/src/curve25519_scalar_64.rs b/fiat-rust/src/curve25519_scalar_64.rs
index 446bab0b65..99d45d3b3a 100644
--- a/fiat-rust/src/curve25519_scalar_64.rs
+++ b/fiat-rust/src/curve25519_scalar_64.rs
@@ -25,8 +25,8 @@ pub type fiat_25519_scalar_i1 = i8;
 pub type fiat_25519_scalar_u2 = u8;
 pub type fiat_25519_scalar_i2 = i8;
 
-/* The type fiat_25519_scalar_montgomery_domain_field_element is a field element in the Montgomery domain. */
-/* Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */
+/** The type fiat_25519_scalar_montgomery_domain_field_element is a field element in the Montgomery domain. */
+/** Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */
 #[derive(Clone, Copy)]
 pub struct fiat_25519_scalar_montgomery_domain_field_element(pub [u64; 4]);
 
@@ -45,8 +45,8 @@ impl core::ops::IndexMut<usize> for fiat_25519_scalar_montgomery_domain_field_el
     }
 }
 
-/* The type fiat_25519_scalar_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */
-/* Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */
+/** The type fiat_25519_scalar_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */
+/** Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */
 #[derive(Clone, Copy)]
 pub struct fiat_25519_scalar_non_montgomery_domain_field_element(pub [u64; 4]);
 
diff --git a/fiat-rust/src/p224_32.rs b/fiat-rust/src/p224_32.rs
index f8ae409768..b839b5c6f4 100644
--- a/fiat-rust/src/p224_32.rs
+++ b/fiat-rust/src/p224_32.rs
@@ -25,8 +25,8 @@ pub type fiat_p224_i1 = i8;
 pub type fiat_p224_u2 = u8;
 pub type fiat_p224_i2 = i8;
 
-/* The type fiat_p224_montgomery_domain_field_element is a field element in the Montgomery domain. */
-/* Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */
+/** The type fiat_p224_montgomery_domain_field_element is a field element in the Montgomery domain. */
+/** Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */
 #[derive(Clone, Copy)]
 pub struct fiat_p224_montgomery_domain_field_element(pub [u32; 7]);
 
@@ -45,8 +45,8 @@ impl core::ops::IndexMut<usize> for fiat_p224_montgomery_domain_field_element {
     }
 }
 
-/* The type fiat_p224_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */
-/* Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */
+/** The type fiat_p224_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */
+/** Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */
 #[derive(Clone, Copy)]
 pub struct fiat_p224_non_montgomery_domain_field_element(pub [u32; 7]);
 
diff --git a/fiat-rust/src/p224_64.rs b/fiat-rust/src/p224_64.rs
index 573bcd0fd3..0253f73f95 100644
--- a/fiat-rust/src/p224_64.rs
+++ b/fiat-rust/src/p224_64.rs
@@ -25,8 +25,8 @@ pub type fiat_p224_i1 = i8;
 pub type fiat_p224_u2 = u8;
 pub type fiat_p224_i2 = i8;
 
-/* The type fiat_p224_montgomery_domain_field_element is a field element in the Montgomery domain. */
-/* Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */
+/** The type fiat_p224_montgomery_domain_field_element is a field element in the Montgomery domain. */
+/** Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */
 #[derive(Clone, Copy)]
 pub struct fiat_p224_montgomery_domain_field_element(pub [u64; 4]);
 
@@ -45,8 +45,8 @@ impl core::ops::IndexMut<usize> for fiat_p224_montgomery_domain_field_element {
     }
 }
 
-/* The type fiat_p224_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */
-/* Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */
+/** The type fiat_p224_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */
+/** Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */
 #[derive(Clone, Copy)]
 pub struct fiat_p224_non_montgomery_domain_field_element(pub [u64; 4]);
 
diff --git a/fiat-rust/src/p256_32.rs b/fiat-rust/src/p256_32.rs
index e9dc68ac64..cc3599e506 100644
--- a/fiat-rust/src/p256_32.rs
+++ b/fiat-rust/src/p256_32.rs
@@ -25,8 +25,8 @@ pub type fiat_p256_i1 = i8;
 pub type fiat_p256_u2 = u8;
 pub type fiat_p256_i2 = i8;
 
-/* The type fiat_p256_montgomery_domain_field_element is a field element in the Montgomery domain. */
-/* Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */
+/** The type fiat_p256_montgomery_domain_field_element is a field element in the Montgomery domain. */
+/** Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */
 #[derive(Clone, Copy)]
 pub struct fiat_p256_montgomery_domain_field_element(pub [u32; 8]);
 
@@ -45,8 +45,8 @@ impl core::ops::IndexMut<usize> for fiat_p256_montgomery_domain_field_element {
     }
 }
 
-/* The type fiat_p256_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */
-/* Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */
+/** The type fiat_p256_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */
+/** Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */
 #[derive(Clone, Copy)]
 pub struct fiat_p256_non_montgomery_domain_field_element(pub [u32; 8]);
 
diff --git a/fiat-rust/src/p256_64.rs b/fiat-rust/src/p256_64.rs
index 37937c822f..22c5a34299 100644
--- a/fiat-rust/src/p256_64.rs
+++ b/fiat-rust/src/p256_64.rs
@@ -25,8 +25,8 @@ pub type fiat_p256_i1 = i8;
 pub type fiat_p256_u2 = u8;
 pub type fiat_p256_i2 = i8;
 
-/* The type fiat_p256_montgomery_domain_field_element is a field element in the Montgomery domain. */
-/* Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */
+/** The type fiat_p256_montgomery_domain_field_element is a field element in the Montgomery domain. */
+/** Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */
 #[derive(Clone, Copy)]
 pub struct fiat_p256_montgomery_domain_field_element(pub [u64; 4]);
 
@@ -45,8 +45,8 @@ impl core::ops::IndexMut<usize> for fiat_p256_montgomery_domain_field_element {
     }
 }
 
-/* The type fiat_p256_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */
-/* Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */
+/** The type fiat_p256_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */
+/** Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */
 #[derive(Clone, Copy)]
 pub struct fiat_p256_non_montgomery_domain_field_element(pub [u64; 4]);
 
diff --git a/fiat-rust/src/p256_scalar_32.rs b/fiat-rust/src/p256_scalar_32.rs
index 620a02a3e2..bcb75ec884 100644
--- a/fiat-rust/src/p256_scalar_32.rs
+++ b/fiat-rust/src/p256_scalar_32.rs
@@ -25,8 +25,8 @@ pub type fiat_p256_scalar_i1 = i8;
 pub type fiat_p256_scalar_u2 = u8;
 pub type fiat_p256_scalar_i2 = i8;
 
-/* The type fiat_p256_scalar_montgomery_domain_field_element is a field element in the Montgomery domain. */
-/* Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */
+/** The type fiat_p256_scalar_montgomery_domain_field_element is a field element in the Montgomery domain. */
+/** Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */
 #[derive(Clone, Copy)]
 pub struct fiat_p256_scalar_montgomery_domain_field_element(pub [u32; 8]);
 
@@ -45,8 +45,8 @@ impl core::ops::IndexMut<usize> for fiat_p256_scalar_montgomery_domain_field_ele
     }
 }
 
-/* The type fiat_p256_scalar_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */
-/* Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */
+/** The type fiat_p256_scalar_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */
+/** Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */
 #[derive(Clone, Copy)]
 pub struct fiat_p256_scalar_non_montgomery_domain_field_element(pub [u32; 8]);
 
diff --git a/fiat-rust/src/p256_scalar_64.rs b/fiat-rust/src/p256_scalar_64.rs
index bb858e252b..17191a35fa 100644
--- a/fiat-rust/src/p256_scalar_64.rs
+++ b/fiat-rust/src/p256_scalar_64.rs
@@ -25,8 +25,8 @@ pub type fiat_p256_scalar_i1 = i8;
 pub type fiat_p256_scalar_u2 = u8;
 pub type fiat_p256_scalar_i2 = i8;
 
-/* The type fiat_p256_scalar_montgomery_domain_field_element is a field element in the Montgomery domain. */
-/* Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */
+/** The type fiat_p256_scalar_montgomery_domain_field_element is a field element in the Montgomery domain. */
+/** Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */
 #[derive(Clone, Copy)]
 pub struct fiat_p256_scalar_montgomery_domain_field_element(pub [u64; 4]);
 
@@ -45,8 +45,8 @@ impl core::ops::IndexMut<usize> for fiat_p256_scalar_montgomery_domain_field_ele
     }
 }
 
-/* The type fiat_p256_scalar_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */
-/* Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */
+/** The type fiat_p256_scalar_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */
+/** Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */
 #[derive(Clone, Copy)]
 pub struct fiat_p256_scalar_non_montgomery_domain_field_element(pub [u64; 4]);
 
diff --git a/fiat-rust/src/p384_32.rs b/fiat-rust/src/p384_32.rs
index d18e82b3bc..53f759d85f 100644
--- a/fiat-rust/src/p384_32.rs
+++ b/fiat-rust/src/p384_32.rs
@@ -25,8 +25,8 @@ pub type fiat_p384_i1 = i8;
 pub type fiat_p384_u2 = u8;
 pub type fiat_p384_i2 = i8;
 
-/* The type fiat_p384_montgomery_domain_field_element is a field element in the Montgomery domain. */
-/* Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */
+/** The type fiat_p384_montgomery_domain_field_element is a field element in the Montgomery domain. */
+/** Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */
 #[derive(Clone, Copy)]
 pub struct fiat_p384_montgomery_domain_field_element(pub [u32; 12]);
 
@@ -45,8 +45,8 @@ impl core::ops::IndexMut<usize> for fiat_p384_montgomery_domain_field_element {
     }
 }
 
-/* The type fiat_p384_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */
-/* Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */
+/** The type fiat_p384_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */
+/** Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */
 #[derive(Clone, Copy)]
 pub struct fiat_p384_non_montgomery_domain_field_element(pub [u32; 12]);
 
diff --git a/fiat-rust/src/p384_64.rs b/fiat-rust/src/p384_64.rs
index 29e14d8f65..f70b28b0e2 100644
--- a/fiat-rust/src/p384_64.rs
+++ b/fiat-rust/src/p384_64.rs
@@ -25,8 +25,8 @@ pub type fiat_p384_i1 = i8;
 pub type fiat_p384_u2 = u8;
 pub type fiat_p384_i2 = i8;
 
-/* The type fiat_p384_montgomery_domain_field_element is a field element in the Montgomery domain. */
-/* Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */
+/** The type fiat_p384_montgomery_domain_field_element is a field element in the Montgomery domain. */
+/** Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */
 #[derive(Clone, Copy)]
 pub struct fiat_p384_montgomery_domain_field_element(pub [u64; 6]);
 
@@ -45,8 +45,8 @@ impl core::ops::IndexMut<usize> for fiat_p384_montgomery_domain_field_element {
     }
 }
 
-/* The type fiat_p384_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */
-/* Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */
+/** The type fiat_p384_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */
+/** Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */
 #[derive(Clone, Copy)]
 pub struct fiat_p384_non_montgomery_domain_field_element(pub [u64; 6]);
 
diff --git a/fiat-rust/src/p384_scalar_32.rs b/fiat-rust/src/p384_scalar_32.rs
index c702880fd6..bcc3121363 100644
--- a/fiat-rust/src/p384_scalar_32.rs
+++ b/fiat-rust/src/p384_scalar_32.rs
@@ -25,8 +25,8 @@ pub type fiat_p384_scalar_i1 = i8;
 pub type fiat_p384_scalar_u2 = u8;
 pub type fiat_p384_scalar_i2 = i8;
 
-/* The type fiat_p384_scalar_montgomery_domain_field_element is a field element in the Montgomery domain. */
-/* Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */
+/** The type fiat_p384_scalar_montgomery_domain_field_element is a field element in the Montgomery domain. */
+/** Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */
 #[derive(Clone, Copy)]
 pub struct fiat_p384_scalar_montgomery_domain_field_element(pub [u32; 12]);
 
@@ -45,8 +45,8 @@ impl core::ops::IndexMut<usize> for fiat_p384_scalar_montgomery_domain_field_ele
     }
 }
 
-/* The type fiat_p384_scalar_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */
-/* Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */
+/** The type fiat_p384_scalar_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */
+/** Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */
 #[derive(Clone, Copy)]
 pub struct fiat_p384_scalar_non_montgomery_domain_field_element(pub [u32; 12]);
 
diff --git a/fiat-rust/src/p384_scalar_64.rs b/fiat-rust/src/p384_scalar_64.rs
index fabae265d0..d4b2da8178 100644
--- a/fiat-rust/src/p384_scalar_64.rs
+++ b/fiat-rust/src/p384_scalar_64.rs
@@ -25,8 +25,8 @@ pub type fiat_p384_scalar_i1 = i8;
 pub type fiat_p384_scalar_u2 = u8;
 pub type fiat_p384_scalar_i2 = i8;
 
-/* The type fiat_p384_scalar_montgomery_domain_field_element is a field element in the Montgomery domain. */
-/* Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */
+/** The type fiat_p384_scalar_montgomery_domain_field_element is a field element in the Montgomery domain. */
+/** Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */
 #[derive(Clone, Copy)]
 pub struct fiat_p384_scalar_montgomery_domain_field_element(pub [u64; 6]);
 
@@ -45,8 +45,8 @@ impl core::ops::IndexMut<usize> for fiat_p384_scalar_montgomery_domain_field_ele
     }
 }
 
-/* The type fiat_p384_scalar_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */
-/* Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */
+/** The type fiat_p384_scalar_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */
+/** Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */
 #[derive(Clone, Copy)]
 pub struct fiat_p384_scalar_non_montgomery_domain_field_element(pub [u64; 6]);
 
diff --git a/fiat-rust/src/p434_64.rs b/fiat-rust/src/p434_64.rs
index d25c449112..b4f550e20e 100644
--- a/fiat-rust/src/p434_64.rs
+++ b/fiat-rust/src/p434_64.rs
@@ -25,8 +25,8 @@ pub type fiat_p434_i1 = i8;
 pub type fiat_p434_u2 = u8;
 pub type fiat_p434_i2 = i8;
 
-/* The type fiat_p434_montgomery_domain_field_element is a field element in the Montgomery domain. */
-/* Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */
+/** The type fiat_p434_montgomery_domain_field_element is a field element in the Montgomery domain. */
+/** Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */
 #[derive(Clone, Copy)]
 pub struct fiat_p434_montgomery_domain_field_element(pub [u64; 7]);
 
@@ -45,8 +45,8 @@ impl core::ops::IndexMut<usize> for fiat_p434_montgomery_domain_field_element {
     }
 }
 
-/* The type fiat_p434_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */
-/* Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */
+/** The type fiat_p434_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */
+/** Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */
 #[derive(Clone, Copy)]
 pub struct fiat_p434_non_montgomery_domain_field_element(pub [u64; 7]);
 
diff --git a/fiat-rust/src/p448_solinas_32.rs b/fiat-rust/src/p448_solinas_32.rs
index 6d7aff5c04..165bf8b461 100644
--- a/fiat-rust/src/p448_solinas_32.rs
+++ b/fiat-rust/src/p448_solinas_32.rs
@@ -20,8 +20,8 @@ pub type fiat_p448_i1 = i8;
 pub type fiat_p448_u2 = u8;
 pub type fiat_p448_i2 = i8;
 
-/* The type fiat_p448_loose_field_element is a field element with loose bounds. */
-/* Bounds: [[0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000]] */
+/** The type fiat_p448_loose_field_element is a field element with loose bounds. */
+/** Bounds: [[0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000]] */
 #[derive(Clone, Copy)]
 pub struct fiat_p448_loose_field_element(pub [u32; 16]);
 
@@ -40,8 +40,8 @@ impl core::ops::IndexMut<usize> for fiat_p448_loose_field_element {
     }
 }
 
-/* The type fiat_p448_tight_field_element is a field element with tight bounds. */
-/* Bounds: [[0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000]] */
+/** The type fiat_p448_tight_field_element is a field element with tight bounds. */
+/** Bounds: [[0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000]] */
 #[derive(Clone, Copy)]
 pub struct fiat_p448_tight_field_element(pub [u32; 16]);
 
diff --git a/fiat-rust/src/p448_solinas_64.rs b/fiat-rust/src/p448_solinas_64.rs
index 44ef66b77e..7a881c10ed 100644
--- a/fiat-rust/src/p448_solinas_64.rs
+++ b/fiat-rust/src/p448_solinas_64.rs
@@ -20,8 +20,8 @@ pub type fiat_p448_i1 = i8;
 pub type fiat_p448_u2 = u8;
 pub type fiat_p448_i2 = i8;
 
-/* The type fiat_p448_loose_field_element is a field element with loose bounds. */
-/* Bounds: [[0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000]] */
+/** The type fiat_p448_loose_field_element is a field element with loose bounds. */
+/** Bounds: [[0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000]] */
 #[derive(Clone, Copy)]
 pub struct fiat_p448_loose_field_element(pub [u64; 8]);
 
@@ -40,8 +40,8 @@ impl core::ops::IndexMut<usize> for fiat_p448_loose_field_element {
     }
 }
 
-/* The type fiat_p448_tight_field_element is a field element with tight bounds. */
-/* Bounds: [[0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000]] */
+/** The type fiat_p448_tight_field_element is a field element with tight bounds. */
+/** Bounds: [[0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000]] */
 #[derive(Clone, Copy)]
 pub struct fiat_p448_tight_field_element(pub [u64; 8]);
 
diff --git a/fiat-rust/src/p521_32.rs b/fiat-rust/src/p521_32.rs
index 996b079cb1..6f4a06213b 100644
--- a/fiat-rust/src/p521_32.rs
+++ b/fiat-rust/src/p521_32.rs
@@ -20,8 +20,8 @@ pub type fiat_p521_i1 = i8;
 pub type fiat_p521_u2 = u8;
 pub type fiat_p521_i2 = i8;
 
-/* The type fiat_p521_loose_field_element is a field element with loose bounds. */
-/* Bounds: [[0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x18000000]] */
+/** The type fiat_p521_loose_field_element is a field element with loose bounds. */
+/** Bounds: [[0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x30000000], [0x0 ~> 0x18000000], [0x0 ~> 0x18000000]] */
 #[derive(Clone, Copy)]
 pub struct fiat_p521_loose_field_element(pub [u32; 19]);
 
@@ -40,8 +40,8 @@ impl core::ops::IndexMut<usize> for fiat_p521_loose_field_element {
     }
 }
 
-/* The type fiat_p521_tight_field_element is a field element with tight bounds. */
-/* Bounds: [[0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x8000000]] */
+/** The type fiat_p521_tight_field_element is a field element with tight bounds. */
+/** Bounds: [[0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x10000000], [0x0 ~> 0x8000000], [0x0 ~> 0x8000000]] */
 #[derive(Clone, Copy)]
 pub struct fiat_p521_tight_field_element(pub [u32; 19]);
 
diff --git a/fiat-rust/src/p521_64.rs b/fiat-rust/src/p521_64.rs
index afe6bc272e..c2f6614c6a 100644
--- a/fiat-rust/src/p521_64.rs
+++ b/fiat-rust/src/p521_64.rs
@@ -20,8 +20,8 @@ pub type fiat_p521_i1 = i8;
 pub type fiat_p521_u2 = u8;
 pub type fiat_p521_i2 = i8;
 
-/* The type fiat_p521_loose_field_element is a field element with loose bounds. */
-/* Bounds: [[0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0x600000000000000]] */
+/** The type fiat_p521_loose_field_element is a field element with loose bounds. */
+/** Bounds: [[0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0x600000000000000]] */
 #[derive(Clone, Copy)]
 pub struct fiat_p521_loose_field_element(pub [u64; 9]);
 
@@ -40,8 +40,8 @@ impl core::ops::IndexMut<usize> for fiat_p521_loose_field_element {
     }
 }
 
-/* The type fiat_p521_tight_field_element is a field element with tight bounds. */
-/* Bounds: [[0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x200000000000000]] */
+/** The type fiat_p521_tight_field_element is a field element with tight bounds. */
+/** Bounds: [[0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x200000000000000]] */
 #[derive(Clone, Copy)]
 pub struct fiat_p521_tight_field_element(pub [u64; 9]);
 
diff --git a/fiat-rust/src/poly1305_32.rs b/fiat-rust/src/poly1305_32.rs
index 419d13b05c..b9caf8461c 100644
--- a/fiat-rust/src/poly1305_32.rs
+++ b/fiat-rust/src/poly1305_32.rs
@@ -20,8 +20,8 @@ pub type fiat_poly1305_i1 = i8;
 pub type fiat_poly1305_u2 = u8;
 pub type fiat_poly1305_i2 = i8;
 
-/* The type fiat_poly1305_loose_field_element is a field element with loose bounds. */
-/* Bounds: [[0x0 ~> 0xc000000], [0x0 ~> 0xc000000], [0x0 ~> 0xc000000], [0x0 ~> 0xc000000], [0x0 ~> 0xc000000]] */
+/** The type fiat_poly1305_loose_field_element is a field element with loose bounds. */
+/** Bounds: [[0x0 ~> 0xc000000], [0x0 ~> 0xc000000], [0x0 ~> 0xc000000], [0x0 ~> 0xc000000], [0x0 ~> 0xc000000]] */
 #[derive(Clone, Copy)]
 pub struct fiat_poly1305_loose_field_element(pub [u32; 5]);
 
@@ -40,8 +40,8 @@ impl core::ops::IndexMut<usize> for fiat_poly1305_loose_field_element {
     }
 }
 
-/* The type fiat_poly1305_tight_field_element is a field element with tight bounds. */
-/* Bounds: [[0x0 ~> 0x4000000], [0x0 ~> 0x4000000], [0x0 ~> 0x4000000], [0x0 ~> 0x4000000], [0x0 ~> 0x4000000]] */
+/** The type fiat_poly1305_tight_field_element is a field element with tight bounds. */
+/** Bounds: [[0x0 ~> 0x4000000], [0x0 ~> 0x4000000], [0x0 ~> 0x4000000], [0x0 ~> 0x4000000], [0x0 ~> 0x4000000]] */
 #[derive(Clone, Copy)]
 pub struct fiat_poly1305_tight_field_element(pub [u32; 5]);
 
diff --git a/fiat-rust/src/poly1305_64.rs b/fiat-rust/src/poly1305_64.rs
index 9807d257c7..2e840347ba 100644
--- a/fiat-rust/src/poly1305_64.rs
+++ b/fiat-rust/src/poly1305_64.rs
@@ -20,8 +20,8 @@ pub type fiat_poly1305_i1 = i8;
 pub type fiat_poly1305_u2 = u8;
 pub type fiat_poly1305_i2 = i8;
 
-/* The type fiat_poly1305_loose_field_element is a field element with loose bounds. */
-/* Bounds: [[0x0 ~> 0x300000000000], [0x0 ~> 0x180000000000], [0x0 ~> 0x180000000000]] */
+/** The type fiat_poly1305_loose_field_element is a field element with loose bounds. */
+/** Bounds: [[0x0 ~> 0x300000000000], [0x0 ~> 0x180000000000], [0x0 ~> 0x180000000000]] */
 #[derive(Clone, Copy)]
 pub struct fiat_poly1305_loose_field_element(pub [u64; 3]);
 
@@ -40,8 +40,8 @@ impl core::ops::IndexMut<usize> for fiat_poly1305_loose_field_element {
     }
 }
 
-/* The type fiat_poly1305_tight_field_element is a field element with tight bounds. */
-/* Bounds: [[0x0 ~> 0x100000000000], [0x0 ~> 0x80000000000], [0x0 ~> 0x80000000000]] */
+/** The type fiat_poly1305_tight_field_element is a field element with tight bounds. */
+/** Bounds: [[0x0 ~> 0x100000000000], [0x0 ~> 0x80000000000], [0x0 ~> 0x80000000000]] */
 #[derive(Clone, Copy)]
 pub struct fiat_poly1305_tight_field_element(pub [u64; 3]);
 
diff --git a/fiat-rust/src/secp256k1_montgomery_32.rs b/fiat-rust/src/secp256k1_montgomery_32.rs
index 15b3c9bd34..cc963262aa 100644
--- a/fiat-rust/src/secp256k1_montgomery_32.rs
+++ b/fiat-rust/src/secp256k1_montgomery_32.rs
@@ -25,8 +25,8 @@ pub type fiat_secp256k1_montgomery_i1 = i8;
 pub type fiat_secp256k1_montgomery_u2 = u8;
 pub type fiat_secp256k1_montgomery_i2 = i8;
 
-/* The type fiat_secp256k1_montgomery_montgomery_domain_field_element is a field element in the Montgomery domain. */
-/* Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */
+/** The type fiat_secp256k1_montgomery_montgomery_domain_field_element is a field element in the Montgomery domain. */
+/** Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */
 #[derive(Clone, Copy)]
 pub struct fiat_secp256k1_montgomery_montgomery_domain_field_element(pub [u32; 8]);
 
@@ -45,8 +45,8 @@ impl core::ops::IndexMut<usize> for fiat_secp256k1_montgomery_montgomery_domain_
     }
 }
 
-/* The type fiat_secp256k1_montgomery_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */
-/* Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */
+/** The type fiat_secp256k1_montgomery_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */
+/** Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */
 #[derive(Clone, Copy)]
 pub struct fiat_secp256k1_montgomery_non_montgomery_domain_field_element(pub [u32; 8]);
 
diff --git a/fiat-rust/src/secp256k1_montgomery_64.rs b/fiat-rust/src/secp256k1_montgomery_64.rs
index 5dd84790a1..e4ff3bb720 100644
--- a/fiat-rust/src/secp256k1_montgomery_64.rs
+++ b/fiat-rust/src/secp256k1_montgomery_64.rs
@@ -25,8 +25,8 @@ pub type fiat_secp256k1_montgomery_i1 = i8;
 pub type fiat_secp256k1_montgomery_u2 = u8;
 pub type fiat_secp256k1_montgomery_i2 = i8;
 
-/* The type fiat_secp256k1_montgomery_montgomery_domain_field_element is a field element in the Montgomery domain. */
-/* Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */
+/** The type fiat_secp256k1_montgomery_montgomery_domain_field_element is a field element in the Montgomery domain. */
+/** Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */
 #[derive(Clone, Copy)]
 pub struct fiat_secp256k1_montgomery_montgomery_domain_field_element(pub [u64; 4]);
 
@@ -45,8 +45,8 @@ impl core::ops::IndexMut<usize> for fiat_secp256k1_montgomery_montgomery_domain_
     }
 }
 
-/* The type fiat_secp256k1_montgomery_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */
-/* Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */
+/** The type fiat_secp256k1_montgomery_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */
+/** Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */
 #[derive(Clone, Copy)]
 pub struct fiat_secp256k1_montgomery_non_montgomery_domain_field_element(pub [u64; 4]);
 
diff --git a/fiat-rust/src/secp256k1_montgomery_scalar_32.rs b/fiat-rust/src/secp256k1_montgomery_scalar_32.rs
index 6693ab6154..ce1cdb3b3e 100644
--- a/fiat-rust/src/secp256k1_montgomery_scalar_32.rs
+++ b/fiat-rust/src/secp256k1_montgomery_scalar_32.rs
@@ -25,8 +25,8 @@ pub type fiat_secp256k1_montgomery_scalar_i1 = i8;
 pub type fiat_secp256k1_montgomery_scalar_u2 = u8;
 pub type fiat_secp256k1_montgomery_scalar_i2 = i8;
 
-/* The type fiat_secp256k1_montgomery_scalar_montgomery_domain_field_element is a field element in the Montgomery domain. */
-/* Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */
+/** The type fiat_secp256k1_montgomery_scalar_montgomery_domain_field_element is a field element in the Montgomery domain. */
+/** Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */
 #[derive(Clone, Copy)]
 pub struct fiat_secp256k1_montgomery_scalar_montgomery_domain_field_element(pub [u32; 8]);
 
@@ -45,8 +45,8 @@ impl core::ops::IndexMut<usize> for fiat_secp256k1_montgomery_scalar_montgomery_
     }
 }
 
-/* The type fiat_secp256k1_montgomery_scalar_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */
-/* Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */
+/** The type fiat_secp256k1_montgomery_scalar_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */
+/** Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */
 #[derive(Clone, Copy)]
 pub struct fiat_secp256k1_montgomery_scalar_non_montgomery_domain_field_element(pub [u32; 8]);
 
diff --git a/fiat-rust/src/secp256k1_montgomery_scalar_64.rs b/fiat-rust/src/secp256k1_montgomery_scalar_64.rs
index 48499f30ed..369258569c 100644
--- a/fiat-rust/src/secp256k1_montgomery_scalar_64.rs
+++ b/fiat-rust/src/secp256k1_montgomery_scalar_64.rs
@@ -25,8 +25,8 @@ pub type fiat_secp256k1_montgomery_scalar_i1 = i8;
 pub type fiat_secp256k1_montgomery_scalar_u2 = u8;
 pub type fiat_secp256k1_montgomery_scalar_i2 = i8;
 
-/* The type fiat_secp256k1_montgomery_scalar_montgomery_domain_field_element is a field element in the Montgomery domain. */
-/* Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */
+/** The type fiat_secp256k1_montgomery_scalar_montgomery_domain_field_element is a field element in the Montgomery domain. */
+/** Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */
 #[derive(Clone, Copy)]
 pub struct fiat_secp256k1_montgomery_scalar_montgomery_domain_field_element(pub [u64; 4]);
 
@@ -45,8 +45,8 @@ impl core::ops::IndexMut<usize> for fiat_secp256k1_montgomery_scalar_montgomery_
     }
 }
 
-/* The type fiat_secp256k1_montgomery_scalar_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */
-/* Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */
+/** The type fiat_secp256k1_montgomery_scalar_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */
+/** Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] */
 #[derive(Clone, Copy)]
 pub struct fiat_secp256k1_montgomery_scalar_non_montgomery_domain_field_element(pub [u64; 4]);
 
diff --git a/src/Stringification/Rust.v b/src/Stringification/Rust.v
index f6196365d0..af9f019857 100644
--- a/src/Stringification/Rust.v
+++ b/src/Stringification/Rust.v
@@ -24,7 +24,7 @@ Import Stringification.Language.Compilers.ToString.int.Notations.
 
 Module Rust.
   Definition comment_module_header_block := List.map (fun line => "//! " ++ line)%string.
-  Definition comment_block := List.map (fun line => "/* " ++ line ++ " */")%string.
+  Definition comment_block := List.map (fun line => "/** " ++ line ++ " */")%string.
 
 
   (* Supported integer bitwidths *)