X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicCoercion.ml;h=04fddee83fdee339546a4bf42484bdf3e23d8f73;hb=0920a5755553774f5b41d7603318ea997ecbdca5;hp=fd697265a2464e4c9255eb6f844fd796b2fe6bac;hpb=7aafcce5268d75a57e69b4085436850567a6c869;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicCoercion.ml b/helm/software/components/ng_refiner/nCicCoercion.ml
index fd697265a..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 = 
@@ -67,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