return_term loc
(CicAst.Binder (`Pi, (Cic.Anonymous, Some t1), t2))
]
- | "eq" LEFTA
+ | "relop" LEFTA
[ t1 = term; SYMBOL "="; t2 = term ->
return_term loc (CicAst.Appl [CicAst.Symbol ("eq", 0); t1; t2])
]
| PAREN "("; t = term; PAREN ")" -> return_term loc t
]
];
- tactic_where: [ [ where = OPT [ "in"; ident = IDENT -> ident ] -> where ] ];
+ tactic_where: [
+ [ where = OPT [ IDENT "in"; ident = IDENT -> ident ] -> where ]
+ ];
tactic_term: [ [ t = term -> t ] ];
ident_list0: [
[ PAREN "["; idents = LIST0 IDENT SEP SYMBOL ";"; PAREN "]" -> idents ]
| IDENT "elim"; IDENT "type"; t = tactic_term ->
return_tactic loc (TacticAst.ElimType t)
| IDENT "elim"; t1 = tactic_term;
- using = OPT [ IDENT "using"; using = tactic_term -> using ] ->
+ using = OPT [ "using"; using = tactic_term -> using ] ->
return_tactic loc (TacticAst.Elim (t1, using))
| IDENT "exact"; t = tactic_term -> return_tactic loc (TacticAst.Exact t)
| IDENT "exists" -> return_tactic loc TacticAst.Exists