+ with
+ | Sup.Success (bag, _, (i,_,_,_)) ->
+ let l =
+ let rec traverse ongoal (accg,acce) i =
+ match Terms.M.find i bag with
+ | (id,_,_,Terms.Exact _) ->
+ if ongoal then [i],acce else
+ if (List.mem i acce) then accg,acce else accg,acce@[i]
+ | (_,_,_,Terms.Step (_,i1,i2,_,_,_)) ->
+ if (not ongoal) && (List.mem i acce) then accg,acce
+ else
+ let accg,acce =
+ traverse false (traverse ongoal (accg,acce) i1) i2
+ in
+ if ongoal then i::accg,acce else accg,i::acce
+ in
+ let gsteps,esteps = traverse true ([],[]) i in
+ (List.rev esteps)@gsteps
+ in
+ prerr_endline (Printf.sprintf "Found proof in %d iterations, %fs"
+ !nb_iter
+ (Unix.gettimeofday() -. timeout +. amount_of_time));
+ (* prerr_endline "Proof:";
+ List.iter (fun x -> prerr_endline (string_of_int x);
+ prerr_endline (Pp.pp_unit_clause (Terms.M.find x bag))) l;*)
+ let proofterm = B.mk_proof bag i l in
+ prerr_endline (Printf.sprintf "Got proof term, %fs"
+ (Unix.gettimeofday() -. timeout +. amount_of_time));
+ 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 `Term 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
+ let metasenv, subst, proofterm, _prooftype =
+ NCicRefiner.typeof
+ (rdb#set_coerc_db NCicCoercion.empty_db)
+ metasenv subst context proofterm None
+ in
+ proofterm, metasenv, subst
+ | Failure s ->
+ prerr_endline s;
+ prerr_endline
+ (Printf.sprintf "FAILURE in %d iterations" !nb_iter); assert false