- fix in intro parsing

- avoid generating seq tactical for a 1-length sequences

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 4bfc7c4457ba7ea6f9be44469e1811bf071052d9..d5f427c4f92f039367f722eceb4abf3bb0ce6b68 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -363,7 +363,7 @@ EXTEND
         let idents = match idents with None -> [] | Some idents -> idents in
         return_tactic loc (TacticAst.Intros (num, idents))
     | [ IDENT "intro" | IDENT "Intro" ] ->
-        return_tactic loc (TacticAst.Intros (Some 1, []))
+        return_tactic loc (TacticAst.Intros (None, []))
     | [ IDENT "left" | IDENT "Left" ] -> return_tactic loc TacticAst.Left
     | [ "let" | "Let" ];
       t = tactic_term; "in"; where = IDENT ->
@@ -405,7 +405,9 @@ EXTEND
       [ cmd = command -> return_tactical loc (TacticAst.Command cmd) ]
     | "sequence" LEFTA
       [ tactics = LIST1 NEXT SEP SYMBOL ";" ->
-          return_tactical loc (TacticAst.Seq tactics)
+          (match tactics with
+          | [tactic] -> tactic
+          | _ -> return_tactical loc (TacticAst.Seq tactics))
       ]
     | "then" NONA
       [ tac = tactical;