X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fcomponents%2Fng_cic_content%2FnTermCicContent.ml;h=dbd6523cf946b302eead79de25beb5fca0037549;hb=42aa528129728611cae9da02904886522b08f94a;hp=5cfda009c26bb564af3a45205860d931c320befb;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/components/ng_cic_content/nTermCicContent.ml b/matita/components/ng_cic_content/nTermCicContent.ml
index 5cfda009c..dbd6523cf 100644
--- a/matita/components/ng_cic_content/nTermCicContent.ml
+++ b/matita/components/ng_cic_content/nTermCicContent.ml
@@ -27,13 +27,15 @@
 
 open Printf
 
-module Ast = CicNotationPt
+module Ast = NotationPt
 
 let debug = false
 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
 
 type id = string
 
+let hide_coercions = ref true;;
+
 (*
 type interpretation_id = int
 
@@ -41,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 =
@@ -87,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 ->
@@ -143,7 +139,7 @@ let nast_of_cic0 status
          | Some n -> idref (Ast.Num (string_of_int n, -1))
          | None ->
             let args =
-             if not !Acic2content.hide_coercions then args
+             if not !hide_coercions then args
              else
               match
                NCicCoercion.match_coercion status ~metasenv ~context ~subst t
@@ -275,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
@@ -303,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
@@ -320,7 +316,7 @@ let rec nast_of_cic1 status ~idref ~output_type ~metasenv ~subst ~context term =
       in
       let _, symbol, args, _ =
         try
-          TermAcicContent.find_level2_patterns32 pid
+          Interpretations.find_level2_patterns32 pid
         with Not_found -> assert false
       in
       let ast = instantiate32 idrefs env symbol args in
@@ -333,19 +329,11 @@ let load_patterns32 t =
  in
   set_compiled32 (lazy (Ncic2astMatcher.Matcher32.compiler t))
 in
- TermAcicContent.add_load_patterns32 load_patterns32;
- TermAcicContent.init ()
+ Interpretations.add_load_patterns32 load_patterns32;
+ Interpretations.init ()
 ;;
 
 (*
-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;