X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flexicon%2FlexiconEngine.ml;h=805da25c8e53c18340649fcbd6ead78db3b6fdde;hb=9e7df95a820cb91d075f1a20d703175da874596c;hp=c86e161357eb9cd136c6a1a0fd9ef8aa6c37835b;hpb=8cfe7f6b2f82db366cf7c868e779b9b1783b637f;p=helm.git

diff --git a/helm/software/components/lexicon/lexiconEngine.ml b/helm/software/components/lexicon/lexiconEngine.ml
index c86e16135..805da25c8 100644
--- a/helm/software/components/lexicon/lexiconEngine.ml
+++ b/helm/software/components/lexicon/lexiconEngine.ml
@@ -120,12 +120,15 @@ let rec eval_command ?(mode=L.WithPreferences) status cmd =
           ->
            let item = DisambiguateTypes.Id id in
             begin try
-              let uri =
-               match DisambiguateTypes.Environment.find item status.aliases with
-                  L.Ident_alias (_, uri)-> UriManager.uri_of_string uri
-                | _ -> assert false
-              in
-               CicNotationPt.UriPattern uri
+              match DisambiguateTypes.Environment.find item status.aliases with
+                 L.Ident_alias (_, uri) ->
+                  (try
+                    CicNotationPt.NRefPattern
+                     (NReference.reference_of_string uri)
+                   with
+                    NReference.IllFormedReference _ ->
+                     CicNotationPt.UriPattern (UriManager.uri_of_string uri))
+               | _ -> assert false
              with Not_found -> 
               prerr_endline ("LexiconEngine.eval_command: domain item not found: " ^ 
                (DisambiguateTypes.string_of_domain_item item));