| Some eq_uri ->
try
let bag, current = Equality.equality_of_term bag term ty newmetas in
- let bag, current = Equality.fix_metas bag current in
- match add_to_active_aux bag active passive env eq_uri current with
- | _,a,p,b -> a,p,b
+ let w,_,_,_,_ = Equality.open_equality current in
+ if w > 100 then
+ (HLog.debug
+ ("skipping giant " ^ CicPp.ppterm term ^ " of weight " ^
+ string_of_int w); active, passive, bag)
+ else
+ let bag, current = Equality.fix_metas bag current in
+ match add_to_active_aux bag active passive env eq_uri current with
+ | _,a,p,b -> a,p,b
with
| Equality.TermIsNotAnEquality -> active, passive, bag
;;