+;;
+
+let wfo goalproof =
+ let rec aux acc id =
+ let p,_,_ = proof_of_id id in
+ match p with
+ | Exact _ -> id :: acc
+ | Step (_,(_,id1, (_,id2), _)) ->
+ let acc = if not (List.mem id1 acc) then aux acc id1 else acc in
+ let acc = if not (List.mem id2 acc) then aux acc id2 else acc in
+ id :: acc
+ in
+ List.fold_left (fun acc (_,id,_,_) -> aux acc id) [] goalproof
+;;
+
+let string_of_id names id =
+ try
+ let (_,(p,_),(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in
+ match p with
+ | Exact t ->
+ Printf.sprintf "%d = %s: %s = %s" id
+ (CicPp.pp t names) (CicPp.pp l names) (CicPp.pp r names)
+ | Step (_,(step,id1, (_,id2), _) ) ->
+ Printf.sprintf "%5d: %s %4d %4d %s = %s" id
+ (if step = SuperpositionRight then "SupR" else "Demo")
+ id1 id2 (CicPp.pp l names) (CicPp.pp r names)
+ with
+ Not_found -> assert false
+
+let pp_proof names goalproof =
+ String.concat "\n" (List.map (string_of_id names) (wfo goalproof))