TacticAst.Check (loc, t)
| [ IDENT "hint" ] -> TacticAst.Hint loc
| [ IDENT "pmatch" ] ; t = term -> TacticAst.Match (loc,t)
+ | [ IDENT "instance" ] ; t = term -> TacticAst.Instance (loc,t)
| [ IDENT "print" ]; name = QSTRING -> TacticAst.Print (loc, name)
]];