cicNotation* ==> notation*

[helm.git] / matita / components / content_pres / content2pres.ml

diff --git a/matita/components/content_pres/content2pres.ml b/matita/components/content_pres/content2pres.ml
index 617c9ddcacbb6fa0aed9dfd47e5f3b68d0db740b..cd2e62c21c06631316f2baed41142bd86ef7412b 100644 (file)
--- a/matita/components/content_pres/content2pres.ml
+++ b/matita/components/content_pres/content2pres.ml
@@ -916,7 +916,7 @@ let definition2pres ?recno term2pres d =
   let name = match d.Content.def_name with Some x -> x|_->assert false in
   let rno = match recno with None -> -1 (* cofix *) | Some x -> x in
   let ty = d.Content.def_type in
-  let module P = CicNotationPt in
+  let module P = NotationPt in
   let rec split_pi i t = 
     if i <= 1 then 
       match t with 
@@ -994,7 +994,7 @@ let njoint_def2pres term2pres joint_kind defs =
 
 let ncontent2pres0
   ?skip_initial_lambdas ?(skip_thm_and_qed=false) term2pres 
-  (id,params,metasenv,obj : CicNotationPt.term Content.cobj) 
+  (id,params,metasenv,obj : NotationPt.term Content.cobj) 
 =
   match obj with
   | `Def (Content.Const, thesis, `Proof p) ->