1
2
3

let static_modules = ""
let core_libs = "lib/clib.cma lib/lib.cma kernel/kernel.cma intf/intf.cma library/library.cma engine/engine.cma pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma parsing/parsing.cma printing/printing.cma tactics/tactics.cma vernac/vernac.cma stm/stm.cma toplevel/toplevel.cma API/API.cma "
let core_objs = "Coq_config Terminal Canary Hook Hashset Hashcons CSet CMap Int Dyn HMap Option Store Exninfo Backtrace IStream Flags Control Loc CAst DAst CList CString Deque CObj CArray CStack Util Stateid Pp Feedback CUnix Envars Aux_file Monad CoqProject_file CErrors CWarnings Bigint Segmenttree Unicodetable Unicode Minisys System CThread Spawn Trie CProfile Explore Predicate Rtree Heap Unionfind Genarg CEphemeron Future RemoteCounter Names Uint31 Univ UGraph Esubst Sorts Evar Constr Context Vars Term Mod_subst Cbytecodes Copcodes Cemitcodes Opaqueproof Declarations Entries Nativevalues CPrimitives Declareops Retroknowledge Conv_oracle Pre_env Cbytegen Nativelambda Nativecode Nativelib Environ CClosure Reduction Nativeconv Type_errors Modops Inductive Typeops Indtypes Cooking Term_typing Subtyping Mod_typing Nativelibrary Safe_typing Vm Csymtable Vconv Constrexpr Evar_kinds Genredexpr Locus Notation_term Decl_kinds Extend Glob_term Misctypes Pattern Vernacexpr Libnames Globnames Libobject Summary Nametab Global Lib Declaremods Loadpath Library States Kindops Dischargedhypsmap Goptions Decls Heads Keys Coqlib Universes Univops UState Nameops Evd EConstr Namegen Termops Evarutil Logic_monad Proofview_monad Proofview Ftactic Geninterp Ltac_pretype Locusops Pretype_errors Reductionops Inductiveops Vnorm Arguments_renaming Nativenorm Retyping Cbv Find_subterm Evardefine Evarsolve Recordops Evarconv Typing Miscops Glob_ops Redops Patternops Constr_matching Tacred Typeclasses_errors Typeclasses Classops Program Coercion Detyping Indrec Cases Pretyping Unification Univdecls Tactypes Stdarg Genintern Notation_ops Notation Syntax_def Smartlocate Constrexpr_ops Ppextend Dumpglob Topconstr Reserve Impargs Implicit_quantifiers Constrintern Modintern Constrextern Discharge Declare Miscprint Goal Evar_refiner Proof_type Logic Refine Proof Proof_bullet Proof_global Redexpr Refiner Tacmach Pfedit Clenv Clenvtac Tok CLexer Pcoq Egramml Egramcoq G_constr G_vernac G_prim G_proofs Genprint Pputils Ppconstr Printer Printmod Prettyp Ppvernac Dnet Dn Btermdn Tacticals Hipattern Ind_tables Eqschemes Elimschemes Tactics Elim Equality Contradiction Inv Leminv Hints Auto Eauto Class_tactics Term_dnet Eqdecide Autorewrite Vernacprop Proof_using Lemmas Himsg ExplainErr Class Locality Metasyntax Auto_ind_decl Search Indschemes DeclareDef Obligations Command Classes Record Assumptions Vernacstate Vernacinterp Mltop Topfmt Vernacentries Spawned Dag Vcs TQueue WorkerPool Vernac_classifier CoqworkmgrApi WorkerLoop AsyncTaskQueue Stm ProofBlockDelimiter Vio_checking Vernac Usage Coqloop Coqinit Coqtop API"