notation on steroids: 'term 40 x' is a valid variable name in notation and

[helm.git] / helm / software / components / grafite_parser / grafiteParser.ml

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 101e55a547d77a6e29e8d2d058773a9475934af3..6fcb9dba4f0a8e83620b84534f68523ef2d1cd07 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -743,6 +743,9 @@ let exc_located_wrapper f =
   | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
   | Stdpp.Exc_located (floc, Stream.Error msg) ->
       raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
+  | Stdpp.Exc_located (floc, HExtlib.Localized(_,exn)) ->
+      raise
+       (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
   | Stdpp.Exc_located (floc, exn) ->
       raise
        (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))