Names Univ Esubst Sorts Evar Constr Context Vars Term Mod_subst Cbytecodes Copcodes Cemitcodes Nativevalues Lazyconstr Declareops Retroknowledge Pre_env Cbytegen Nativelambda Nativecode Nativelib Environ Conv_oracle Closure Reduction Nativeconv Type_errors Modops Inductive Typeops Indtypes Cooking Term_typing Subtyping Mod_typing Nativelibrary Safe_typing Vm Csymtable Vconv