The pattern of a fold cannot have the "wanted" part (for the same reasons as

rewrite)

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index e59e139872e252751a2168e5f58aabc866374a68..072b8fa03b97bbb83ed38846155259f60eb2b82f 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -399,7 +399,13 @@ EXTEND
         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 ->