+let rec max_weight_in_proof current =
+ function
+ | Exact _ -> current
+ | Step (_, (_,id1,(_,id2),_)) ->
+ let eq1 = Hashtbl.find id_to_eq id1 in
+ let eq2 = Hashtbl.find id_to_eq id2 in
+ let (w1,p1,(_,_,_,_),_,_) = open_equality eq1 in
+ let (w2,p2,(_,_,_,_),_,_) = open_equality eq2 in
+ let current = max current w1 in
+ let current = max_weight_in_proof current p1 in
+ let current = max current w2 in
+ max_weight_in_proof current p2
+
+let max_weight_in_goal_proof =
+ List.fold_left
+ (fun current (_,_,id,_,_) ->
+ let eq = Hashtbl.find id_to_eq id in
+ let (w,p,(_,_,_,_),_,_) = open_equality eq in
+ let current = max current w in
+ max_weight_in_proof current p)
+
+let max_weight goal_proof proof =
+ let current = max_weight_in_proof 0 proof in
+ max_weight_in_goal_proof current goal_proof
+