X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_cic_content%2FnTermCicContent.ml;h=18685f35b808f4e7b5bdf36358cf08279d4a4984;hb=8a660ee06d72cfee52c707bb1d8d8be3bab0d682;hp=b8d474cc2e260d5e9779baaf0cf002521cd4611a;hpb=5553ac7623425bce6f34eed6e17d4f0f8163e9aa;p=helm.git

diff --git a/matita/components/ng_cic_content/nTermCicContent.ml b/matita/components/ng_cic_content/nTermCicContent.ml
index b8d474cc2..18685f35b 100644
--- a/matita/components/ng_cic_content/nTermCicContent.ml
+++ b/matita/components/ng_cic_content/nTermCicContent.ml
@@ -27,7 +27,7 @@
 
 open Printf
 
-module Ast = CicNotationPt
+module Ast = NotationPt
 
 let debug = false
 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
@@ -89,7 +89,7 @@ let destroy_nat =
 (* CODICE c&p da NCicPp *)
 let nast_of_cic0 status
  ~(idref:
-    ?reference:NReference.reference -> CicNotationPt.term -> CicNotationPt.term)
+    ?reference:NReference.reference -> NotationPt.term -> NotationPt.term)
  ~output_type ~metasenv ~subst k ~context =
   function
     | NCic.Rel n ->
@@ -277,7 +277,7 @@ let instantiate32 idrefs env symbol args =
         in
         let rec add_lambda t n =
           if n > 0 then
-            let name = CicNotationUtil.fresh_name () in
+            let name = NotationUtil.fresh_name () in
             Ast.Binder (`Lambda, (Ast.Ident (name, None), None),
               Ast.Appl [add_lambda t (n - 1); Ast.Ident (name, None)])
           else
@@ -305,7 +305,7 @@ let rec nast_of_cic1 status ~idref ~output_type ~metasenv ~subst ~context term =
            idref
             ~reference:
               (match term with NCic.Const nref -> nref | _ -> assert false)
-           (CicNotationPt.Ident ("dummy",None))
+           (NotationPt.Ident ("dummy",None))
           in
            match attrterm with
               Ast.AttributedTerm (`IdRef id, _) -> id
@@ -345,7 +345,7 @@ let ast_of_acic ~output_type id_to_sort annterm =
     ^ CicPp.ppterm (Deannotate.deannotate_term annterm)));
   let term_info = { sort = id_to_sort; uri = Hashtbl.create 211 } in
   let ast = ast_of_acic1 ~output_type term_info annterm in
-  debug_print (lazy ("ast_of_acic -> " ^ CicNotationPp.pp_term ast));
+  debug_print (lazy ("ast_of_acic -> " ^ NotationPp.pp_term ast));
   ast, term_info.uri
 
 let fresh_id =