+ (* concl_cost are the costants in the conclusion of the proof
+ while hyp_const are the constants in the hypothesis *)
+ let (_,concl_const) = NewConstraints.constants_of ty in
+ prerr_endline ("Ne sono rimasti " ^ string_of_int (List.length uris));
+ let hyp t set =
+ match t with
+ Some (_,Cic.Decl t) -> (NewConstraints.StringSet.union set (NewConstraints.constants_concl t))
+ | Some (_,Cic.Def (t,_)) -> (NewConstraints.StringSet.union set (NewConstraints.constants_concl t))
+ | _ -> set in
+ let hyp_const =
+ List.fold_right hyp ey NewConstraints.StringSet.empty in
+ prerr_endline (NewConstraints.pp_StringSet (NewConstraints.StringSet.union hyp_const concl_const));
+ (* uris with new constants in the proof are filtered *)
+ let uris = List.filter (Filter_auto.filter_new_constants conn (NewConstraints.StringSet.union hyp_const concl_const)) uris in