X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_cic_content%2FnTermCicContent.ml;h=dbd6523cf946b302eead79de25beb5fca0037549;hb=42aa528129728611cae9da02904886522b08f94a;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..dbd6523cf 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 ()
@@ -43,12 +43,6 @@ type term_info =
   { sort: (Cic.id, Ast.sort_kind) Hashtbl.t;
     uri: (Cic.id, UriManager.uri) Hashtbl.t;
   }
-
-let get_types uri =
-  let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
-    match o with
-      | Cic.InductiveDefinition (l,_,leftno,_) -> l, leftno 
-      | _ -> assert false
 *)
 
 let idref register_ref =
@@ -89,7 +83,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 +271,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 +299,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
@@ -340,14 +334,6 @@ in
 ;;
 
 (*
-let ast_of_acic ~output_type id_to_sort annterm =
-  debug_print (lazy ("ast_of_acic <- "
-    ^ 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));
-  ast, term_info.uri
-
 let fresh_id =
   fun () ->
     incr counter;