- let _,_,_,_,nobj = obj in
+ let _,_,_,_,nobj = obj in
+ (* attempting to generate an inversion principle on the maximum
+ * universe can take a long time to fail: this code removes maximal
+ * sorts from the universe list *)
+ let universes = NCicEnvironment.get_universes () in
+ let max_univ = List.fold_left max [] universes in
+ let universes =
+ List.filter (fun x -> NCicEnvironment.universe_lt x max_univ)
+ universes
+ in