* Bug fixed: "tac." was parsed as Seq [tac]

[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 9ce70062f7c31dd843e96ac7d7191c7aaa4ba2fc..fd79cdab176374096c76b36ed3ca28bc092447c0 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -477,8 +477,8 @@ EXTEND
   ];
   tactical:
     [ "sequence" LEFTA
-      [ tacticals = LIST1 NEXT SEP SYMBOL ";" ->
-          TacticAst.Seq (loc, tacticals)
+      [ tactical = NEXT -> tactical
+      | tacticals = LIST1 NEXT SEP SYMBOL ";" -> TacticAst.Seq (loc, tacticals)
       ]
     | "then" NONA
       [ tac = tactical;
@@ -486,9 +486,9 @@ EXTEND
           (TacticAst.Then (loc, tac, tacs))
       ]
     | "loops" RIGHTA
-      [ [ IDENT "do" ]; count = int; tac = tactical ->
+      [ IDENT "do"; count = int; tac = tactical ->
           TacticAst.Do (loc, count, tac)
-      | [ IDENT "repeat" ]; tac = tactical ->
+      | IDENT "repeat"; tac = tactical ->
           TacticAst.Repeat (loc, tac)
       ]
     | "simple" NONA