diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index b19f7e478bd77f9e680841b0e5403008695b9a50..59ed65b49bbedb6a849581dec87a98ffd099a705 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -720,9 +720,12 @@ cv:
 ;
 
 type_spec_cv:
-     type_spec { $1 }
+     type_spec cv_after { $2 $1 }
 |    cv type_spec_cv { LTattribute ($2, $1) }
-|    type_spec_cv cv { LTattribute ($1, $2) }
+
+cv_after:
+  /* empty */ { fun t -> t }
+| cv cv_after { fun t -> $2 (LTattribute (t,$1)) }
 
 cast_logic_type:
  | type_spec_cv abs_spec_cv_option { $2 $1 }