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 =
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