debian version 0.0.6-6

[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 8eca106304e96def0c883fa11885889751abcfcd..c64fcd42cb96faad16d4efb759b3fcb52324ffe1 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -65,7 +65,8 @@ let return_tactic loc tactic = TacticAst.LocatedTactic (loc, tactic)
 let return_tactical loc tactical = TacticAst.LocatedTactical (loc, tactical)
 let return_command loc cmd = cmd
 
-let fail (x, y) msg =
+let fail floc msg =
+  let (x, y) = CicAst.loc_of_floc floc in
   failwith (Printf.sprintf "Error at characters %d - %d: %s" x y msg)
 
 let name_of_string = function
@@ -79,7 +80,7 @@ EXTEND
         try
           int_of_string num
         with Failure _ ->
-          let (x, y) = loc in
+          let (x, y) = CicAst.loc_of_floc loc in
           raise (Parse_error (sprintf
             "integer literal expected at characters %d-%d" x y))
     ]
@@ -109,7 +110,7 @@ EXTEND
   substituted_name: [ (* a subs.name is an explicit substitution subject *)
     [ s = [ IDENT | SYMBOL ];
       subst = OPT [
-        SYMBOL "\subst";  (* to avoid catching frequent "a [1]" cases *)
+        SYMBOL "\\subst";  (* to avoid catching frequent "a [1]" cases *)
         PAREN "[";
         substs = LIST1 [
           i = IDENT; SYMBOL <:unicode<Assign>> (* ≔ *); t = term -> (i, t)
@@ -304,7 +305,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 +332,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 +343,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)
@@ -360,7 +363,8 @@ END
 let exc_located_wrapper f =
   try
     Lazy.force f
-  with Stdpp.Exc_located ((x, y), exn) ->
+  with Stdpp.Exc_located (floc, exn) ->
+    let (x, y) = CicAst.loc_of_floc floc in
     raise (Parse_error (sprintf "parse error at characters %d-%d: %s" x y
         (Printexc.to_string exn)))
 
@@ -437,7 +441,8 @@ module EnvironmentP3 =
       else
         try
           Grammar.Entry.parse aliases (Stream.of_string s)
-        with Stdpp.Exc_located ((x, y), exn) ->
+        with Stdpp.Exc_located (floc, exn) ->
+          let (x, y) = CicAst.loc_of_floc floc in
           raise (Parse_error (sprintf "parse error at characters %d-%d: %s" x y
           (Printexc.to_string exn)))
   end