Closed ColinRothgang closed 5 years ago
This breaks the parsing of the header of inductively-defined functions and record terms.
@florian-rabe Before the commit, they used to parse correctly as OMIDs.
It might or might not be solved by your latest commits (hard to say, as none of them currently compiles). EDIT: It is not.
Seems gone now (or hidden by a different issue).
This breaks the parsing of the header of inductively-defined functions and record terms.
@florian-rabe Before the commit, they used to parse correctly as OMIDs.