From 789a633d6df5e23a4f5fd418e74c9f3e83df1be4 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 30 Jun 2005 14:48:12 +0000 Subject: [PATCH 1/1] The pattern of a fold cannot have the "wanted" part (for the same reasons as rewrite) --- helm/ocaml/cic_disambiguation/cicTextualParser2.ml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) 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 -> -- 2.39.2