X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Flexicon%2FlexiconEngine.ml;h=a0dfb87cf227a375ebc2e3a59243b2a2e54bf0ea;hb=3f9cb46b5e167955e85b3d2544f1bed90f1a25b7;hp=39d95a7f2cd02c5f503390286c502a08e7e09d08;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/components/lexicon/lexiconEngine.ml b/matita/components/lexicon/lexiconEngine.ml
index 39d95a7f2..a0dfb87cf 100644
--- a/matita/components/lexicon/lexiconEngine.ml
+++ b/matita/components/lexicon/lexiconEngine.ml
@@ -124,23 +124,18 @@ let rec eval_command ?(mode=L.WithPreferences) sstatus cmd =
   | L.Interpretation (loc, dsc, (symbol, args), cic_appl_pattern) ->
      let rec disambiguate =
       function
-         CicNotationPt.ApplPattern l ->
-          CicNotationPt.ApplPattern (List.map disambiguate l)
-       | CicNotationPt.VarPattern id
+         NotationPt.ApplPattern l ->
+          NotationPt.ApplPattern (List.map disambiguate l)
+       | NotationPt.VarPattern id
           when not
            (List.exists
-            (function (CicNotationPt.IdentArg (_,id')) -> id'=id) args)
+            (function (NotationPt.IdentArg (_,id')) -> id'=id) args)
           ->
            let item = DisambiguateTypes.Id id in
             begin try
               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))
+                  NotationPt.NRefPattern (NReference.reference_of_string uri)
                | _ -> assert false
              with Not_found -> 
               prerr_endline ("LexiconEngine.eval_command: domain item not found: " ^