X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Flexicon%2FlexiconMarshal.ml;h=6693de21492b394a0817b3fcb41161fd909677d8;hb=8a660ee06d72cfee52c707bb1d8d8be3bab0d682;hp=5d69fafc002cd6751f69813d026720a068d3654a;hpb=5553ac7623425bce6f34eed6e17d4f0f8163e9aa;p=helm.git

diff --git a/matita/components/lexicon/lexiconMarshal.ml b/matita/components/lexicon/lexiconMarshal.ml
index 5d69fafc0..6693de214 100644
--- a/matita/components/lexicon/lexiconMarshal.ml
+++ b/matita/components/lexicon/lexiconMarshal.ml
@@ -43,15 +43,15 @@ let rehash_cmd_uris =
   | LexiconAst.Interpretation (loc, dsc, args, cic_appl_pattern) ->
       let rec aux =
         function
-        | CicNotationPt.UriPattern uri ->
-            CicNotationPt.UriPattern (rehash_uri uri)
-        | CicNotationPt.NRefPattern (NReference.Ref (uri,spec)) ->
+        | NotationPt.UriPattern uri ->
+            NotationPt.UriPattern (rehash_uri uri)
+        | NotationPt.NRefPattern (NReference.Ref (uri,spec)) ->
            let uri = NCicLibrary.refresh_uri uri in
-            CicNotationPt.NRefPattern (NReference.reference_of_spec uri spec)
-        | CicNotationPt.ApplPattern args ->
-            CicNotationPt.ApplPattern (List.map aux args)
-        | CicNotationPt.VarPattern _
-        | CicNotationPt.ImplicitPattern as pat -> pat
+            NotationPt.NRefPattern (NReference.reference_of_spec uri spec)
+        | NotationPt.ApplPattern args ->
+            NotationPt.ApplPattern (List.map aux args)
+        | NotationPt.VarPattern _
+        | NotationPt.ImplicitPattern as pat -> pat
       in
       let appl_pattern = aux cic_appl_pattern in
       LexiconAst.Interpretation (loc, dsc, args, appl_pattern)