From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 30 Jun 2005 14:48:12 +0000 (+0000)
Subject: The pattern of a fold cannot have the "wanted" part (for the same reasons as
X-Git-Tag: PRE_GETTER_STORAGE~87
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=789a633d6df5e23a4f5fd418e74c9f3e83df1be4;p=helm.git

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 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 ->