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
(fun _ k -> k+1) k aux metasenv t
in
aux 0 metasenv proofterm
- in
+ in *)
debug (lazy (NCicPp.ppterm ~metasenv ~subst ~context proofterm));
(*
let stamp = Unix.gettimeofday () in
let bag,clause = P.mk_passive bag (t,ty) in
if Terms.is_eq_clause clause then
P.forward_infer_step (P.replace_bag s bag) clause 0
- else (prerr_endline "not eq"; s)
+ else (debug (lazy "not eq"); s)
;;
let index_obj s uri =
let obj = NCicEnvironment.get_checked_obj uri in
+ debug (lazy ("indexing : " ^ (NUri.string_of_uri uri)));
+ debug (lazy ("no : " ^ (string_of_int (fst (Obj.magic uri)))));
match obj with
| (_,d,[],[],NCic.Constant(_,_,Some(_),ty,_)) ->
let nref = NReference.reference_of_spec uri (NReference.Def d) in