Require doc-strings to start with "/**" with exactly 2 asterisks.

Things like "/******* WARNING ********/" are now parsed as ordinary
comments. See #438.

src/Cryptol/Parser/Lexer.x

@@ -57,7 +57,8 @@ $unitick        = \x7
 
 <0,comment> {
 \/\*                     { startComment False }
-\/\*\*+                  { startComment True  }
+\/\*\*                   { startComment True  }
+\/\*\*\*+                { startComment False }
 \/\*+\/                  { startEndComment    }
 }