From 4c72514fddee0ca37b41f676a9beeacf4e2938ea Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 10 Feb 2005 15:54:00 +0000 Subject: [PATCH] - fix in intro parsing - avoid generating seq tactical for a 1-length sequences --- helm/ocaml/cic_disambiguation/cicTextualParser2.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index 4bfc7c445..d5f427c4f 100644 --- 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; -- 2.39.2