X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FcicTextualParser2.ml;h=1b2ef365730c6310ac89997b711eb98f92f81af9;hb=9af598ece6749c1854799f5aa83133b9e3da052c;hp=8eca106304e96def0c883fa11885889751abcfcd;hpb=5f57966efd85fb295701f06fd0488e9fe1bbb99f;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 8eca10630..1b2ef3657 100644
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -304,7 +304,9 @@ EXTEND
   ];
   tactical0: [ [ t = tactical; SYMBOL "." -> t ] ];
   tactical:
-    [ "sequence" LEFTA
+    [ "command" NONA
+      [ cmd = command -> return_tactical loc (TacticAst.Command cmd) ]
+    | "sequence" LEFTA
       [ tactics = LIST1 NEXT SEP SYMBOL ";" ->
           return_tactical loc (TacticAst.Seq tactics)
       ]
@@ -329,7 +331,6 @@ EXTEND
       | [ IDENT "id" | IDENT "Id" ] -> return_tactical loc TacticAst.IdTac
       | PAREN "("; tac = tactical; PAREN ")" -> return_tactical loc tac
       | tac = tactic -> return_tactical loc (TacticAst.Tactic tac)
-      | cmd = command -> return_tactical loc (TacticAst.Command cmd)
       ]
     ];
   theorem_flavour: [  (* all flavours but Goal *)
@@ -341,7 +342,8 @@ EXTEND
     ]
   ];
   command: [
-    [ [ IDENT "proof" | IDENT "Proof" ] -> return_command loc TacticAst.Proof
+    [ [ IDENT "abort" | IDENT "Abort" ] -> return_command loc TacticAst.Abort
+    | [ IDENT "proof" | IDENT "Proof" ] -> return_command loc TacticAst.Proof
     | [ IDENT "quit"  | IDENT "Quit"  ] -> return_command loc TacticAst.Quit
     | [ IDENT "qed"   | IDENT "Qed"   ] ->
         return_command loc (TacticAst.Qed None)