sort: [
[ "Prop" -> `Prop
| "Set" -> `Set
- | "Type"; SYMBOL "["; n = NUMBER; SYMBOL "]" -> `NType n
+ | "Type"; SYMBOL "["; n = [ NUMBER| IDENT ]; SYMBOL "]" -> `NType n
| "Type" -> `Type (CicUniv.fresh ())
- | "CProp"; SYMBOL "["; n = NUMBER; SYMBOL "]" -> `NCProp n
+ | "CProp"; SYMBOL "["; n = [ NUMBER| IDENT ]; SYMBOL "]" -> `NCProp n
| "CProp" -> `CProp (CicUniv.fresh ())
]
];