diff --git a/Primitive/Asymmetric/Signature/ECDSA/UnconstrainedSpec.cry b/Primitive/Asymmetric/Signature/ECDSA/UnconstrainedSpec.cry
index 9db5af86..819b972b 100644
--- a/Primitive/Asymmetric/Signature/ECDSA/UnconstrainedSpec.cry
+++ b/Primitive/Asymmetric/Signature/ECDSA/UnconstrainedSpec.cry
@@ -208,6 +208,7 @@ publicKey d = EC::scmul (fromZ d) EC::G
  * [FIPS-186-5] Section 3.3.
  * ```repl
  * :check signAndVerifyIsCorrect`{64}
+ * ```
  */
 signAndVerifyIsCorrect : {m} (fin m, width m < 64) => [m] -> Z EC::n -> Z EC::n -> Bool
 property signAndVerifyIsCorrect M d k = verification
diff --git a/Primitive/Keyless/Hash/SHA3/Tests.cry b/Primitive/Keyless/Hash/SHA3/Tests.cry
index 8347531d..10d9dda9 100644
--- a/Primitive/Keyless/Hash/SHA3/Tests.cry
+++ b/Primitive/Keyless/Hash/SHA3/Tests.cry
@@ -1,4 +1,4 @@
-/*
+/**
  * Tests of the SHA3 hash functions.
  *
  * Test vectors drawn from the NIST Cryptographic Standards and Guidelines
@@ -17,7 +17,7 @@ import Primitive::Keyless::Hash::utils
 submodule SHA3_224 where
   import Primitive::Keyless::Hash::SHA3::SHA3_224
 
-  /*
+  /**
    * ```repl
    * :prove t1
    * ```
@@ -25,7 +25,7 @@ submodule SHA3_224 where
   property t1 = join (toBytes (sha3 [])) ==
     0x6b4e03423667dbb73b6e15454f0eb1abd4597f9a1b078e3f5b5a6bc7
 
-  /*
+  /**
    * ```repl
    * :prove t2
    * ```
@@ -36,7 +36,7 @@ submodule SHA3_224 where
   msg1600 : [1600]
   msg1600 = join [ 0b11000101 | _ <- zero : [200] ]
 
-  /*
+  /**
    * ```repl
    * :prove t3
    * ```
@@ -44,7 +44,7 @@ submodule SHA3_224 where
   property t3 = join (toBytes (sha3 msg1600)) ==
     0x9376816aba503f72f96ce7eb65ac095deee3be4bf9bbc2a1cb7e11e0
 
-  /*
+  /**
    * ```repl
    * :prove t4
    * ```
@@ -56,7 +56,7 @@ submodule SHA3_224 where
 submodule SHA3_256 where
   import Primitive::Keyless::Hash::SHA3::SHA3_256
 
-  /*
+  /**
    * ```repl
    * :prove t1
    * ```
@@ -64,7 +64,7 @@ submodule SHA3_256 where
   property t1 = join (toBytes (sha3 [])) ==
     0xa7ffc6f8bf1ed76651c14756a061d662f580ff4de43b49fa82d80a4b80f8434a
 
-  /*
+  /**
    * ```repl
    * :prove t2
    * ```
@@ -72,7 +72,7 @@ submodule SHA3_256 where
   property t2 = join (toBytes (sha3 0b11001)) ==
     0x7b0047cf5a456882363cbf0fb05322cf65f4b7059a46365e830132e3b5d957af
 
-  /*
+  /**
    * ```repl
    * :prove t3
    * ```
@@ -84,7 +84,7 @@ submodule SHA3_256 where
 submodule SHA3_384 where
   import Primitive::Keyless::Hash::SHA3::SHA3_384
 
-  /*
+  /**
    * ```repl
    * :prove t1
    * ```
@@ -92,7 +92,7 @@ submodule SHA3_384 where
   property t1 = join (toBytes (sha3 [])) ==
     0x0c63a75b845e4f7d01107d852e4c2485c51a50aaaa94fc61995e71bbee983a2ac3713831264adb47fb6bd1e058d5f004
 
-  /*
+  /**
    * ```repl
    * :prove t2
    * ```
@@ -104,7 +104,7 @@ submodule SHA3_384 where
 submodule SHA3_512 where
   import Primitive::Keyless::Hash::SHA3::SHA3_512
 
-  /*
+  /**
    * ```repl
    * :prove t1
    * ```
@@ -112,7 +112,7 @@ submodule SHA3_512 where
   property t1 = join (toBytes (sha3 [])) ==
     0xa69f73cca23a9ac5c8b567dc185a756e97c982164fe25859e0d1dcc1475c80a615b2123af1f5f94c11e3e9402c3ac558f500199d95b6d3e301758586281dcd26
 
-  /*
+  /**
    * ```repl
    * :prove t2
    * ```
diff --git a/Primitive/Keyless/Hash/SHAKE/SHAKE256.cry b/Primitive/Keyless/Hash/SHAKE/SHAKE256.cry
index d68fa44e..509301c3 100644
--- a/Primitive/Keyless/Hash/SHAKE/SHAKE256.cry
+++ b/Primitive/Keyless/Hash/SHAKE/SHAKE256.cry
@@ -34,7 +34,7 @@ import Primitive::Keyless::Hash::utils (toBytes)
 shake256: {d, m} (fin m) => [m] -> [d]
 shake256 M = Keccak (M # 0b1111)
 
-/*
+/**
  * ```repl
  * :prove k5
  * ```
@@ -47,7 +47,7 @@ property k5 = join (toBytes (shake256`{512} [])) == expected_result where
         0xfc821c49479ab48640292eacb3b7c4be
     ]
 
-/*
+/**
  * ```repl
  * :prove k6
  * ```
@@ -60,7 +60,7 @@ property k6 = join (toBytes (shake256 0b0)) == expected_result where
         0x55d30410d71b8e275a676545600f1c35
     ]
 
-/*
+/**
  * ```repl
  * :prove k7
  * ```
@@ -73,7 +73,7 @@ property k7 = join (toBytes (shake256 0b11 : [512])) == expected_result where
         0x7c98f3948e6b7959a9b8950ffd6345d5
     ]
 
-/*
+/**
  * ```repl
  * :prove k8
  * ```
diff --git a/Primitive/Symmetric/Cipher/Block/AES_specification.cry b/Primitive/Symmetric/Cipher/Block/AES_specification.cry
index 40317c31..5ea9b5f8 100644
--- a/Primitive/Symmetric/Cipher/Block/AES_specification.cry
+++ b/Primitive/Symmetric/Cipher/Block/AES_specification.cry
@@ -44,7 +44,7 @@ encrypt k = encryptWithSchedule (keyExpansion k)
 decrypt : [KeySize] -> [BlockSize] -> [BlockSize]
 decrypt k = decryptWithSchedule (keyExpansion k)
 
-/*
+/**
  * This property must be true for each instantiation.
  * With high probability, it will be extremely slow to prove.
  *