- term: LEVEL "90" (* simple *)
- [ "90" NONA
- [ id = IDENT -> return_term loc (Ident (id, None))
- | id = IDENT; s = explicit_subst -> return_term loc (Ident (id, Some s))
- | s = CSYMBOL -> return_term loc (Symbol (s, 0))
- | u = URI -> return_term loc (Uri (u, None))
- | n = NUMBER -> return_term loc (Num (n, 0))
- | IMPLICIT -> return_term loc (Implicit)
- | PLACEHOLDER -> return_term loc UserInput
- | m = META -> return_term loc (Meta (int_of_string m, []))
- | m = META; s = meta_substs -> return_term loc (Meta (int_of_string m, s))
- | s = sort -> return_term loc (Sort s)
- | outtyp = OPT [ SYMBOL "["; ty = term; SYMBOL "]" -> ty ];
- "match"; t = term;
- indty_ident = OPT [ "in"; id = IDENT -> id ];
+ term: LEVEL "90N" (* simple *)
+ [
+ [ id = IDENT -> return_term loc (Ast.Ident (id, None))
+ | id = IDENT; s = explicit_subst ->
+ return_term loc (Ast.Ident (id, Some s))
+ | s = CSYMBOL -> return_term loc (Ast.Symbol (s, 0))
+ | u = URI -> return_term loc (Ast.Uri (u, None))
+ | n = NUMBER -> return_term loc (Ast.Num (n, 0))
+ | IMPLICIT -> return_term loc (Ast.Implicit)
+ | PLACEHOLDER -> return_term loc Ast.UserInput
+ | m = META -> return_term loc (Ast.Meta (int_of_string m, []))
+ | m = META; s = meta_substs ->
+ return_term loc (Ast.Meta (int_of_string m, s))
+ | s = sort -> return_term loc (Ast.Sort s)
+ | "match"; t = term;
+ indty_ident = OPT [ "in"; id = IDENT -> id, None ];
+ outtyp = OPT [ "return"; ty = term -> ty ];