urimanager removed

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

diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml
index 110c9e912c6b5946ddd603ae20b3a3859a3e3812..f0da64a51586c86ee93c4b71f64894127827fb9a 100644 (file)
--- a/matita/components/grafite_parser/grafiteParser.ml
+++ b/matita/components/grafite_parser/grafiteParser.ml
@@ -461,9 +461,7 @@ EXTEND
         let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in
         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) ||
-             (try ignore (NReference.reference_of_string uri); true
+          if (try ignore (NReference.reference_of_string uri); true
               with NReference.IllFormedReference _ -> false)
           then
             L.Ident_alias (id, uri)
@@ -532,8 +530,7 @@ EXTEND
       ]
     ];
     level3_term: [
-      [ u = URI -> N.UriPattern (UriManager.uri_of_string u)
-      | r = NREF -> N.NRefPattern (NReference.reference_of_string r)
+      [ r = NREF -> N.NRefPattern (NReference.reference_of_string r)
       | IMPLICIT -> N.ImplicitPattern
       | id = IDENT -> N.VarPattern id
       | LPAREN; terms = LIST1 SELF; RPAREN ->