b = binder_low; (vars, typ) = binder_vars; SYMBOL "."; body = term ->
let binder = mk_binder_ast b typ vars body in
return_term loc binder
- | t1 = term; SYMBOL <:unicode<to>> (* → *); t2 = term ->
- return_term loc (CicAst.Binder (`Pi, (Cic.Anonymous, Some t1), t2))
]
| "logic_add" LEFTA [ (* nothing here by default *) ]
| "logic_mult" LEFTA [ (* nothing here by default *) ]
b = binder_high; (vars, typ) = binder_vars; SYMBOL "."; body = term ->
let binder = mk_binder_ast b typ vars body in
return_term loc binder
+ | t1 = term; SYMBOL <:unicode<to>> (* → *); t2 = term ->
+ return_term loc (CicAst.Binder (`Pi, (Cic.Anonymous, Some t1), t2))
]
| "simple" NONA
[ sort = sort -> CicAst.Sort sort
(match (pat, terms) with
| None, [] -> TacticAst.Reduce (loc, kind, None)
| None, terms -> TacticAst.Reduce (loc, kind, Some (terms, `Goal))
- | Some pat, [] -> TacticAst.Reduce (loc, kind, Some ([], pat))
+ | Some pat, [] -> fail loc "Missing term [list]"
| Some pat, terms -> TacticAst.Reduce (loc, kind, Some (terms, pat)))
| [ IDENT "reflexivity" ] ->
TacticAst.Reflexivity loc
TacticAst.Check (loc, t)
| [ IDENT "hint" ] -> TacticAst.Hint loc
| [ IDENT "whelp"; "match" ] ; t = term ->
- TacticAst.Match (loc,t)
+ TacticAst.WMatch (loc,t)
| [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
- TacticAst.Instance (loc,t)
+ TacticAst.WInstance (loc,t)
+ | [ IDENT "whelp"; IDENT "locate" ] ; id = IDENT ->
+ TacticAst.WLocate (loc,id)
+ | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
+ TacticAst.WElim (loc, t)
+ | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
+ TacticAst.WHint (loc,t)
| [ IDENT "print" ]; name = QSTRING -> TacticAst.Print (loc, name)
]];