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])
]
| 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