diff --git a/src/driver/driver_lexer.mll b/src/driver/driver_lexer.mll
index 8cbceb4944c60d491aa44e645c36e0bd1c2ef60a..40784adfe2e16d20f3d1c764e0cc4a271a263b0a 100644
--- a/src/driver/driver_lexer.mll
+++ b/src/driver/driver_lexer.mll
@@ -52,7 +52,6 @@
         "converter", CONVERTER;
         "literal", LITERAL;
       ]
-
 }
 
 let space = [' ' '\t' '\r']
@@ -65,12 +64,18 @@ let op_char = ['=' '<' '>' '~' '+' '-' '*' '/' '%'
 
 rule token = parse
   | '\n'
-      { new_line lexbuf; token lexbuf }
+      { Lexing.new_line lexbuf; token lexbuf }
   | space+
       { token lexbuf }
-  | "(*)"
-      { LEFTPAR_STAR_RIGHTPAR }
-  | "(*"
+  | "(**)"
+      { token lexbuf }
+  | "(*(*"
+      { Lexlib.comment lexbuf; Lexlib.comment lexbuf; token lexbuf }
+  | "(*" '\n'
+      { Lexing.new_line lexbuf; Lexlib.comment lexbuf; token lexbuf }
+  | "(*(*)"
+  | "(*" eof
+  | "(*" [^ ')']
       { Lexlib.comment lexbuf; token lexbuf }
   | '_'
       { UNDERSCORE }
diff --git a/src/driver/driver_parser.mly b/src/driver/driver_parser.mly
index e510496997f7a6d9c2ff657e320219d57a8c51fa..c0fb63135315d52b00ca9c5fb66b50226bc5d5ad 100644
--- a/src/driver/driver_parser.mly
+++ b/src/driver/driver_parser.mly
@@ -26,7 +26,7 @@
 %token BLACKLIST
 %token MODULE EXCEPTION VAL CONVERTER LITERAL
 %token FUNCTION PREDICATE TYPE PROP ALL FILENAME TRANSFORM PLUGIN
-%token LEFTPAR_STAR_RIGHTPAR COMMA CONSTANT
+%token COMMA CONSTANT
 %token LEFTSQ RIGHTSQ LARROW
 
 %nonassoc SYNTAX REMOVE PRELUDE
@@ -133,7 +133,6 @@ ident:
 
 ident_rich:
 | ident                     { $1 }
-| LEFTPAR_STAR_RIGHTPAR     { Ident.infix "*" }
 | LEFTPAR operator RIGHTPAR { $2 }
 
 operator:
diff --git a/src/parser/lexer.mll b/src/parser/lexer.mll
index 538eee7510092e985f6e27346d10d1817424278f..b27bd1e7b7368c332846228a4e0872f0a85b9e75 100644
--- a/src/parser/lexer.mll
+++ b/src/parser/lexer.mll
@@ -166,9 +166,15 @@ rule token = parse
         (['p' 'P'] (['-' '+']? digit+ as e))?
       { REAL (Number.real_const_hex i f
           (Opt.map Lexlib.remove_leading_plus e)) }
-  | "(*)"
-      { LEFTPAR_STAR_RIGHTPAR }
-  | "(*"
+  | "(**)"
+      { token lexbuf }
+  | "(*(*"
+      { Lexlib.comment lexbuf; Lexlib.comment lexbuf; token lexbuf }
+  | "(*" '\n'
+      { Lexing.new_line lexbuf; Lexlib.comment lexbuf; token lexbuf }
+  | "(*(*)"
+  | "(*" eof
+  | "(*" [^ ')']
       { Lexlib.comment lexbuf; token lexbuf }
   | "'" (lident as id)
       { QUOTE_LIDENT id }
diff --git a/src/parser/parser.mly b/src/parser/parser.mly
index d6050d649759a67c95bb1fb46c85012c911c8c00..5c7134008a85bc357a7771fb7aa4a6f916843682 100644
--- a/src/parser/parser.mly
+++ b/src/parser/parser.mly
@@ -147,7 +147,7 @@
 %token BAR
 %token COLON COMMA
 %token DOT DOTDOT EQUAL LT GT LTGT MINUS
-%token LEFTPAR LEFTPAR_STAR_RIGHTPAR LEFTSQ
+%token LEFTPAR LEFTSQ
 %token LARROW LRARROW OR
 %token RIGHTPAR RIGHTSQ
 %token UNDERSCORE
@@ -1183,11 +1183,6 @@ lident_rich:
 
 lident_op_id:
 | LEFTPAR lident_op RIGHTPAR  { mk_id $2 $startpos($2) $endpos($2) }
-| LEFTPAR_STAR_RIGHTPAR
-    { (* parentheses are removed from the location *)
-      let s = let s = $startpos in { s with Lexing.pos_cnum = s.Lexing.pos_cnum + 1 } in
-      let e = let e = $endpos   in { e with Lexing.pos_cnum = e.Lexing.pos_cnum - 1 } in
-      mk_id (Ident.infix "*") s e }
 
 lident_op:
 | op_symbol               { Ident.infix $1 }