cicNotation* ==> notation*

[helm.git] / matita / components / lexicon / lexiconAstPp.ml

diff --git a/matita/components/lexicon/lexiconAstPp.ml b/matita/components/lexicon/lexiconAstPp.ml
index c11e4f0945440a1d3ee83d5b70ca26125d0c799c..cf8ea3d03540b23d505d677f99568f2696d4086c 100644 (file)
--- 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 -> ""