Names TransparentState Uint63 Parray Float64 Univ UGraph Esubst Sorts Evar Context Constr Vars Term CPrimitives Mod_subst Vmvalues Cbytecodes Copcodes Cemitcodes Opaqueproof Declarations Entries Nativevalues Declareops Retroknowledge Conv_oracle Environ Primred CClosure Relevanceops Reduction Clambda Nativelambda Cbytegen Nativecode Nativelib Csymtable Vm Vconv Nativeconv Type_errors Modops Inductive Typeops InferCumulativity IndTyping Indtypes Cooking Term_typing Subtyping Mod_typing Nativelibrary Section Safe_typing