X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Flexicon%2FlexiconEngine.ml;h=805da25c8e53c18340649fcbd6ead78db3b6fdde;hb=497563d35f24bbcbcbd8d669d73284b76a823118;hp=6f30801a4b1c284d5ee6758e1bd02678217d2268;hpb=6cc401c4136bafb6515bd39d86db6b5a917318bf;p=helm.git

diff --git a/helm/software/components/lexicon/lexiconEngine.ml b/helm/software/components/lexicon/lexiconEngine.ml
index 6f30801a4..805da25c8 100644
--- a/helm/software/components/lexicon/lexiconEngine.ml
+++ b/helm/software/components/lexicon/lexiconEngine.ml
@@ -27,7 +27,7 @@
 
 module L = LexiconAst
 
-let debug = ref true
+let debug = ref false
 
 (* lexicon file name * ma file name *)
 exception IncludedFileNotCompiled of string * string 
@@ -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));