diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly index c3f968a0c0352136741f9b8ed8d85430290ceedd..fb91e86165755fdfcf0c4503b84707e95f82e9ca 100644 --- a/src/kernel_internals/parsing/logic_parser.mly +++ b/src/kernel_internals/parsing/logic_parser.mly @@ -1868,7 +1868,7 @@ any_identifier: ; identifier_or_typename: /* allowed as C field names */ -| is_acsl_other_typename { $1 } +| is_acsl_typename { $1 } | TYPENAME { $1 } /* followed by the same list than 'identifier' */ | IDENTIFIER { $1 } /* token list used inside ascl clauses: */ @@ -1889,7 +1889,7 @@ identifier: /* part included into 'identifier_or_typename', but duplicated to av bounded_var: | identifier { $1 } -| is_acsl_other_typename /* Since TYPENAME cannot be accepted by lexpr rule */ +| is_acsl_typename /* Since TYPENAME cannot be accepted by lexpr rule */ { raise (Not_well_formed(loc (), "Type names are not allowed as binding variable"))