| n = substituted_name -> return_term loc n
| i = NUM -> return_term loc (CicAst.Num (i, (fresh_num_instance ())))
| IMPLICIT -> return_term loc CicAst.Implicit
+ | PLACEHOLDER -> return_term loc CicAst.UserInput
| m = META;
substs = [
PAREN "["; substs = LIST0 meta_subst SEP SYMBOL ";" ; PAREN "]" ->
reduction_kind: [
[ [ IDENT "reduce" ] -> `Reduce
| [ IDENT "simplify" ] -> `Simpl
- | [ IDENT "whd" ] -> `Whd ]
+ | [ IDENT "whd" ] -> `Whd
+ | [ IDENT "normalize" ] -> `Normalize ]
];
tactic: [
[ [ IDENT "absurd" ]; t = tactic_term ->
| None, terms -> TacticAst.Reduce (loc, kind, Some (terms, `Goal))
| Some pat, [] -> fail loc "Missing term [list]"
| Some pat, terms -> TacticAst.Reduce (loc, kind, Some (terms, pat)))
+ | kind = reduction_kind; where = IDENT ; IDENT "at" ; pat = term ->
+ TacticAst.ReduceAt (loc, kind, where, pat)
| [ IDENT "reflexivity" ] ->
TacticAst.Reflexivity loc
| [ IDENT "replace" ];