-- Check whether the entire module is deprecated
-- This happens only once per module
let { mod_deprecs = checkModDeprec mod_deprec } ;
-- Add exports and deprecations to envt
-- Check whether the entire module is deprecated
-- This happens only once per module
let { mod_deprecs = checkModDeprec mod_deprec } ;
-- Add exports and deprecations to envt