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

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 1b2ef3657..c64fcd42c 100644
--- 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)
@@ -362,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)))
 
@@ -439,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