Signature and concrete syntax of fold fixed.

[helm.git] / helm / ocaml / cic_disambiguation / cicTextualParser2.ml

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 728ff94a085157d37933e1d14e782f108c2866d6..e59e139872e252751a2168e5f58aabc866374a68 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -398,8 +398,8 @@ EXTEND
     | IDENT "exists" ->
         TacticAst.Exists loc
     | IDENT "fail" -> TacticAst.Fail loc
-    | IDENT "fold"; kind = reduction_kind; p = pattern_spec ->
-        TacticAst.Fold (loc, kind, p)
+    | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec ->
+        TacticAst.Fold (loc, kind, t, p)
     | IDENT "fourier" ->
         TacticAst.Fourier loc
     | IDENT "fwd"; hyp = IDENT; idents = OPT ident_list0 ->