+let infer_goal_set env active goals =
+ let active_goals, passive_goals = goals in
+ let rec aux = function
+ | [] -> goals
+ | hd::tl ->
+ let changed,selected = simplify_goal env hd active in
+ if changed then
+ prerr_endline ("--------------- goal semplificato");
+ let (_,_,t1) = selected in
+ if (List.exists
+ (fun (_,_,t) ->
+ Equality.meta_convertibility t t1)
+ active_goals) then aux tl
+ else
+ let passive_goals = tl in
+ let new_passive_goals =
+ if Utils.metas_of_term t1 = [] then passive_goals
+ else
+ let new' =
+ Indexing.superposition_left env (snd active) selected in
+ passive_goals @ new'
+ in
+ selected::active_goals, new_passive_goals
+ in
+ aux passive_goals
+;;
+
+(* old