Change Sort.merge (deprecated) with List.merge

[helm.git] / matitaB / components / ng_cic_content / interpretations.ml

diff --git a/matitaB/components/ng_cic_content/interpretations.ml b/matitaB/components/ng_cic_content/interpretations.ml
index 226eecdfde7800c7d06bbd2868acd7c215398902..ed2b58a79235389ae0f335975aad982a454f9854 100644 (file)
--- a/matitaB/components/ng_cic_content/interpretations.ml
+++ b/matitaB/components/ng_cic_content/interpretations.ml
@@ -67,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 >}
@@ -89,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 = 
@@ -112,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)
 
@@ -338,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 =