+NCicBlob.set_default_eqP()
+;;
+NCicProof.set_default_sig()
+;;
+
+let debug _ = ();;
+let print s = prerr_endline (Lazy.force s);;
+
+module B(C : NCicBlob.NCicContext): Orderings.Blob
+ with type t = NCic.term and type input = NCic.term
+ = Orderings.LPO(NCicBlob.NCicBlob(C))
+
+module NCicParamod(C : NCicBlob.NCicContext) = Paramod.Paramod(B(C))
+
+let readback rdb metasenv subst context (bag,i,fo_subst,l) =
+(*
+ List.iter (fun x ->
+ print_endline (Pp.pp_unit_clause ~margin:max_int
+ (fst(Terms.M.find x bag)))) l;
+*)
+ (* let stamp = Unix.gettimeofday () in *)
+ let proofterm,prooftype = NCicProof.mk_proof bag i fo_subst l in
+ (* debug (lazy (Printf.sprintf "Got proof term in %fs"
+ (Unix.gettimeofday() -. stamp))); *)
+(*
+ let metasenv, proofterm =
+ let rec aux k metasenv = function
+ | NCic.Meta _ as t -> metasenv, t
+ | NCic.Implicit _ ->
+ let metasenv, i, _, _ =
+ NCicMetaSubst.mk_meta metasenv context `IsTerm
+ in
+ metasenv, NCic.Meta (i,(k,NCic.Irl (List.length context)))
+ | t -> NCicUntrusted.map_term_fold_a
+ (fun _ k -> k+1) k aux metasenv t
+ in
+ aux 0 metasenv proofterm
+ in *)
+ debug (lazy (NCicPp.ppterm ~metasenv ~subst ~context proofterm));
+(*
+ let stamp = Unix.gettimeofday () in
+ let metasenv, subst, proofterm, _prooftype =
+ NCicRefiner.typeof
+ (rdb#set_coerc_db NCicCoercion.empty_db)
+ metasenv subst context proofterm None
+ in
+ print (lazy (Printf.sprintf "Refined in %fs"
+ (Unix.gettimeofday() -. stamp)));
+*)
+ proofterm, prooftype, metasenv, subst
+