X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matitaB%2Fcomponents%2Fng_cic_content%2Finterpretations.ml;h=ed2b58a79235389ae0f335975aad982a454f9854;hb=3b7b8afcb429a60d716d5226a5b6ab0d003228b1;hp=c898c0faaf9c8e487cb429fabad72e46ec051395;hpb=6f020d79dea92003151e5e588fd73452f20ffb2c;p=helm.git

diff --git a/matitaB/components/ng_cic_content/interpretations.ml b/matitaB/components/ng_cic_content/interpretations.ml
index c898c0faa..ed2b58a79 100644
--- a/matitaB/components/ng_cic_content/interpretations.ml
+++ b/matitaB/components/ng_cic_content/interpretations.ml
@@ -38,11 +38,6 @@ let hide_coercions = ref true;;
 
 type cic_id = string
 
-type term_info =
-  { sort: (cic_id, Ast.sort_kind) Hashtbl.t;
-    uri: (cic_id, NReference.reference) Hashtbl.t;
-  }
-
 module IntMap = Map.Make(struct type t = int let compare = compare end);;
 module StringMap = Map.Make(String);;
 
@@ -72,9 +67,9 @@ class type g_status =
     method interp_db: db
   end
  
-class virtual status =
+class virtual status uid =
  object(self)
-   inherit NCicCoercion.status
+   inherit NCicCoercion.status uid
    val mutable interp_db = None (* mutable only to initialize it :-( *)
    method interp_db = match interp_db with None -> assert false | Some x -> x
    method set_interp_db v = {< interp_db = Some v >}
@@ -94,7 +89,7 @@ let level_of_uri u =
 let find_level2_patterns32 status pid =
  IntMap.find pid status#interp_db.level2_patterns32
 
-let instantiate32 env symbol args =
+let instantiate32 env symbol dsc args =
   let rec instantiate_arg = function
     | Ast.IdentArg (n, name) ->
         let t = 
@@ -117,7 +112,7 @@ let instantiate32 env symbol args =
         in
         add_lambda t (n - count_lambda t)
   in
-  let head = Ast.Symbol (symbol, None) in
+  let head = Ast.Symbol (symbol, Some (None, dsc)) in
   if args = [] then head
   else Ast.Appl (head :: List.map instantiate_arg args)
 
@@ -343,12 +338,12 @@ let rec nast_of_cic1 status ~output_type ~metasenv ~subst ~context term =
             term
         ) env
       in
-      let _, symbol, args, _ =
+      let dsc, symbol, args, _ =
         try
          find_level2_patterns32 status pid
         with Not_found -> assert false
       in
-      instantiate32 env symbol args 
+      instantiate32 env symbol dsc args 
 ;;
 
 let nmap_context0 status ~metasenv ~subst context =