Skip to content

Cleanup BuiltInSyntax vs UserSyntax

Matthew Pickering requested to merge wip/user-vs-builtin into master

There was some confusion about whether FUN/TYPE/One/Many should be BuiltInSyntax or UserSyntax. The answer is certainly UserSyntax as BuiltInSyntax is for things which are directly constructed by the parser rather than going through normal renaming channels.

I fixed all the obviously wrong places I could find and added a test for the original bug which was caused by this (#21752 (closed))

Fixes #21752 (closed)

Merge request reports