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

diff --git a/matita/components/lexicon/lexiconAstPp.ml b/matita/components/lexicon/lexiconAstPp.ml
index c11e4f094..cf8ea3d03 100644
--- a/matita/components/lexicon/lexiconAstPp.ml
+++ b/matita/components/lexicon/lexiconAstPp.ml
@@ -29,8 +29,8 @@ open Printf
 
 open LexiconAst
 
-let pp_l1_pattern = CicNotationPp.pp_term
-let pp_l2_pattern = CicNotationPp.pp_term
+let pp_l1_pattern = NotationPp.pp_term
+let pp_l2_pattern = NotationPp.pp_term
 
 let pp_alias = function
   | Ident_alias (id, uri) -> sprintf "alias id \"%s\" = \"%s\"." id uri
@@ -50,7 +50,7 @@ let pp_associativity = function
 let pp_precedence i = sprintf "with precedence %d" i
 
 let pp_argument_pattern = function
-  | CicNotationPt.IdentArg (eta_depth, name) ->
+  | NotationPt.IdentArg (eta_depth, name) ->
       let eta_buf = Buffer.create 5 in
       for i = 1 to eta_depth do
         Buffer.add_string eta_buf "\\eta."
@@ -61,7 +61,7 @@ let pp_interpretation dsc symbol arg_patterns cic_appl_pattern =
   sprintf "interpretation \"%s\" '%s %s = %s."
     dsc symbol
     (String.concat " " (List.map pp_argument_pattern arg_patterns))
-    (CicNotationPp.pp_cic_appl_pattern cic_appl_pattern)
+    (NotationPp.pp_cic_appl_pattern cic_appl_pattern)
  
 let pp_dir_opt = function
   | None -> ""