It is now possible to declare new aliases using the old syntax

[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 633d98ea9d69bece6e5c6de070adbdc8be59269f..324231b50db3e0bdc9655036535acc93f9f8fbe1 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -629,10 +629,12 @@ EXTEND
         let rex = Str.regexp ("^"^ident^"$") in
         if Str.string_match rex id 0 then
           if (try ignore (UriManager.uri_of_string uri); true
-              with UriManager.IllFormedUri _ -> false)
+              with UriManager.IllFormedUri _ -> false) ||
+             (try ignore (NReference.reference_of_string uri); true
+              with NReference.IllFormedReference _ -> false)
           then
             L.Ident_alias (id, uri)
-          else 
+          else
             raise
              (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
         else