- moved up in the grammar precedences command entry so that sequence of

  commands are not permitted
- added parsing of "abort" command

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 8eca106304e96def0c883fa11885889751abcfcd..1b2ef365730c6310ac89997b711eb98f92f81af9 100644 (file)
--- 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)