comment improvements
consistent use of IsLocal and IsNull local notations
move ooextendable_isnull_fibers to Extensions.v
avoid inexcusably slow typeclass inference