+ with
+ | Sup.Success (bag, _, (i,_,_,_)) ->
+ let l =
+ let module S =
+ HTopoSort.Make(struct type t=int let compare=Pervasives.compare end)
+ in
+ let module C : Set.S with type elt = int =
+ Set.Make(struct type t=int let compare=Pervasives.compare end)
+ in
+ let all id =
+ let rec traverse ongoal (accg,acce) i =
+ match Terms.M.find i bag with
+ | (_,_,_,Terms.Exact _) -> accg, acce
+ | (_,_,_,Terms.Step (_,i1,i2,_,_,_)) ->
+ let accg, acce =
+ if ongoal then C.add i1 accg, acce
+ else accg, C.add i1 acce
+ in
+ let acce = C.add i2 acce in
+ traverse false (traverse ongoal (accg,acce) i1) i2
+ in
+ traverse true (C.empty,C.empty) id
+ in
+ let esteps =
+ S.topological_sort (C.elements (snd (all i)))
+ (fun i -> C.elements (C.union (snd (all i)) (fst (all i)) ))
+ in
+ let gsteps =
+ S.topological_sort (C.elements (fst (all i)))
+ (fun i -> C.elements (fst (all i)))
+ in
+ let gsteps = List.rev gsteps in
+ esteps@(i::gsteps)
+ in
+ debug "YES!";
+ debug ("Meeting point : " ^ (string_of_int i));
+ debug "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 (NCicPp.ppterm ~metasenv:C.metasenv
+ ~subst:C.subst ~context:C.context proofterm);
+ let metasenv, subst, proofterm, _prooftype =
+ NCicRefiner.typeof
+ (rdb#set_coerc_db NCicCoercion.empty_db)
+ C.metasenv C.subst C.context proofterm None
+ in
+ proofterm, metasenv, subst
+ | Failure _ -> prerr_endline "FAILURE"; assert false