TacticAst.Exists loc
| IDENT "fail" -> TacticAst.Fail loc
| IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec ->
- TacticAst.Fold (loc, kind, t, p)
+ let (pt,_,_) = p in
+ if pt <> None then
+ raise
+ (Parse_error
+ (loc,"the pattern cannot specify the term to replace, only its paths in the hypotheses and in the conclusion"))
+ else
+ TacticAst.Fold (loc, kind, t, p)
| IDENT "fourier" ->
TacticAst.Fourier loc
| IDENT "fwd"; hyp = IDENT; idents = OPT ident_list0 ->