X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicCoercion.ml;h=04fddee83fdee339546a4bf42484bdf3e23d8f73;hb=123e66ead6ee8f502bd2fc2baf5482fe78ae6f34;hp=037c5c6e2ce6b80f23e4bbacfe2f0471162e1b8b;hpb=c1f12859e933fdbd2ca5e054fc23c01f79f8cc56;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicCoercion.ml b/helm/software/components/ng_refiner/nCicCoercion.ml
index 037c5c6e2..04fddee83 100644
--- a/helm/software/components/ng_refiner/nCicCoercion.ml
+++ b/helm/software/components/ng_refiner/nCicCoercion.ml
@@ -14,6 +14,9 @@
 let debug s = prerr_endline (Lazy.force s);;
 let debug _ = ();;
 
+let convert_term = ref (fun _ _ -> assert false);;
+let set_convert_term f = convert_term := f;;
+
 module COT : Set.OrderedType 
 with type t = string * NCic.term * int * int  * NCic.term *
 NCic.term = 
@@ -31,6 +34,12 @@ type db = DB.t * DB.t
 
 let empty_db = DB.empty,DB.empty
 
+class type g_status =
+ object
+  inherit NCicUnifHint.g_status
+  method coerc_db: db
+ end
+
 class status =
  object
   inherit NCicUnifHint.status
@@ -38,21 +47,18 @@ class status =
   method coerc_db = db
   method set_coerc_db v = {< db = v >}
   method set_coercion_status
-  : 'status. < coerc_db : db; uhint_db: NCicUnifHint.db; .. > as 'status -> 
-          'self
-          = fun o -> {< db = o#coerc_db >}#set_unifhint_status o
+   : 'status. #g_status as 'status -> 'self
+   = fun o -> {< db = o#coerc_db >}#set_unifhint_status o
  end
 
 let index_coercion status name c src tgt arity arg =
   let db_src,db_tgt = status#coerc_db in
   let data = (name,c,arity,arg,src,tgt) in
-
   debug (lazy ("INDEX:" ^ 
     NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^
     NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] tgt ^ "  :=  " ^
     NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] c ^ " " ^ 
     string_of_int arg ^ " " ^ string_of_int arity));
-
   let db_src = DB.index db_src src data in
   let db_tgt = DB.index db_tgt tgt data in
   status#set_coerc_db (db_src, db_tgt)
@@ -64,7 +70,7 @@ let index_old_db odb (status : #status) =
        List.fold_left 
          (fun status (uri,_,arg) ->
            try
-            let c=fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)) in
+            let c=fst (!convert_term uri (CicUtil.term_of_uri uri)) in
             let arity = match tgt with | CoercDb.Fun i -> i | _ -> 0 in
             let src, tgt = 
               let cty = NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] c in