X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FcicTextualParser2.ml;h=072b8fa03b97bbb83ed38846155259f60eb2b82f;hb=789a633d6df5e23a4f5fd418e74c9f3e83df1be4;hp=e59e139872e252751a2168e5f58aabc866374a68;hpb=44d337f8d772c6895d310a1b1d62770c3355fe03;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index e59e13987..072b8fa03 100644
--- 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 ->