rocq-runtime-9.2.0-1.fc45 RPM for ppc64le

From Fedora Rawhide for ppc64le / r

Rocq is a formal proof management system.  It provides a formal language to
write mathematical definitions, executable algorithms and theorems together
with an environment for semi-interactive development of machine-checked proofs.

This package includes the Rocq prover core binaries, plugins, and tools, but
not the vernacular standard library.

Provides

• rocq-runtime
• coq-core
• ocaml(Abbreviation)
• ocaml(Abstract)
• ocaml(AcyclicGraph)
• ocaml(AllScheme)
• ocaml(Arguments_renaming)
• ocaml(Assumptions)
• ocaml(AsyncTaskQueue)
• ocaml(Attributes)
• ocaml(Auto)
• ocaml(Auto_ind_decl)
• ocaml(Autorewrite)
• ocaml(Aux_file)
• ocaml(Boot)
• ocaml(Boot__Env)
• ocaml(Boot__Path)
• ocaml(Boot__Usage)
• ocaml(Boot__Util)
• ocaml(Btauto_plugin)
• ocaml(Btauto_plugin__G_btauto)
• ocaml(Btauto_plugin__Refl_btauto)
• ocaml(Btermdn)
• ocaml(CArray)
• ocaml(CAst)
• ocaml(CClosure)
• ocaml(CDebug)
• ocaml(CEphemeron)
• ocaml(CErrors)
• ocaml(CLexer)
• ocaml(CList)
• ocaml(CMap)
• ocaml(CObj)
• ocaml(CPrimitives)
• ocaml(CSet)
• ocaml(CSig)
• ocaml(CString)
• ocaml(CThread)
• ocaml(CUnix)
• ocaml(CWarnings)
• ocaml(Canonical)
• ocaml(Cases)
• ocaml(Cbn)
• ocaml(Cbv)
• ocaml(Cc_core_plugin)
• ocaml(Cc_core_plugin__Ccalgo)
• ocaml(Cc_core_plugin__Ccprojectability)
• ocaml(Cc_core_plugin__Ccproof)
• ocaml(Cc_core_plugin__Cctac)
• ocaml(Cc_plugin)
• ocaml(Cc_plugin__G_congruence)
• ocaml(Ccompile)
• ocaml(Class_tactics)
• ocaml(Classes)
• ocaml(Clenv)
• ocaml(Coercion)
• ocaml(Coercionops)
• ocaml(Colors)
• ocaml(ComArguments)
• ocaml(ComAssumption)
• ocaml(ComCoercion)
• ocaml(ComDefinition)
• ocaml(ComExtraDeps)
• ocaml(ComFixpoint)
• ocaml(ComHints)
• ocaml(ComInductive)
• ocaml(ComPrimitive)
• ocaml(ComRewriteRule)
• ocaml(ComSearch)
• ocaml(ComTactic)
• ocaml(Combinators)
• ocaml(Common_compile)
• ocaml(Constant_typing)
• ocaml(Constr)
• ocaml(Constr_matching)
• ocaml(Constrexpr)
• ocaml(Constrexpr_ops)
• ocaml(Constrextern)
• ocaml(Constrintern)
• ocaml(Context)
• ocaml(Contradiction)
• ocaml(Control)
• ocaml(Conv_oracle)
• ocaml(Conversion)
• ocaml(Cooking)
• ocaml(CoqProject_file)
• ocaml(Coq_byte_config)
• ocaml(Coq_checklib)
• ocaml(Coq_checklib__Analyze)
• ocaml(Coq_checklib__CheckFlags)
• ocaml(Coq_checklib__CheckInductive)
• ocaml(Coq_checklib__CheckLibrary)
• ocaml(Coq_checklib__Check_stat)
• ocaml(Coq_checklib__Coqchk_main)
• ocaml(Coq_checklib__Mod_checking)
• ocaml(Coq_checklib__Safe_checking)
• ocaml(Coq_checklib__Validate)
• ocaml(Coq_checklib__Values)
• ocaml(Coq_config)
• ocaml(Coqargs)
• ocaml(Coqc)
• ocaml(Coqcargs)
• ocaml(Coqdeplib)
• ocaml(Coqdeplib__Args)
• ocaml(Coqdeplib__Common)
• ocaml(Coqdeplib__Dep_info)
• ocaml(Coqdeplib__Error)
• ocaml(Coqdeplib__File_util)
• ocaml(Coqdeplib__Fl)
• ocaml(Coqdeplib__Lexer)
• ocaml(Coqdeplib__Loadpath)
• ocaml(Coqdeplib__Makefile)
• ocaml(Coqdeplib__Rocqdep_main)
• ocaml(Coqinit)
• ocaml(Coqlib)
• ocaml(Coqloadpath)
• ocaml(Coqloop)
• ocaml(Coqrc)
• ocaml(Coqrun)
• ocaml(Coqtop)
• ocaml(CoqworkmgrApi)
• ocaml(DAst)
• ocaml(Dag)
• ocaml(DebugHook)
• ocaml(Debugger_support)
• ocaml(Declarations)
• ocaml(Declare)
• ocaml(DeclareInd)
• ocaml(DeclareScheme)
• ocaml(DeclareUniv)
• ocaml(Declaremods)
• ocaml(Declareops)
• ocaml(Decls)
• ocaml(Deprecation)
• ocaml(Derive_plugin)
• ocaml(Derive_plugin__Derive)
• ocaml(Derive_plugin__G_derive)
• ocaml(Detyping)
• ocaml(Diff2)
• ocaml(Discharge)
• ocaml(Dn)
• ocaml(Dumpglob)
• ocaml(Dyn)
• ocaml(EClause)
• ocaml(EConstr)
• ocaml(Eauto)
• ocaml(Egramml)
• ocaml(Egramrocq)
• ocaml(Elim)
• ocaml(Elimschemes)
• ocaml(Entries)
• ocaml(Envars)
• ocaml(Environ)
• ocaml(Eqdecide)
• ocaml(Eqschemes)
• ocaml(Equality)
• ocaml(Esubst)
• ocaml(Evaluable)
• ocaml(Evar)
• ocaml(Evar_kinds)
• ocaml(Evar_tactics)
• ocaml(Evarconv)
• ocaml(Evardefine)
• ocaml(Evarnames)
• ocaml(Evarsolve)
• ocaml(Evarutil)
• ocaml(Evd)
• ocaml(Exninfo)
• ocaml(Extend)
• ocaml(Extraction_plugin)
• ocaml(Extraction_plugin__Common)
• ocaml(Extraction_plugin__Extract_env)
• ocaml(Extraction_plugin__Extraction)
• ocaml(Extraction_plugin__G_extraction)
• ocaml(Extraction_plugin__Haskell)
• ocaml(Extraction_plugin__Json)
• ocaml(Extraction_plugin__Miniml)
• ocaml(Extraction_plugin__Mlutil)
• ocaml(Extraction_plugin__Modutil)
• ocaml(Extraction_plugin__Ocaml)
• ocaml(Extraction_plugin__Scheme)
• ocaml(Extraction_plugin__Table)
• ocaml(Feedback)
• ocaml(Find_subterm)
• ocaml(Firstorder_core_plugin)
• ocaml(Firstorder_core_plugin__Formula)
• ocaml(Firstorder_core_plugin__Ground)
• ocaml(Firstorder_core_plugin__Instances)
• ocaml(Firstorder_core_plugin__Rules)
• ocaml(Firstorder_core_plugin__Sequent)
• ocaml(Firstorder_core_plugin__Unify)
• ocaml(Firstorder_plugin)
• ocaml(Firstorder_plugin__G_ground)
• ocaml(FixTactics)
• ocaml(Flags)
• ocaml(Float64)
• ocaml(Float64_common)
• ocaml(Ftactic)
• ocaml(Funind_plugin)
• ocaml(Funind_plugin__Functional_principles_proofs)
• ocaml(Funind_plugin__Functional_principles_types)
• ocaml(Funind_plugin__G_indfun)
• ocaml(Funind_plugin__Gen_principle)
• ocaml(Funind_plugin__Glob_term_to_relation)
• ocaml(Funind_plugin__Glob_termops)
• ocaml(Funind_plugin__Indfun)
• ocaml(Funind_plugin__Indfun_common)
• ocaml(Funind_plugin__Invfun)
• ocaml(Funind_plugin__Recdef)
• ocaml(Future)
• ocaml(G_constr)
• ocaml(G_obligations)
• ocaml(G_prim)
• ocaml(G_proofs)
• ocaml(G_redexpr)
• ocaml(G_toplevel)
• ocaml(G_vernac)
• ocaml(Genarg)
• ocaml(Generalize)
• ocaml(Genintern)
• ocaml(Geninterp)
• ocaml(Genlambda)
• ocaml(Genprint)
• ocaml(Genredexpr)
• ocaml(Gensubst)
• ocaml(Gentactic)
• ocaml(GlobEnv)
• ocaml(Glob_ops)
• ocaml(Glob_term)
• ocaml(Global)
• ocaml(Globnames)
• ocaml(Goal_select)
• ocaml(Goptions)
• ocaml(Gramlib)
• ocaml(Gramlib__Gramext)
• ocaml(Gramlib__Grammar)
• ocaml(Gramlib__LStream)
• ocaml(Gramlib__Plexing)
• ocaml(Gramlib__Stream)
• ocaml(HConstr)
• ocaml(HMap)
• ocaml(Hashcons)
• ocaml(Hashset)
• ocaml(Heads)
• ocaml(Heap)
• ocaml(Himsg)
• ocaml(Hints)
• ocaml(Hipattern)
• ocaml(Hook)
• ocaml(IStream)
• ocaml(Impargs)
• ocaml(Implicit_quantifiers)
• ocaml(IndTyping)
• ocaml(Ind_tables)
• ocaml(Indrec)
• ocaml(Indschemes)
• ocaml(Indtypes)
• ocaml(Induction)
• ocaml(Inductive)
• ocaml(Inductiveops)
• ocaml(InferCumulativity)
• ocaml(Instr)
• ocaml(Int)
• ocaml(Inv)
• ocaml(Keys)
• ocaml(Lib)
• ocaml(LibBinding)
• ocaml(Libnames)
• ocaml(Libobject)
• ocaml(Library)
• ocaml(Library_info)
• ocaml(Load)
• ocaml(Loadpath)
• ocaml(Loc)
• ocaml(Locality)
• ocaml(Locus)
• ocaml(Locusops)
• ocaml(Logic)
• ocaml(Logic_monad)
• ocaml(Ltac2_ltac1_plugin)
• ocaml(Ltac2_ltac1_plugin__G_ltac2_ltac1)
• ocaml(Ltac2_ltac1_plugin__Tac2core_ltac1)
• ocaml(Ltac2_ltac1_plugin__Tac2quote_ltac1)
• ocaml(Ltac2_ltac1_plugin__Tac2stdlib_ltac1)
• ocaml(Ltac2_plugin)
• ocaml(Ltac2_plugin__G_ltac2)
• ocaml(Ltac2_plugin__Tac2bt)
• ocaml(Ltac2_plugin__Tac2core)
• ocaml(Ltac2_plugin__Tac2dyn)
• ocaml(Ltac2_plugin__Tac2entries)
• ocaml(Ltac2_plugin__Tac2env)
• ocaml(Ltac2_plugin__Tac2expr)
• ocaml(Ltac2_plugin__Tac2externals)
• ocaml(Ltac2_plugin__Tac2extffi)
• ocaml(Ltac2_plugin__Tac2extravals)
• ocaml(Ltac2_plugin__Tac2ffi)
• ocaml(Ltac2_plugin__Tac2intern)
• ocaml(Ltac2_plugin__Tac2interp)
• ocaml(Ltac2_plugin__Tac2match)
• ocaml(Ltac2_plugin__Tac2print)
• ocaml(Ltac2_plugin__Tac2qexpr)
• ocaml(Ltac2_plugin__Tac2quote)
• ocaml(Ltac2_plugin__Tac2stdlib)
• ocaml(Ltac2_plugin__Tac2tactics)
• ocaml(Ltac2_plugin__Tac2types)
• ocaml(Ltac2_plugin__Tac2typing_env)
• ocaml(Ltac2_plugin__Tac2val)
• ocaml(Ltac_plugin)
• ocaml(Ltac_plugin__ComRewrite)
• ocaml(Ltac_plugin__Coretactics)
• ocaml(Ltac_plugin__Extraargs)
• ocaml(Ltac_plugin__Extratactics)
• ocaml(Ltac_plugin__G_auto)
• ocaml(Ltac_plugin__G_class)
• ocaml(Ltac_plugin__G_eqdecide)
• ocaml(Ltac_plugin__G_ltac)
• ocaml(Ltac_plugin__G_rewrite)
• ocaml(Ltac_plugin__G_tactic)
• ocaml(Ltac_plugin__Internals)
• ocaml(Ltac_plugin__Leminv)
• ocaml(Ltac_plugin__Pltac)
• ocaml(Ltac_plugin__Pptactic)
• ocaml(Ltac_plugin__Profile_ltac_tactics)
• ocaml(Ltac_plugin__Tacarg)
• ocaml(Ltac_plugin__Taccoerce)
• ocaml(Ltac_plugin__Tacentries)
• ocaml(Ltac_plugin__Tacenv)
• ocaml(Ltac_plugin__Tacexpr)
• ocaml(Ltac_plugin__Tacintern)
• ocaml(Ltac_plugin__Tacinterp)
• ocaml(Ltac_plugin__Tacsubst)
• ocaml(Ltac_plugin__Tactic_debug)
• ocaml(Ltac_plugin__Tactic_matching)
• ocaml(Ltac_pretype)
• ocaml(Memprof_coq)
• ocaml(Memtrace_init)
• ocaml(Metasyntax)
• ocaml(Micromega_core_plugin)
• ocaml(Micromega_core_plugin__Micromega)
• ocaml(Micromega_core_plugin__Mutils)
• ocaml(Micromega_core_plugin__NumCompat)
• ocaml(Micromega_core_plugin__Sos)
• ocaml(Micromega_core_plugin__Sos_lib)
• ocaml(Micromega_core_plugin__Sos_types)
• ocaml(Micromega_plugin)
• ocaml(Micromega_plugin__Certificate)
• ocaml(Micromega_plugin__Coq_micromega)
• ocaml(Micromega_plugin__G_micromega)
• ocaml(Micromega_plugin__Itv)
• ocaml(Micromega_plugin__Linsolve)
• ocaml(Micromega_plugin__Persistent_cache)
• ocaml(Micromega_plugin__Polynomial)
• ocaml(Micromega_plugin__Simplex)
• ocaml(Micromega_plugin__Vect)
• ocaml(Miscprint)
• ocaml(Mltop)
• ocaml(Mod_declarations)
• ocaml(Mod_subst)
• ocaml(Mod_typing)
• ocaml(Modintern)
• ocaml(Modops)
• ocaml(Monad)
• ocaml(Mutex_aux)
• ocaml(Namegen)
• ocaml(Nameops)
• ocaml(Names)
• ocaml(Nametab)
• ocaml(Nativecode)
• ocaml(Nativeconv)
• ocaml(Nativelambda)
• ocaml(Nativelib)
• ocaml(Nativelibrary)
• ocaml(Nativenorm)
• ocaml(Nativevalues)
• ocaml(NeList)
• ocaml(NewProfile)
• ocaml(Notation)
• ocaml(Notation_gram)
• ocaml(Notation_ops)
• ocaml(Notation_term)
• ocaml(Notationextern)
• ocaml(Notgram_ops)
• ocaml(Nsatz_core_plugin)
• ocaml(Nsatz_core_plugin__Ideal)
• ocaml(Nsatz_core_plugin__Nsatz)
• ocaml(Nsatz_core_plugin__Polynom)
• ocaml(Nsatz_core_plugin__Utile)
• ocaml(Nsatz_plugin)
• ocaml(Nsatz_plugin__G_nsatz)
• ocaml(NumTok)
• ocaml(Number_string_notation_plugin)
• ocaml(Number_string_notation_plugin__G_number_string)
• ocaml(Number_string_notation_plugin__Number_string)
• ocaml(ObjFile)
• ocaml(Opaqueproof)
• ocaml(Opaques)
• ocaml(Option)
• ocaml(OrderedType)
• ocaml(PConstraints)
• ocaml(Parray)
• ocaml(Partac)
• ocaml(Partial_subst)
• ocaml(Pattern)
• ocaml(Patternops)
• ocaml(Pcoq)
• ocaml(Perf)
• ocaml(PolyFlags)
• ocaml(PolyMap)
• ocaml(Pp)
• ocaml(Pp_diff)
• ocaml(Ppconstr)
• ocaml(Ppextend)
• ocaml(Ppred)
• ocaml(Pputils)
• ocaml(Ppvernac)
• ocaml(Predicate)
• ocaml(Prettyp)
• ocaml(Pretype_errors)
• ocaml(Pretyping)
• ocaml(PrimNotations)
• ocaml(Primred)
• ocaml(Printer)
• ocaml(PrintingFlags)
• ocaml(Printmod)
• ocaml(Procq)
• ocaml(Profile_tactic)
• ocaml(Program)
• ocaml(Proof)
• ocaml(ProofBlockDelimiter)
• ocaml(Proof_bullet)
• ocaml(Proof_diffs)
• ocaml(Proof_using)
• ocaml(Proofview)
• ocaml(Proofview_monad)
• ocaml(Pstring)
• ocaml(Pvernac)
• ocaml(QGraph)
• ocaml(Quickfix)
• ocaml(Range)
• ocaml(RecLemmas)
• ocaml(Record)
• ocaml(RedFlags)
• ocaml(Redexpr)
• ocaml(Redops)
• ocaml(Reduction)
• ocaml(Reductionops)
• ocaml(Refine)
• ocaml(Relevanceops)
• ocaml(Reserve)
• ocaml(RetrieveObl)
• ocaml(Retroknowledge)
• ocaml(Retyping)
• ocaml(Rewrite)
• ocaml(Ring_plugin)
• ocaml(Ring_plugin__G_ring)
• ocaml(Ring_plugin__Ring)
• ocaml(Ring_plugin__Ring_ast)
• ocaml(Rocqlib)
• ocaml(Rocqshim)
• ocaml(Rtauto_plugin)
• ocaml(Rtauto_plugin__G_rtauto)
• ocaml(Rtauto_plugin__Proof_search)
• ocaml(Rtauto_plugin__Refl_tauto)
• ocaml(Rtree)
• ocaml(SList)
• ocaml(Safe_typing)
• ocaml(Search)
• ocaml(Section)
• ocaml(Segmenttree)
• ocaml(Smartlocate)
• ocaml(Sorts)
• ocaml(Spawn)
• ocaml(Spawned)
• ocaml(Ssreflect_plugin)
• ocaml(Ssreflect_plugin__Ssrast)
• ocaml(Ssreflect_plugin__Ssrbwd)
• ocaml(Ssreflect_plugin__Ssrcommon)
• ocaml(Ssreflect_plugin__Ssrelim)
• ocaml(Ssreflect_plugin__Ssrequality)
• ocaml(Ssreflect_plugin__Ssrfwd)
• ocaml(Ssreflect_plugin__Ssripats)
• ocaml(Ssreflect_plugin__Ssrparser)
• ocaml(Ssreflect_plugin__Ssrprinters)
• ocaml(Ssreflect_plugin__Ssrtacs)
• ocaml(Ssreflect_plugin__Ssrtacticals)
• ocaml(Ssreflect_plugin__Ssrvernac)
• ocaml(Ssreflect_plugin__Ssrview)
• ocaml(Ssrmatching_plugin)
• ocaml(Ssrmatching_plugin__G_ssrmatching)
• ocaml(Ssrmatching_plugin__Ssrmatching)
• ocaml(Stateid)
• ocaml(Stdarg)
• ocaml(Stm)
• ocaml(Stmargs)
• ocaml(Store)
• ocaml(Structures)
• ocaml(Subproof)
• ocaml(Subtyping)
• ocaml(Summary)
• ocaml(Synterp)
• ocaml(System)
• ocaml(TQueue)
• ocaml(Tacmach)
• ocaml(Tacred)
• ocaml(TacticErrors)
• ocaml(Tactic_option)
• ocaml(Tacticals)
• ocaml(Tactics)
• ocaml(Tactypes)
• ocaml(Tauto_plugin)
• ocaml(Tauto_plugin__Tauto)
• ocaml(TemplateArity)
• ocaml(Term)
• ocaml(Terminal)
• ocaml(Termops)
• ocaml(Tok)
• ocaml(Top_printers)
• ocaml(Topfmt)
• ocaml(TransparentState)
• ocaml(Trie)
• ocaml(Tuto0_plugin)
• ocaml(Tuto0_plugin__G_tuto0)
• ocaml(Tuto0_plugin__Tuto0_main)
• ocaml(Tuto1_plugin)
• ocaml(Tuto1_plugin__G_tuto1)
• ocaml(Tuto1_plugin__Inspector)
• ocaml(Tuto1_plugin__Simple_check)
• ocaml(Tuto1_plugin__Simple_declare)
• ocaml(Tuto1_plugin__Simple_print)
• ocaml(Tuto2_plugin)
• ocaml(Tuto2_plugin__Counter)
• ocaml(Tuto2_plugin__Custom)
• ocaml(Tuto2_plugin__G_tuto2)
• ocaml(Tuto2_plugin__Persistent_counter)
• ocaml(Tuto3_plugin)
• ocaml(Tuto3_plugin__Construction_game)
• ocaml(Tuto3_plugin__G_tuto3)
• ocaml(Tuto3_plugin__Tuto_tactic)
• ocaml(Tuto4_plugin)
• ocaml(Tuto4_plugin__Myexternals)
• ocaml(Type_errors)
• ocaml(Typeclasses)
• ocaml(Typeclasses_errors)
• ocaml(Typeops)
• ocaml(Typing)
• ocaml(UGraph)
• ocaml(UState)
• ocaml(UVars)
• ocaml(Uint63)
• ocaml(Unicode)
• ocaml(Unicodetable)
• ocaml(Unification)
• ocaml(Unionfind)
• ocaml(Univ)
• ocaml(UnivFlex)
• ocaml(UnivGen)
• ocaml(UnivMinim)
• ocaml(UnivNames)
• ocaml(UnivProblem)
• ocaml(UnivSubst)
• ocaml(UserWarn)
• ocaml(Util)
• ocaml(Values)
• ocaml(Vars)
• ocaml(Vconv)
• ocaml(Vcs)
• ocaml(Vernac)
• ocaml(VernacControl)
• ocaml(Vernac_classifier)
• ocaml(Vernacentries)
• ocaml(Vernacexpr)
• ocaml(Vernacextend)
• ocaml(Vernacinterp)
• ocaml(Vernacoptions)
• ocaml(Vernacprop)
• ocaml(Vernacstate)
• ocaml(Vernactypes)
• ocaml(Vm)
• ocaml(Vm_printers)
• ocaml(Vmbytecodes)
• ocaml(Vmbytegen)
• ocaml(Vmemitcodes)
• ocaml(Vmerrors)
• ocaml(Vmlambda)
• ocaml(Vmlibrary)
• ocaml(Vmopcodes)
• ocaml(Vmsymtable)
• ocaml(Vmvalues)
• ocaml(Vnorm)
• ocaml(WorkerLoop)
• ocaml(WorkerPool)
• ocaml(WriteOnceArray)
• ocaml(Xml_datatype)
• ocaml(Zify_plugin)
• ocaml(Zify_plugin__G_zify)
• ocaml(Zify_plugin__Zify)
• rocq-runtime(ppc-64)
• tex(coqdoc.sty)

Requires

• /usr/bin/ocamlrun
• /usr/bin/python3
• glibc >= 2.43.9000-11
• ld64.so.2()(64bit)
• ld64.so.2(GLIBC_2.22)(64bit)
• libc.so.6()(64bit)
• libc.so.6(GLIBC_2.17)(64bit)
• libc.so.6(GLIBC_2.25)(64bit)
• libc.so.6(GLIBC_2.28)(64bit)
• libc.so.6(GLIBC_2.32)(64bit)
• libc.so.6(GLIBC_2.33)(64bit)
• libc.so.6(GLIBC_2.34)(64bit)
• libc.so.6(GLIBC_2.38)(64bit)
• libc.so.6(GLIBC_2.42)(64bit)
• libc.so.6(GLIBC_ABI_DT_RELR)(64bit)
• libgmp.so.10()(64bit)
• libm.so.6()(64bit)
• libm.so.6(GLIBC_2.17)(64bit)
• libm.so.6(GLIBC_2.29)(64bit)
• libm.so.6(GLIBC_2.35)(64bit)
• libm.so.6(GLIBC_2.38)(64bit)
• libm.so.6(GLIBC_2.44)(64bit)
• ocaml(Abbreviation) = 3f5bba4028ae5d50af71a3755b918176
• ocaml(Abstract) = a3e1da23f7e920eff602afa657cc8cf7
• ocaml(AcyclicGraph) = a0928ab85aa9d3f76c78f32d885ccf4b
• ocaml(AllScheme) = 9169880a91d2a22e406be5a1975b3036
• ocaml(Arguments_renaming) = f3f26f4bac7adb7ab57131103d1dadf8
• ocaml(Assumptions) = fadcea1e6e1b2272a5305aa9406e3af6
• ocaml(Asttypes) = e507ef6e691c55af686b09bd398e52fe
• ocaml(AsyncTaskQueue) = c2c76e34bd65fad7f95570f1f5d3810d
• ocaml(Attributes) = ee94f0e950a4045506fadfd8f8a692ed
• ocaml(Auto) = 4ab240c90c4eea4cdf2f14efa7f6d886
• ocaml(Auto_ind_decl) = 2c6fb53af45575d44e58925cf3cc3f1b
• ocaml(Autorewrite) = edaa5d598a18b966dadd7fbadacf1543
• ocaml(Aux_file) = 80391d3302cfd4395c115333517cd26e
• ocaml(Big_int_Z) = d6cb9e1c54060ad10e28f7ba86ae266a
• ocaml(Boot) = c10d1826ec03550bc542cef705e8a113
• ocaml(Boot__Env) = 6761f5c82d57f92b184c43064da1a433
• ocaml(Boot__Path) = db34ea431173f9ae4c5adf48124456ea
• ocaml(Boot__Usage) = 38a803d96d64d1260891320e63e0a08b
• ocaml(Boot__Util) = 7ba9a906ee0085778ce0b96e0afcfde3
• ocaml(Btauto_plugin) = 021f47edaa1c3dcd96029f3b21dd4a96
• ocaml(Btauto_plugin__Refl_btauto) = d579f77166fe9fd01d50a2e31756acf9
• ocaml(Btermdn) = 488b70b914ee4bb6ee316ccbbcf74e2b
• ocaml(Build_path_prefix_map) = e0f5cdd3ea76275f8c562bce411ee08b
• ocaml(CArray) = a2e455be7013ec529edc7deeb9c88dcd
• ocaml(CAst) = 23961d59b930d5aa36baa14c1928b394
• ocaml(CClosure) = ad77f6a8affd525d51346515f6cfef66
• ocaml(CDebug) = 7f2e1a015766edd1310ed03bf997b5bf
• ocaml(CEphemeron) = 7cae4867455538660558bdff12463859
• ocaml(CErrors) = fd6fe9d08d9caf8ea4d446ec01e9281a
• ocaml(CLexer) = fb825ee2f56f1eea8e0db95c92534d73
• ocaml(CList) = 9a2830c6a7f1e5138c25f4567f0e7335
• ocaml(CMap) = d8df1ab91a0cf1bc2bb100f53ca23222
• ocaml(CObj) = 2adb6c04a1dd1ddff801b115e6e3dfd6
• ocaml(CPrimitives) = 6cdb488917c5d051bf02f9e386b819ed
• ocaml(CSet) = c99ec5a860a1db040e3cb46a4ef41cff
• ocaml(CSig) = 8cb23fa269471e19f2cc9161ba3980d0
• ocaml(CString) = b8a8bb70f9e4d08f167510409e9a6053
• ocaml(CThread) = c04f6295803e585cd503bd0078828dee
• ocaml(CUnix) = f6850de84f62fe0043b8f44ae8b780c8
• ocaml(CWarnings) = 3d3d432d806232d106cde8a3e8935ad4
• ocaml(CamlinternalFormat) = 70bcbb90ec668384a2248434bb2eb1ab
• ocaml(CamlinternalFormatBasics) = bb23651112c1e05c61498d902472830d
• ocaml(CamlinternalLazy) = 321f83e197d23ef3129f66a139b9829f
• ocaml(CamlinternalMod) = 091e0f55942111b1b8c378809123a052
• ocaml(Canonical) = 20331db6d9d64a0d0729df9b459f4a9c
• ocaml(Cases) = 003e751b937c5cc21c94ee0d5cb8a138
• ocaml(Cbn) = 236066a400da4d814f2119c56735ef7a
• ocaml(Cbv) = 2003e5adc2306e96649a952111a2b6a3
• ocaml(Cc_core_plugin) = 7221186ffe2b1d4feeb3b619e5518b5b
• ocaml(Cc_core_plugin__Ccalgo) = 3021d5584f1c9e3c569cc9e0a1ff7724
• ocaml(Cc_core_plugin__Ccprojectability) = b76b4bdc530cced9dfa7229b84162d9e
• ocaml(Cc_core_plugin__Ccproof) = c48036745b83ed94558daea2266c7b0f
• ocaml(Cc_core_plugin__Cctac) = ee7088f181f2e6255466b0e5773c3d8f
• ocaml(Cc_plugin) = ace7197075e417f45053eabc4ecb5148
• ocaml(Ccompile) = 848d594b5b3157579a921350c6c6c085
• ocaml(Class_tactics) = ddac1e3b49536853cfaf7a2360457937
• ocaml(Classes) = 449e6958e278090082e504c288e99a58
• ocaml(Clenv) = 49801c3265e5ca44465712bce0a67291
• ocaml(Clflags) = 1e5696f0c01b2a0894699729b9bf930a
• ocaml(Cmi_format) = af4e87c82d2bb018b25d798368662790
• ocaml(Coercion) = cf3bb56d124f15d75dd2a785fe5e81da
• ocaml(Coercionops) = 1bf96a451fdcf2424f92a69f4082338a
• ocaml(Colors) = f64d1bac25e83f529dca98fcd2183c24
• ocaml(ComArguments) = d81497434355d29924bee4c1b257f6cb
• ocaml(ComAssumption) = b6126e6fc5cbfb9f7f4768b0df409af8
• ocaml(ComCoercion) = adcc1342065f09866c51b0b72e5acbac
• ocaml(ComDefinition) = 067563eeb5f58689d50e2f3f1c19ec5a
• ocaml(ComExtraDeps) = 79893939cc5bdaa4ca73b2c5453efd0f
• ocaml(ComFixpoint) = 1034e87dc914412a9246c9bc4c6a0bf1
• ocaml(ComHints) = 4c3c7deb5b6932ec08bd43cfdd274ed1
• ocaml(ComInductive) = d481114e597b0ee5096138907d407ca3
• ocaml(ComPrimitive) = 135718eb5f3dc08f8c1a8e3c20a6a835
• ocaml(ComRewriteRule) = 9ad871aa2ff0e59f2f1ad6362d5e216e
• ocaml(ComSearch) = 2beb882c408b222cab8a6d09dbf6a25b
• ocaml(ComTactic) = 6b3a8b2a9b6534500719669552759b92
• ocaml(Combinators) = aff8fb08e995265bb73902b8d2ecf0a2
• ocaml(Common_compile) = 8b9f1ab2504e41a1a73402d8199ec792
• ocaml(Compenv) = c5b2a25f63b81e35600f80ebdc868b4b
• ocaml(Constant_typing) = 232dfa45389b1a03fd80579aa06999cc
• ocaml(Constr) = fb261580b2c56e92b79230e91984b99e
• ocaml(Constr_matching) = ccd482778e57cac8e5068a728fba470b
• ocaml(Constrexpr) = fb00393fe0cfeeb27d5e33468e787bdd
• ocaml(Constrexpr_ops) = deb3af588fafaa786558b8a4b25a28a9
• ocaml(Constrextern) = 831877d48444b8b26432396cd48e7e06
• ocaml(Constrintern) = 6587e6cdecff8821f9e2719a01bd8340
• ocaml(Context) = b7bf9c2dd9f01e83956292783ef0d7dc
• ocaml(Contradiction) = a61fb5a04b1eac03e254cda669e4b11a
• ocaml(Control) = acbb11261e0a40401d541b02d202d7b6
• ocaml(Conv_oracle) = ca9287d023dd57759fc769dc6d98e187
• ocaml(Conversion) = 3a7b3cb133deea09a215118994a3a709
• ocaml(Cooking) = ab1e9c5cf41a861b8d8e39a08760f872
• ocaml(CoqProject_file) = 88f02f03103b88830d4ada291869936a
• ocaml(Coq_checklib) = 2baf09a1c451962aa0d821a3fdd11db5
• ocaml(Coq_checklib__Analyze) = 83361539cce55e3551b4cf869801cbcf
• ocaml(Coq_checklib__CheckFlags) = 9f99ae3ec66544f4f16e052d78a78061
• ocaml(Coq_checklib__CheckInductive) = b3b411480e40c8b42cd77a10e87bd53b
• ocaml(Coq_checklib__CheckLibrary) = 834137950de034eb991b536d5a13c2d6
• ocaml(Coq_checklib__Check_stat) = a784bfd46ad20190e8509f511b015cd9
• ocaml(Coq_checklib__Mod_checking) = f607749868ea5fc1e286e67c28617954
• ocaml(Coq_checklib__Safe_checking) = e86df2d5fc6e8dfe0bc13277fd4f6369
• ocaml(Coq_checklib__Validate) = ad1a44e6c3fd2bd40f5ee2efa483b7c8
• ocaml(Coq_checklib__Values) = 0e0d1b05633b37f4cda113582947eb1a
• ocaml(Coq_config) = 4e8d62ba5366a6130182d87b6d493cae
• ocaml(Coqargs) = c538ffb8aeafe4fa8275c154af0d1638
• ocaml(Coqcargs) = 4d1c534dfb4113cbe372218a3c1c386b
• ocaml(Coqdeplib) = 9691a482b51456c82d6ef9fd3de101f6
• ocaml(Coqdeplib__Args) = 87a6f6360c4b113744b22e70269b440f
• ocaml(Coqdeplib__Common) = 3b3fcbc98940c5dfa1ff45e7f1c19a70
• ocaml(Coqdeplib__Dep_info) = 37179962dcd3a08a8d1f8e09e3146442
• ocaml(Coqdeplib__Error) = 3199b2f9af50547faa9a2461af74b609
• ocaml(Coqdeplib__File_util) = e9dac49d7c06afe6ea1525967bf2c283
• ocaml(Coqdeplib__Fl) = 2a6a849b34ab36eb546766001bb63e20
• ocaml(Coqdeplib__Lexer) = 82c4fea37565fce0467a43e8e7de58a2
• ocaml(Coqdeplib__Loadpath) = 3315feaa5dd4659542a5827e742f3c15
• ocaml(Coqdeplib__Makefile) = a654c740c362576d61ce0b4b924453eb
• ocaml(Coqinit) = 4ddaf590ad1be61a8de1433b680106cf
• ocaml(Coqloadpath) = cfdcf87c77a8825a6eed649a39337559
• ocaml(Coqloop) = 7d1ba6f0887b4f9e0f56e40eb6f94221
• ocaml(Coqrc) = 45ccec5688f862bdaed8c239b882e172
• ocaml(Coqtop) = 2906ce1694d974148389c20f27a55c57
• ocaml(CoqworkmgrApi) = bf9291ab65d50704790e0ce2f6f3b962
• ocaml(DAst) = dfe8298509e157009558d4e8012a58d7
• ocaml(Dag) = 7e85dc3bd26aa26d7f1582df587d5618
• ocaml(Data_types) = 9f178cf8e1e58dacbc1ab559802bb5d5
• ocaml(DebugHook) = 4a0b419408abdbaad3466f51bd079051
• ocaml(Declarations) = 030ba3d93147be2f26b3e9ab56f774ac
• ocaml(Declare) = 75949e6a91a3375dd3feac2aad4ca540
• ocaml(DeclareInd) = c85c86be5818a9726de4567134d5abf0
• ocaml(DeclareScheme) = f98a7f3cabde4e7d32dc7d745fe5a575
• ocaml(DeclareUniv) = 18e61a8748026a5a5d98bfbbf4acb256
• ocaml(Declaremods) = d700e258fb2196fe2f6231a5999bdf53
• ocaml(Declareops) = e39872ed9c52eb1e93c2b5577033c708
• ocaml(Decls) = 54fed2f8d8694a8ed3706c9743199440
• ocaml(Deprecation) = df915a2364b805360c5b333eff08e454
• ocaml(Derive_plugin) = cfa1f7052a4b7c1f11cf5d3c30e00cf2
• ocaml(Derive_plugin__Derive) = 570950f79300176e513f1464531b91c6
• ocaml(Detyping) = 51a09f670b6d95c1f34da720e92885e2
• ocaml(Diff2) = 8940429ed83ad199f81a27ff5df3fadc
• ocaml(Discharge) = cf4de47443c63686ccac0d6bc54d1882
• ocaml(Dn) = f8f3a88ab1ade13c85ae0378e1148817
• ocaml(Dumpglob) = 375ece1d72754a626848fe883fc6a68c
• ocaml(Dyn) = f0cdf5756549bfb2f13af24fa17b15ff
• ocaml(Dynlink) = 08e1461841151b2dfdeeb2b217719fea
• ocaml(EClause) = da9b009d69a78147a46237c21313ec96
• ocaml(EConstr) = 8045370f4188bbd9ccb9faf948edaeba
• ocaml(Eauto) = 7377475c068a0dffb05801a31b4c943a
• ocaml(Egramml) = 8fec6cb19a865f6006ffc455256b5f3c
• ocaml(Egramrocq) = 97e9b3009ca22f96f6a5b721e1b35ed6
• ocaml(Elim) = 330c4f2ca3075fbaddde7b57f6ac1373
• ocaml(Elimschemes) = e0621e338b8f527f15667aaa5c644c24
• ocaml(Entries) = 2ff75b285b4a2a968be0145f18804393
• ocaml(Env) = 0cdf66ea216efe371c58a7976afe2075
• ocaml(Envars) = fc8d9acafb03dbdf0cf9bd347b88c21f
• ocaml(Environ) = aede06b1411b49706b7510e2e4434f71
• ocaml(Eqdecide) = f257a0bda507cd4a82618a8bec0c45fc
• ocaml(Eqschemes) = ff6a4ff1ecfd532428bcdd797cd1716e
• ocaml(Equality) = d8621a5ddcac13d84a5c2ae7ff3873f3
• ocaml(Esubst) = 31516adf5d49c65ff5034d2fb4a17e23
• ocaml(Evaluable) = c23c968b6d8ec423fb5972ca9324f499
• ocaml(Evar) = 5c12d3020e6c58f5eec50fd86ffb3278
• ocaml(Evar_kinds) = 14944ba8a5fafb11f4045137ed5ad8de
• ocaml(Evar_tactics) = b36f5edbcd76f93475009d6691031047
• ocaml(Evarconv) = d135cecb107fbd2f29cc69f549912499
• ocaml(Evardefine) = 6e3eaff04cdaa76ddfcdb5d33cca727b
• ocaml(Evarnames) = df97c3e2f620dfa10970988b72d37276
• ocaml(Evarsolve) = b27ce4e0d7e6f908a79cef283c27810a
• ocaml(Evarutil) = 69bde9e70acfd360778497e8dcd20d85
• ocaml(Evd) = 9102614a89005ace383e19f7d0554bf5
• ocaml(Exninfo) = 95e7f938070548b5b5d750588295e6db
• ocaml(Extend) = 400158e1a07efc1d779de794d8a9dc32
• ocaml(Extraction_plugin) = 45385a433336b20d3b91e013e59f2671
• ocaml(Extraction_plugin__Common) = 5ac585bba9fc6c5ffbddfd5d03f4de41
• ocaml(Extraction_plugin__Extract_env) = a64fad1bedb49694a2741af6a26a10d5
• ocaml(Extraction_plugin__Extraction) = 0d937a6e53de96540f11503ce18e38fe
• ocaml(Extraction_plugin__Haskell) = 0192cb45f29bf117e18ade5632618c61
• ocaml(Extraction_plugin__Json) = cedf77d385a759ce2464a4edb9782ccd
• ocaml(Extraction_plugin__Miniml) = 204b49923b09139582d3cc4469642e20
• ocaml(Extraction_plugin__Mlutil) = a2499478a817fb73f8e5e2fc48e1a555
• ocaml(Extraction_plugin__Modutil) = 74a116de51e13b3705c381d237d79e27
• ocaml(Extraction_plugin__Ocaml) = f8151831c224316363f5b14577b730f9
• ocaml(Extraction_plugin__Scheme) = 649450122d90fc4833cb9e2726b2b813
• ocaml(Extraction_plugin__Table) = 6518fed33334e5af1a3f688380e1da5d
• ocaml(Feedback) = 747950a142a2a3b06505c9203be8ca69
• ocaml(Find_subterm) = 4f8f3b56b58928afea0bc4ecb8c9ca6f
• ocaml(Findlib) = a5fc3db70ae71cda44eb0da93e094eb2
• ocaml(Firstorder_core_plugin) = 117b378e702191a4f2b1921366b5a21f
• ocaml(Firstorder_core_plugin__Formula) = 701a99cf619bf6baaaf31bc7d7cd74a8
• ocaml(Firstorder_core_plugin__Ground) = f019e7b8fd496b34f2391acfe4645bbe
• ocaml(Firstorder_core_plugin__Instances) = b779170986767772632fa44463d08e21
• ocaml(Firstorder_core_plugin__Rules) = 1bf0c681e0ce4b001cc253fdc4771829
• ocaml(Firstorder_core_plugin__Sequent) = 8e5dd2802b830fce993408f0a2ab4c80
• ocaml(Firstorder_core_plugin__Unify) = e75f31f9ac62692b7fc2a203c5cbc751
• ocaml(Firstorder_plugin) = de43944fb21b3ca4a0fdc2c59c4173d1
• ocaml(FixTactics) = 9aea761547091d21611743d3e57bff4a
• ocaml(Fl_metascanner) = f2833d59fc6fb9013774ad16022f6e1f
• ocaml(Fl_metatoken) = c52aa6baf9d82887fc926a04bacae69b
• ocaml(Fl_package_base) = b49943184674c704462363ed948c27f6
• ocaml(Flags) = 19916178d870280fe9f95ab2ef02f47d
• ocaml(Float64) = e3af59c461d447770a9513d585363662
• ocaml(Float64_common) = 8bb3514a86d9aa53eca574fb5a08dba4
• ocaml(Format_doc) = e9bc76d69e0a38952eeb83c757a95d18
• ocaml(Ftactic) = 3be3bbb1998ac5357e0ceff1ecb3e794
• ocaml(Funind_plugin) = 478d36ea9a949ae615ecf6f234e67878
• ocaml(Funind_plugin__Functional_principles_proofs) = 697ecea0899f8b52f5b70e0b75699b1a
• ocaml(Funind_plugin__Functional_principles_types) = ffd3bac7f21282d0c9a45d3cf0f5c5c7
• ocaml(Funind_plugin__Gen_principle) = 461d6f2be1cec54f74f4221c5a489864
• ocaml(Funind_plugin__Glob_term_to_relation) = 393fcf35eeda3e14faf8d4fde8cd2b12
• ocaml(Funind_plugin__Glob_termops) = b292d4095edc2978528b1d67c8d3b08c
• ocaml(Funind_plugin__Indfun) = 63b3f684af3c022289946cc08b5dfbcb
• ocaml(Funind_plugin__Indfun_common) = df8bf88ef6f3f94d9015b1b94a74c282
• ocaml(Funind_plugin__Invfun) = 696caca99970a8454aa207657f4145e1
• ocaml(Funind_plugin__Recdef) = 38138e4cc99aff354a39f77542f96eab
• ocaml(Future) = 0834bf495a97d13fe3d43454740f6994
• ocaml(G_constr) = 6e54875421ab902186e9f47471a31da8
• ocaml(G_proofs) = 6e327ea88f59f6f5a9016b5f2aa3c58d
• ocaml(G_redexpr) = bcedd738705776f5451470c348e71b4a
• ocaml(G_toplevel) = 40cc12f25ac856e7e86d707d84ccf35d
• ocaml(G_vernac) = f55506af214255c01090a55da8446ccc
• ocaml(Genarg) = b7d1b46b3555c6085534dc23bdd45ce2
• ocaml(Generalize) = 54ba689217bf7b77036e9228439b3e39
• ocaml(Genintern) = 11b6ab7464837ebd4e6d8b92fa589577
• ocaml(Geninterp) = 83fd29396e95aa620ef80e09cd7931dc
• ocaml(Genlambda) = 754cd6e7d91a4a53fdbdfdca25b3ddca
• ocaml(Genprint) = 9a9fb8ecbec26bf0c7d4212c77f9c263
• ocaml(Genredexpr) = 5d175f6163784bbfeddf6c186f6ace40
• ocaml(Gensubst) = d8ce3f530105e98c0927957d0db81613
• ocaml(Gentactic) = af12900fcf8c3f1a009c4d91b1406c4c
• ocaml(GlobEnv) = 3f612e3cc8565501734ac24751f3d9d5
• ocaml(Glob_ops) = 950c9ee758c74347607398aafe9a4954
• ocaml(Glob_term) = 96a14cf41e84f3fccf0f2ddc3786420d
• ocaml(Global) = 88d35a7c0bf9dbcf40f1afca4d221a8b
• ocaml(Globnames) = 052f59172207e5158a79c1e79e4d22a0
• ocaml(Goal_select) = 2814ca816c54330bf63114b93e467e39
• ocaml(Goptions) = ffdb7184b0ab5016877800c33ccd1a19
• ocaml(Gramlib) = ae39fd0bb86764a48d691d550ddeb9d2
• ocaml(Gramlib__Gramext) = e49c510afe5490ea4e64d84dc46dd6a9
• ocaml(Gramlib__Grammar) = f4df4fab3c9493ad0e0d895296764756
• ocaml(Gramlib__LStream) = e1885b119f7b1a59c48b239662cf0379
• ocaml(Gramlib__Plexing) = 4610fa3e2850b51afbc1eb3052b9141e
• ocaml(Gramlib__Stream) = 4764be9973f4964bc0d6417ffa24b77b
• ocaml(HConstr) = cb7dbcb43bf81b1bf81eb6f09d41ef17
• ocaml(HMap) = 809701de4a3651c0788d2967c526cb88
• ocaml(Hashcons) = d9da5b4a5d48cabeddb2878692bf1fce
• ocaml(Hashset) = f2a941d55c9ded6be6c8f9026ec7a921
• ocaml(Heads) = 1df5c26e88a193fd6c2806be0dc1ff87
• ocaml(Heap) = 4f083d427cb30e39d3d786a1cf292eaa
• ocaml(Himsg) = 48a5e88ee17b95264eb62407e516af57
• ocaml(Hints) = f06c15c1a5a46b5d254a17ccfd3d7438
• ocaml(Hipattern) = bd9f6100358d2e713c3863e79e9f1eed
• ocaml(Hook) = f86461414dc1ef72fcb0b45bed7f95ce
• ocaml(IStream) = 2da469b3f4ce192ed5a5dc8fab75ced2
• ocaml(Ident) = 61cbd919c8f6ef60ced7ecbe7fb6faf5
• ocaml(Identifiable) = 8621bc2814d3f193b9cab59619693489
• ocaml(Impargs) = f83f4a1f007162bb4f50c56e3307e6a7
• ocaml(Implicit_quantifiers) = 5bc9c2fe825fcc0b0e8cb198a4ec1557
• ocaml(IndTyping) = b821f35aa3cbf1adc7f7b867851f6874
• ocaml(Ind_tables) = 37faf8fc4e3a244d008d9d60f6887166
• ocaml(Indrec) = e45dec78cac1cbe4f91dc8bde9f21232
• ocaml(Indschemes) = 756a6b42d7aef7be5cdad8857a668698
• ocaml(Indtypes) = e7cdbfa0b056eb80062469ca4cec9724
• ocaml(Induction) = a8168844f75a9795f491826ae8e24b28
• ocaml(Inductive) = 5d4e95b3b303626537151353b4f25223
• ocaml(Inductiveops) = edac5475f0b0c5fb1fa466341acf092a
• ocaml(InferCumulativity) = 9e8a4924786fb6da36a5719856040a7e
• ocaml(Instr) = 82b17b769bc0349c36beeb461e0ca02d
• ocaml(Int) = 88f311a03d57180dbb31c55fea3304a2
• ocaml(Inv) = 14d5ba850261eeecb22f21b3173daed3
• ocaml(Keys) = 21d9ba33957e4f4daf6560d1d453ba4d
• ocaml(Lib) = 34637da1a9ad40f2e974b43ae42e7ff5
• ocaml(LibBinding) = b9d058eaef18b0e9ba8b8ed8c76d1ec0
• ocaml(Libnames) = e5b66e348bb5442b01e64137ae7f2d2a
• ocaml(Libobject) = bb05130ad670044a529ebb92d8c348fa
• ocaml(Library) = eca31ae4c1829ebd9c718eaf00807c14
• ocaml(Library_info) = bb67c359dd87a433666bd624be33a6e2
• ocaml(Load) = 58b0a34d7edbf60c52429b2ec0b1fd53
• ocaml(Load_path) = 311833dc50b7f0117c7580122e8b521b
• ocaml(Loadpath) = f6874b51089cc3498e6fa1c0624d55f9
• ocaml(Loc) = 11ac099f9c19f0c65bf3b47a73ef6e27
• ocaml(Locality) = 0b0715af09ba64e4cca27ca908696be5
• ocaml(Location) = 1f3b4a14027aa1c3d06755358fe40ab9
• ocaml(Locus) = 448271cd0d030c79416c91609509bb50
• ocaml(Locusops) = 0eead919b92fed8916c8b142c5981c9f
• ocaml(Logic) = ad092736ccbcc60c2cd9c84fd03f6ac7
• ocaml(Logic_monad) = 49c62e4f37eda148c3cd7a98e103b78e
• ocaml(Longident) = 4fec6bb94016657f43f91bd096f27b38
• ocaml(Ltac2_ltac1_plugin) = f36ee64104bf7571ca1347ac2369081a
• ocaml(Ltac2_ltac1_plugin__Tac2quote_ltac1) = d8e6060e40079bad6f05d51b3aa03acb
• ocaml(Ltac2_plugin) = 7daee34a649601c4e5fbec1b44a1e83e
• ocaml(Ltac2_plugin__G_ltac2) = 113e3ee6ff9525ba7aaaed7029ec6c1d
• ocaml(Ltac2_plugin__Tac2bt) = 738260e4509cf0ebbbb55e0b5995cce8
• ocaml(Ltac2_plugin__Tac2core) = 52dcb4a52cd72b0d173c6c61b1739dc7
• ocaml(Ltac2_plugin__Tac2dyn) = 2193dfcaea52b177f52ad4c6000125b7
• ocaml(Ltac2_plugin__Tac2entries) = 17a8455d4a003fe110d9cfc9bea198c5
• ocaml(Ltac2_plugin__Tac2env) = c3c3ec7b79c6411053bbeed50f987977
• ocaml(Ltac2_plugin__Tac2expr) = 8d54077db7ebd15964bcc14127ac712c
• ocaml(Ltac2_plugin__Tac2externals) = 9e6cffd1357c16609c8d2f84a756c6e0
• ocaml(Ltac2_plugin__Tac2extffi) = c9358d378b9d8fadc00ee11a8ed1e693
• ocaml(Ltac2_plugin__Tac2ffi) = 681b80e10842ae90ae4d8c157dc459ba
• ocaml(Ltac2_plugin__Tac2intern) = 53b8360df4c10b2784209e2d3d04427b
• ocaml(Ltac2_plugin__Tac2interp) = 93546dc836fa0fea7a62a7b0ca19ebae
• ocaml(Ltac2_plugin__Tac2match) = e04436e616b385aec39f484605a3f680
• ocaml(Ltac2_plugin__Tac2print) = 2bcc26e6e0212464eb0bf3d15463b17b
• ocaml(Ltac2_plugin__Tac2qexpr) = 23ce1a59b48e65b2d071b7ff844ca2fd
• ocaml(Ltac2_plugin__Tac2quote) = ab11804c404501f3407d041c8f12beda
• ocaml(Ltac2_plugin__Tac2stdlib) = abca550d9994176d5a9267d291714021
• ocaml(Ltac2_plugin__Tac2tactics) = c887ff016372c15939e60d4905b39f7e
• ocaml(Ltac2_plugin__Tac2types) = 62df338b234e1e1759dd57e13f555216
• ocaml(Ltac2_plugin__Tac2typing_env) = 227ff9099695afda98ebe7f144bbea31
• ocaml(Ltac2_plugin__Tac2val) = 3c519baec408544ea1710a7c68791dc3
• ocaml(Ltac_plugin) = 5409ef6e2f1819f62566d425aa6b978f
• ocaml(Ltac_plugin__ComRewrite) = 5c40765175812a9f71b43508944a7847
• ocaml(Ltac_plugin__Extraargs) = dc3b165984f5ad70592ceb8fc3be4e0b
• ocaml(Ltac_plugin__G_ltac) = dd5179987737a9d4ba8859bfad8c12c1
• ocaml(Ltac_plugin__Internals) = a3b3427b6b675bbd2bdb82b2144c625a
• ocaml(Ltac_plugin__Leminv) = 3e8795f5a561ce69bf8fb1f0aca2aeec
• ocaml(Ltac_plugin__Pltac) = e76dfa9039e057c8e62c20efd6b96c2f
• ocaml(Ltac_plugin__Pptactic) = 03e54c329b30259332800d7aa69bef07
• ocaml(Ltac_plugin__Tacarg) = 4a0e21389d3cb6d1c8c30bec00374f50
• ocaml(Ltac_plugin__Taccoerce) = 95207554c38ce86e6eab2d5cd166cca9
• ocaml(Ltac_plugin__Tacentries) = 33cf52af590ab8bcc3e72b9248747f92
• ocaml(Ltac_plugin__Tacenv) = 5c46901d3f7c582be3fbb04f6d9b60e4
• ocaml(Ltac_plugin__Tacexpr) = 12812dd5ab4f14f215e045033eac11be
• ocaml(Ltac_plugin__Tacintern) = c844d7ea82b55e140d1c4f7e51c7e4a5
• ocaml(Ltac_plugin__Tacinterp) = 699d03891bf128da1a04283dffd01027
• ocaml(Ltac_plugin__Tacsubst) = 941f3bc7c301771608bfe66d0e62a4ca
• ocaml(Ltac_plugin__Tactic_debug) = 6478a1d6638af953e071d5fb0a12671b
• ocaml(Ltac_plugin__Tactic_matching) = b06fb7839e3e2c0ad9e9b92d93d4d8f7
• ocaml(Ltac_pretype) = a2c5dc34c670a49c63c836dcf7de7a96
• ocaml(Memprof_coq) = 52002a7377d174641891b3bb807cfac4
• ocaml(Memtrace_init) = 767bc231aec961de2ef9b3b9c923a001
• ocaml(Metasyntax) = d18e2229c276013295934e1339adbc5f
• ocaml(Micromega_core_plugin) = 7431add2f7d94df09a1d16829af126c7
• ocaml(Micromega_core_plugin__Micromega) = 71eec3b72c1bc19482934ced988a0111
• ocaml(Micromega_core_plugin__Mutils) = 1a771d55f1eb75dcb6bf1c6298f25a43
• ocaml(Micromega_core_plugin__NumCompat) = b4521a7b0c76da1f719112cab513ab9f
• ocaml(Micromega_core_plugin__Sos_lib) = 7984dbed222b5707b22935261e97a1bf
• ocaml(Micromega_core_plugin__Sos_types) = d35f96b164748f21c9464fc982deec04
• ocaml(Micromega_plugin) = a2028cada0a4dc8d4a36ba485208ccd7
• ocaml(Micromega_plugin__Certificate) = 0ff6bce9e4c0b3e61be7ba859ff9935b
• ocaml(Micromega_plugin__Coq_micromega) = 3001cd3d46ac0fdf05c4506db44780be
• ocaml(Micromega_plugin__Linsolve) = c6bf4a1fed428bc78c04d0870bc55dfd
• ocaml(Micromega_plugin__Persistent_cache) = 8cdec97154e15e90f3ad9f9fd6819e56
• ocaml(Micromega_plugin__Polynomial) = 45d7375512df29400a8b8721e0f09e7e
• ocaml(Micromega_plugin__Simplex) = 27248d453e731e71110165b31132dbe1
• ocaml(Micromega_plugin__Vect) = ef45c5589b09036d2b04e4e340656cc8
• ocaml(Misc) = ea5241d01e1dabb94abc602b35e56ade
• ocaml(Miscprint) = 062bb3184a5513bfbb80d378beba1025
• ocaml(Mltop) = b14524a35006f4706fd165f6fe213ee2
• ocaml(Mod_declarations) = 13ee1b9c6af74eb1079b381c1f5d5b03
• ocaml(Mod_subst) = cd69e5446f1ed18d8f4334e10fe92395
• ocaml(Mod_typing) = 780831b9979c664eb569cccc45b1082c
• ocaml(Modintern) = bf6fe5c41c6b05a80ec20e20fa324898
• ocaml(Modops) = f36841081ffdab5f843b9efe36a6d577
• ocaml(Monad) = 2bde140cae2e992b633c464725202d31
• ocaml(Mutex_aux) = 84cdbad35da10d625c4ac3e57b8d5bf7
• ocaml(Namegen) = b174a577fbeda816c838f72f941b74b9
• ocaml(Nameops) = 89f06fe391f7f072a96548bd25842ee8
• ocaml(Names) = f2fd0dd7f492abdd5e55c86dea1a1714
• ocaml(Nametab) = 3176b47410da26f2bcbc20685fe50185
• ocaml(Nativecode) = be58dac2002ed3eabed855e79f8f4907
• ocaml(Nativeconv) = f75564750b9b4a5aa826f167467fecee
• ocaml(Nativelambda) = 284c1a3c0d3d28cdb7717645e9dc684d
• ocaml(Nativelib) = 4a49f52d766cb5e927901e692c3703b9
• ocaml(Nativelibrary) = 448b58e9c95cc8754ee9cb43823593db
• ocaml(Nativenorm) = 96305a20cf0aa095d02b5e5a4a2209f0
• ocaml(Nativevalues) = 39bb8fe443d39b778855766f9522b9af
• ocaml(NeList) = 7fd80b98ad74757a38fb8feefb62c9a7
• ocaml(NewProfile) = 8624ed40210cb2479d322dd52eb526bc
• ocaml(Notation) = f754d5ecc6d6dd838d62fe593b083152
• ocaml(Notation_gram) = 6c5835e53f97593cdd874e7ff229cd16
• ocaml(Notation_ops) = 776f4a7960ef27bd13a4e4546bc2af39
• ocaml(Notation_term) = c0174eac7679198da1252173eac3cb2c
• ocaml(Notationextern) = 10932840cdb3eba36e4f6c04579e21f6
• ocaml(Notgram_ops) = 07657f9e8b10747d5d9eef6a7487831e
• ocaml(Nsatz_core_plugin) = 76d693b67dd1f6dbcb3a3cbabed1fe1b
• ocaml(Nsatz_core_plugin__Ideal) = a765a74ecb2f99dd029774554da4232f
• ocaml(Nsatz_core_plugin__Nsatz) = 4607cf868606053978ea5697ff7c8b3f
• ocaml(Nsatz_core_plugin__Polynom) = 5ab4d812d86ac931b0eb8972d82a6634
• ocaml(Nsatz_core_plugin__Utile) = 7eeebf3221ebec1b72b4d8fca48d6cb4
• ocaml(Nsatz_plugin) = 0197dfd0d488dc3a12f6db250b8ad92a
• ocaml(NumTok) = 5825058b8c83d39fc9fe3c0a71bb2331
• ocaml(Number_string_notation_plugin) = 5eb1faf58a1d0e41dfb791001450f53d
• ocaml(Number_string_notation_plugin__Number_string) = e65ba3a6c5c53cdcfeb328c1c88a28c1
• ocaml(ObjFile) = 25dd0e5647c5865eaa71e7db809a9e5f
• ocaml(Opaqueproof) = 799dbdae573f9a52f90d6ff934941d4a
• ocaml(Opaques) = a8863e22cf7cd58d47dd276ac84ab103
• ocaml(Oprint) = a9904171b8bf1832d4d8d6c06ba280db
• ocaml(Option) = 41b74a99c114f72e84a33073de712a98
• ocaml(OrderedType) = 028516fb8b4953517cfa25d8cafb99fd
• ocaml(Outcometree) = 793c2f1dc6a3183ed387453b3e75c9df
• ocaml(PConstraints) = c690155ab24d08ceeba565bc16954fc4
• ocaml(Parray) = ada8d69c7b1080d775636133f4554360
• ocaml(Parsetree) = a8e773e1784913e8af2f5f83ed53a93b
• ocaml(Partac) = b5aa49e8447f56224772f0a28da09664
• ocaml(Partial_subst) = d0a694f2626cecd5d818f389ea1954a2
• ocaml(Path) = d652fc6085398c2f07e51fed32d448b8
• ocaml(Pattern) = 1d4e37d22fd34a8df4e8b3db774f8309
• ocaml(Patternops) = 00a9ec148173c39ba537740691c95d33
• ocaml(Perf) = f9658dac7d62890a1935a30afa3f96c9
• ocaml(PolyFlags) = 8398e1086f0ee914cfcb2df7139aa845
• ocaml(PolyMap) = 7c20f956cc0034d20d7e6b409315331f
• ocaml(Pp) = a3240b9aca1401ce479dc8d56de4079e
• ocaml(Pp_diff) = ad557b5b20afce42083bda5bb86c722a
• ocaml(Ppconstr) = 7a454380986fa68a0373e621c0f50a69
• ocaml(Ppextend) = 55a1419a527e0e79e5c67cb07733bb25
• ocaml(Ppred) = 352c0c70a3c0c782341946504bc61deb
• ocaml(Pputils) = 439da0d400fc7c4b4791eefc60ce5cd2
• ocaml(Ppvernac) = c5c8b7b775e533fd44b6aca1a42ce3fc
• ocaml(Predicate) = 8dab2e64145accdd2f7a4ca1384b7899
• ocaml(Prettyp) = 9d72eee673b5a29740264ffbc1b153a2
• ocaml(Pretype_errors) = bcb24fe208ddaf4e727fa790749ecd13
• ocaml(Pretyping) = a539cd1213c71b3eaebdb3818e7fe62a
• ocaml(PrimNotations) = 270a1f621fcf0b5178e1968dcc0780a9
• ocaml(Primitive) = 691172872c2967e1d5ca29687c0c6b3f
• ocaml(Primred) = 4db1e0fbff68b72d29343688355b5dcc
• ocaml(Printer) = 1c411c6a4f8fb1658cac2eb2e5b0c146
• ocaml(PrintingFlags) = 3dde8fa6a4dc454860bc3664e97381d1
• ocaml(Printmod) = f609ff3d3f109602a1675968afd0463c
• ocaml(Procq) = 112d6b56f13fa1ef00e41939bba4dbac
• ocaml(Profile) = c057f723b65cb54f6058b2938cfc50a4
• ocaml(Profile_tactic) = 49d25a379ea78ed1643efb2bd3be751b
• ocaml(Program) = 8f5e6f2b8c4ce003d565cb9f564fd4cd
• ocaml(Proof) = db79d4c0a7e3bb1b95089876ddbb3d66
• ocaml(Proof_bullet) = ec74a74b6ccb18651583e503bc9ac83c
• ocaml(Proof_diffs) = d6e55d8704f5278408895153af4d77ce
• ocaml(Proof_using) = 488a3c7beda5289ec83c5a901c135d5e
• ocaml(Proofview) = 8c85721b9dbaf6f01c34d63a398671ec
• ocaml(Proofview_monad) = ab3df107bc210ba0c80e5c9488ad3cc9
• ocaml(Pstring) = 713359389f44624c284e5e4d20a80627
• ocaml(Pvernac) = 7dddf2cc40091ba6ec2202427730188e
• ocaml(Q) = 8b54816595b0494f1630c558d7f2fdec
• ocaml(QGraph) = 065641915882f0927e614c6b4e9c4ef7
• ocaml(Quickfix) = a8f347b27dc5e58c308b6569477dbfb0
• ocaml(Range) = 8ac81b8659e15fffbbfa2497f5d41683
• ocaml(RecLemmas) = bc1a338445afe6afd711c25170d51eb7
• ocaml(Record) = 34477ad573233bf0058f2d910df9abde
• ocaml(RedFlags) = 2eb5167aa428ffc2dee46c0f70469baa
• ocaml(Redexpr) = 80763b37c9a55d6e7fb3c96ef1b42206
• ocaml(Redops) = c73784922d1e1040242a48fd4e2b34f5
• ocaml(Reduction) = f9f8075bdd3e35465e62788e5de76e80
• ocaml(Reductionops) = b4f9469f95615a8f706cb6fe856bd4e1
• ocaml(Refine) = 2d33429cb3ba8775b915d5770e09c984
• ocaml(Relevanceops) = 3e9c148f2514fb540d4ce1eeee245299
• ocaml(Reserve) = 0ebcbdd5d368730804451ec566a53ecb
• ocaml(RetrieveObl) = 68177f07955eafb3d40dab57a939150d
• ocaml(Retroknowledge) = 77f32338d345cb93374614f30f5aebfe
• ocaml(Retyping) = 46225e269157307199fa084e3158c33d
• ocaml(Rewrite) = e5799616aa661b27d31304b021eca987
• ocaml(Ring_plugin) = cc06a0dbb7faaa0affdb43d6e81922f0
• ocaml(Ring_plugin__Ring) = f12b43772e47fe1924d8bc6422a04950
• ocaml(Ring_plugin__Ring_ast) = 9ffd3fe78692223dbc20d4340202934f
• ocaml(Rocqlib) = 3381a857ec924ce53524361a200d0767
• ocaml(Rtauto_plugin) = bef1b1a95c817e3bc0983d58fab82ec3
• ocaml(Rtauto_plugin__Proof_search) = 2395ba64feb37e1b1843d6a0063fe396
• ocaml(Rtauto_plugin__Refl_tauto) = c304c0029edbc7625a0fd0767cf3ccc7
• ocaml(Rtree) = 76c9c7866446e0e30fb1f7e89ba8fe56
• ocaml(SList) = 8f839b11093748431b165456534a4cde
• ocaml(Safe_typing) = 55e1a196fb880f38e2c1aecb8320c18a
• ocaml(Search) = 53edbf0ebb0d7e4ed6008d30c1e9d832
• ocaml(Section) = 96707675d20e8001e22d98d02571f3b4
• ocaml(Segmenttree) = 3542ef972686acbb94ada459284e6bb0
• ocaml(Shape) = 639524fde7fd305260a62f1e1cefbd0a
• ocaml(Smartlocate) = b4deda0e4ccb53c9ed7e7ed06df000d1
• ocaml(Sorts) = e720410f4c1c87fd15bcc0660e5e2773
• ocaml(Spawn) = e58a5144e73bf5ba67b7439648199d64
• ocaml(Spawned) = 890a65f8a9a58a413fdf47cf3bea91cb
• ocaml(Ssreflect_plugin) = df2edbd9591521138483880f58a1bde5
• ocaml(Ssreflect_plugin__Ssrast) = a5b350aba15eaef237c8a80490d7426c
• ocaml(Ssreflect_plugin__Ssrbwd) = 28664d54c3882fe1e90d5835c06162ea
• ocaml(Ssreflect_plugin__Ssrcommon) = 4fed91f71ea7aacf13214b2ef18e966b
• ocaml(Ssreflect_plugin__Ssrelim) = 31e25d7d2784754ee6d11baef8ecfb30
• ocaml(Ssreflect_plugin__Ssrequality) = 57c6b703d250d154929dcf9608676dac
• ocaml(Ssreflect_plugin__Ssrfwd) = a6e061271275dc1c202199d6b05029f2
• ocaml(Ssreflect_plugin__Ssripats) = 0e0c69df15d3885d612a82cf5bd0d5da
• ocaml(Ssreflect_plugin__Ssrparser) = 60af1aa9b9cdbbf406a09b64230b5544
• ocaml(Ssreflect_plugin__Ssrprinters) = 259370b7c0b40752a58326103bcc4df5
• ocaml(Ssreflect_plugin__Ssrtacticals) = c26528172420e9050de60472bde11324
• ocaml(Ssreflect_plugin__Ssrview) = 9d5edd13f2d0a0ce23288a37619369a4
• ocaml(Ssrmatching_plugin) = 47740f9f41d7bde9b34c128f3187aea8
• ocaml(Ssrmatching_plugin__G_ssrmatching) = 44b2e4c0343e7120e39d7dc4cdba1337
• ocaml(Ssrmatching_plugin__Ssrmatching) = a2e35f1e60ffebaab91d3e3527c078a1
• ocaml(Stateid) = 7a2fd3563391a6fa0d41e519f878e667
• ocaml(Stdarg) = b7dbbaa2930b6cc987b1c4c6f8ddda93
• ocaml(Stdlib) = 7ff659a4a6b8ca32adc85623b24921e4
• ocaml(Stdlib__Arg) = c45f9dbce830bdf7c07d08fc27cae4b2
• ocaml(Stdlib__Array) = c1e9990cfc96f4a80be219086df84a1a
• ocaml(Stdlib__Bigarray) = 53e1fb135dc2b52a9be495706f0fe941
• ocaml(Stdlib__Bool) = 7d26c397d64c30c6bfc9fcc31bfd9e64
• ocaml(Stdlib__Buffer) = 199531813c148c733aa4841901f61885
• ocaml(Stdlib__Bytes) = 673437615face5d16342decc909aee70
• ocaml(Stdlib__Callback) = f81228af62f8d1689727fb188b982c9c
• ocaml(Stdlib__Char) = aab5b2646a35544343b9729f2a340b60
• ocaml(Stdlib__Complex) = 10107702cfc5d64ad493797d02699351
• ocaml(Stdlib__Condition) = 1c01c895aec3b63b8ab8cbe2aa66d19e
• ocaml(Stdlib__Digest) = 34f0d73da12b160ad2ec9f14ef6ccb12
• ocaml(Stdlib__Domain) = f4f911af3a887deb4246da1952f3bbde
• ocaml(Stdlib__Either) = d0d544d8ad6cd8d3916ef604e87e8b79
• ocaml(Stdlib__Ephemeron) = 0e97e578bba2a1892394a875582409b1
• ocaml(Stdlib__Filename) = dca44599068c4f1117dfeb6a2637f3f9
• ocaml(Stdlib__Float) = 982b5c7843be6c7a654d37077ab2df6f
• ocaml(Stdlib__Format) = 59fa71efaaaea19dea6b27602dcaaaa2
• ocaml(Stdlib__Fun) = 69dd52f26a432581d74d2acf8cbfdd4f
• ocaml(Stdlib__Gc) = 7001b1bdc5fa669e74321ebe814f5c3c
• ocaml(Stdlib__Hashtbl) = 962e9d183e8a207a666ca7506cf46032
• ocaml(Stdlib__Int) = 415d62528f7701118a1cda50878c4676
• ocaml(Stdlib__Int32) = eb4f33ed29b560525b336e79955fa30a
• ocaml(Stdlib__Int64) = 29e84e0d87545e4220cc5617eb2d20d5
• ocaml(Stdlib__Lazy) = d0b8d3be22a8b5bdfc9dda1877ae006f
• ocaml(Stdlib__Lexing) = 070822eb5537492e7ac0d885f1627b82
• ocaml(Stdlib__List) = 1f65c7c74ac3633417a8002cc6dd0e53
• ocaml(Stdlib__Map) = 2d8ea4e0be35a4403643e7043fc81316
• ocaml(Stdlib__Marshal) = b6dd359978d92b445715f8b6e7291756
• ocaml(Stdlib__Mutex) = be9647a85be946b28ceaaad8440df78c
• ocaml(Stdlib__Nativeint) = 3274bc361f120620f5df0ee8b898262b
• ocaml(Stdlib__Obj) = 70f3df7415d40eb721c8413fa408b7b6
• ocaml(Stdlib__Printexc) = e58645338ce0e91a971f2806d56d691b
• ocaml(Stdlib__Printf) = 689694603948509ee3d0b39b9ac66005
• ocaml(Stdlib__Queue) = 3b321c1bad5b935cfbf4767b238e4180
• ocaml(Stdlib__Random) = 56f5b48db4d9ef67c6b0228d4fe599b4
• ocaml(Stdlib__Result) = 57c890b1fb51649494b6cefd7d3ddc9b
• ocaml(Stdlib__Scanf) = 2e9739978caab34087dc83418ace9de6
• ocaml(Stdlib__Seq) = 1d1c31e02b77070ff0e51eaaab2af0cc
• ocaml(Stdlib__Set) = f1c0353417503cf69279f65dd7b31d22
• ocaml(Stdlib__Stack) = 8beb90704d5de14f0323d6421c8095d6
• ocaml(Stdlib__String) = 64f1c33cae78f3dd80ca58dbba3deaf9
• ocaml(Stdlib__Sys) = 06196acdacded24c46c02b8acd00223a
• ocaml(Stdlib__Uchar) = f6a44dd0c2e2c80b44deed7eb3c121ef
• ocaml(Stdlib__Weak) = d315fd61fbd009f4439cd0d03c62af48
• ocaml(Stm) = a71a0384c1f676ea7103c0e60a122eb0
• ocaml(Stmargs) = 1b963824eb7d6638699545d167312798
• ocaml(Store) = b9136c58a2dd4791fc1d21a39fb36017
• ocaml(Str) = 82bb8230a6bbf7cb2d8be245938b615a
• ocaml(Structures) = 556e801f8904470774103d34c37bcab0
• ocaml(Subproof) = 85d7ed0308d98d45134433a50866b051
• ocaml(Subst) = b930cee1e6bdd0d12aaa3723dec0cbf8
• ocaml(Subtyping) = b037a6164aa123668a89c2d70adfc285
• ocaml(Summary) = 084ed05b9e4907cf646e45b8c54c4bc0
• ocaml(Synterp) = affa9727766de1c58dc349eb85ebd5dc
• ocaml(System) = aa453721262b2b19fe046ed35ba7d892
• ocaml(TQueue) = 06f2f0c295a422dab7042027e9408739
• ocaml(Tacmach) = 334e4a1cf080990a4ce5a98bd96f969f
• ocaml(Tacred) = fedca45abc194c3b9b4864093c41c8e8
• ocaml(TacticErrors) = 771f84c1709b114b50b36cd6f2589d92
• ocaml(Tactic_option) = c1c662627c5a950b0e8af6a77947703a
• ocaml(Tacticals) = 55f5f370ad390c307aa5ac099a638e2b
• ocaml(Tactics) = f28ce01b433fe7f3890df02f506769a9
• ocaml(Tactypes) = a7de095286524f921722a65b9f8ed3c6
• ocaml(Tauto_plugin) = 9ccf8b9a8e9b5f349fb354a6268da0e1
• ocaml(TemplateArity) = c8782dabc1efe536e79bcc2be157fa03
• ocaml(Term) = 3d306a1e65ea3031cd7a49ad2da617ed
• ocaml(Terminal) = e6ddc9c8ac2d341ec485865bea78afaa
• ocaml(Termops) = 455f9f8153e38b272e98e439ddc1c0ad
• ocaml(Thread) = 99d33b3840c6d249522009e7ea8cf472
• ocaml(Tok) = 8801c057512a080e667eb7474745907e
• ocaml(Top_printers) = 5b16997b6dba9670b29d8d804d47b7f2
• ocaml(Topfmt) = 1a9012eecefedbf6000dd918025bb89c
• ocaml(Toploop) = c80e2fca60fda9d8dfe6e9bfde4f1118
• ocaml(TransparentState) = 8644d4ee2bfdfa34b1a36235e0a1d977
• ocaml(Trie) = 49f3b048c4ef037dc20113ac2ad9654a
• ocaml(Tuto0_plugin) = 55bac9a5a042df8029066af4a5ecc9ab
• ocaml(Tuto0_plugin__Tuto0_main) = 501355a8e6223a4f8b30bcc5108f2dc0
• ocaml(Tuto1_plugin) = 00435ebd7722771ac79d9c776a1817c3
• ocaml(Tuto1_plugin__Inspector) = cec56edb003bd7f80868692373c20d80
• ocaml(Tuto1_plugin__Simple_check) = dd20a8d465f013df6fff493178846768
• ocaml(Tuto1_plugin__Simple_declare) = 6000d64de639c75629e83c67cd1fc086
• ocaml(Tuto1_plugin__Simple_print) = 61724e04c2c8f5e15eebcc073669e68e
• ocaml(Tuto2_plugin) = 184262ed8436fe96abc9a352ae926716
• ocaml(Tuto2_plugin__Counter) = adaec3cc229db9f72843af6871311eeb
• ocaml(Tuto2_plugin__Custom) = 35e76c5ea338b2ed2dd6799a746bbf6c
• ocaml(Tuto2_plugin__Persistent_counter) = 4d4990a44c8c04bbd27cc573d45d6caf
• ocaml(Tuto3_plugin) = 8d95e40d324b36be29469244aa44d456
• ocaml(Tuto3_plugin__Construction_game) = 698b96ef6d38b04fcd3d0c84ca944150
• ocaml(Tuto3_plugin__Tuto_tactic) = 5c27bbade08cdddeb4ed4a2c543efdfc
• ocaml(Tuto4_plugin) = 6a376dcf2741cdebdb070a1441263c46
• ocaml(Type_errors) = fcaabd0444a1c99ae30771def4567fa6
• ocaml(Type_immediacy) = e9c7b29e4682b2c8d33db46d874c4407
• ocaml(Typeclasses) = bf9765dc93febeef19bd2eb13d89dd17
• ocaml(Typeclasses_errors) = 7b3549ebb7a52e622956953db820f03b
• ocaml(Typeops) = 18c9b09ad160b26db4e78fba5af9d506
• ocaml(Types) = 9cd5e0c0403b733edee4d9c7b8a72d97
• ocaml(Typing) = 468691db1cdafa74bff42bcee912af18
• ocaml(UGraph) = 9c5978d0bde2abd2822b261d2e1a9cca
• ocaml(UState) = aa29b6ceccaae7a1eab96c226d3a2fee
• ocaml(UVars) = c9355415dc70887145a72d8c6586ac0f
• ocaml(Uint63) = 7dea127224220e1e5822638ceac8a7d9
• ocaml(Unicode) = 1dcf32c58474279195a1088f1570993e
• ocaml(Unicodetable) = 7978a3214251c9eae8c81d10e7e883a3
• ocaml(Unification) = c075390a6c3e4747d77369646af4bd81
• ocaml(Unionfind) = da600e6dc756b192efcd4d76cbc94ec4
• ocaml(Unit_info) = 3c074c0f4cbfe70413b3f89c1a0fbf56
• ocaml(Univ) = 5ddd51b62bb8fc373e6f4c0b3e0e07fe
• ocaml(UnivFlex) = 3f2516e92af8e41682b718f5e11cc4a0
• ocaml(UnivGen) = 5a0346d1e5e501354e829ca26cad2258
• ocaml(UnivMinim) = 4a0b0c88f64fdc30c06b0437e7d68659
• ocaml(UnivNames) = 7ad2c0d7e256c75ab33656025422facb
• ocaml(UnivProblem) = 8886fae4ff0a2fc623a38efdd041b045
• ocaml(UnivSubst) = fceee105827b99460bba49080174ab8f
• ocaml(Unix) = c1dc7711fef7c883b67ab33c46fd7030
• ocaml(UserWarn) = dcba2d44e488412dfb4707f7d5257625
• ocaml(Util) = c9f8d7b5acde205a5d3eff397851b62d
• ocaml(Values) = 696451dda458a5396ea1e78d5be48ab2
• ocaml(Vars) = df994ed4104d22dd6199c09908f7e786
• ocaml(Vconv) = 5247ee8c4b32bc367827dec1582aed9f
• ocaml(Vcs) = c21c4b1f7e473fefa3470cfd323e4ec5
• ocaml(Vernac) = 9a5ec22c2aeceb3133e1dfd101bea67e
• ocaml(VernacControl) = dd5721708763254002dc366a982d421f
• ocaml(Vernac_classifier) = 472f3d43479ea4c4cb095bcfe26c96ac
• ocaml(Vernacentries) = 3353a7be37f04e064268618f90d8a08c
• ocaml(Vernacexpr) = 355a045286cd9533dd28d43ca21ab3d3
• ocaml(Vernacextend) = cddef177f37a2ff236ff56d76d2465c0
• ocaml(Vernacinterp) = f38a92445f8bffde93ea9b41a6bb1daa
• ocaml(Vernacoptions) = a1890d65a59cfad140d3b44eef63a60e
• ocaml(Vernacprop) = 1a88d5348c01e39bd5550c78317bfc3c
• ocaml(Vernacstate) = f256d15466966f44331436fe91f58dc6
• ocaml(Vernactypes) = 72a11a372c4235e87ce5e9d481e877b2
• ocaml(Vm) = e1125464aa3af1d986db25fca47b1d9c
• ocaml(Vmbytecodes) = 4144dfe2dc51e8ad9b44f360d26ebf9d
• ocaml(Vmbytegen) = e928837c364915fed3165522ca8ab1b7
• ocaml(Vmemitcodes) = e8759e16602042822fb45e01e62d0a21
• ocaml(Vmerrors) = 7f4bee013c2a6196517173017f0a838d
• ocaml(Vmlambda) = 9b7cc21b3affa89e6dce24c8f3a65ea5
• ocaml(Vmlibrary) = ce8bcb7232028a1406ef8f53e810d290
• ocaml(Vmopcodes) = 08d9af700e76e6c5b9dc8272952a751d
• ocaml(Vmsymtable) = 622efe11d51621b5faa1676d6610dad4
• ocaml(Vmvalues) = cbed385c0450bda5a0a236753bf2ae79
• ocaml(Vnorm) = f4f92c4c98dd66ddea0a2ff744218ecf
• ocaml(Warnings) = fb0409a10304c2fa86fc9e127c31ff52
• ocaml(WorkerPool) = e4a4344e47882d81661ed9eb7ec855f3
• ocaml(WriteOnceArray) = e6442549510daf391bca4f3c39b254f1
• ocaml(Xml_datatype) = 467b68b73cffd645333815d6b355f3c7
• ocaml(Z) = b8f36df41ec3ad4dd65a34f697424998
• ocaml(Zify_plugin) = 3726fda4ee09d032689f52a677c41d45
• ocaml(Zify_plugin__Zify) = 759165c544a87ba7704729a65ce8808b
• rocq(ppc-64) = 9.2.0-1.fc45
• rpmlib(CompressedFileNames) <= 3.0.4-1
• rpmlib(FileDigests) <= 4.6.0-1
• rpmlib(PayloadFilesHavePrefix) <= 4.0-1
• rpmlib(PayloadIsZstd) <= 5.4.18-1
• rtld(GNU_HASH)

License

LGPL-2.1-only AND LGPL-2.1-only WITH OCaml-LGPL-linking-exception AND MIT AND BSD-3-Clause

Changelog

* Thu Apr 16 2026 Jerry James <loganjerry@gmail.com> - 9.2.0-1
  - Version 9.2.0
  - Drop upstreamed documentation patch
  - Enable the native compiler for x86_64
* Fri Mar 20 2026 Jerry James <loganjerry@gmail.com> - 9.1.1-1
  - Initial RPM

Files

/usr/bin/csdpcert
/usr/bin/ocamllibdep
/usr/bin/rocq
/usr/bin/rocq.byte
/usr/bin/rocqchk
/usr/bin/votour
/usr/lib/.build-id
/usr/lib/.build-id/03
/usr/lib/.build-id/03/45d3ab52a1e433c393ab744a4b91ab73adba17
/usr/lib/.build-id/07
/usr/lib/.build-id/07/ce075d90aa408d00f62f5911e9235951736724
/usr/lib/.build-id/0e
/usr/lib/.build-id/0e/d337104846fd2e02fef2d3037fddb37edbdc9f
/usr/lib/.build-id/1c
/usr/lib/.build-id/1c/c71ee25ba5807226cd36226a39cd890f160f4b
/usr/lib/.build-id/20
/usr/lib/.build-id/20/33773b86caa48c7db091e253a65a160c06aba0
/usr/lib/.build-id/20/c0fa9bd31d83e15b8c2bbdb99f41d3d812320b
/usr/lib/.build-id/2d
/usr/lib/.build-id/2d/0c0f07a2fa144cef52b85bfff2e1f4bf1f92ad
/usr/lib/.build-id/30
/usr/lib/.build-id/30/3adc5541dd797891377e8447550f4399c33932
/usr/lib/.build-id/32
/usr/lib/.build-id/32/e393c2adb6910835e74c764eafdd5454bb0a81
/usr/lib/.build-id/36
/usr/lib/.build-id/36/40882bf8157590a794b5c832533ec985ac694d
/usr/lib/.build-id/3a
/usr/lib/.build-id/3a/4dc1036e272928afbac49550e0e262a26c161d
/usr/lib/.build-id/3b
/usr/lib/.build-id/3b/9ce79474864fc6d2fef60ecc0c0ba63accb19f
/usr/lib/.build-id/3f
/usr/lib/.build-id/3f/7ee530e2472359480afdd617fe95c60b0994b5
/usr/lib/.build-id/55
/usr/lib/.build-id/55/e5b1a00db5f85f72e3496471cd39c057aa4e2d
/usr/lib/.build-id/56
/usr/lib/.build-id/56/bd31812a2632c830f95e1b2102f553290ef019
/usr/lib/.build-id/58
/usr/lib/.build-id/58/7199648c804d6a6f892df6f25be4010d5faa28
/usr/lib/.build-id/59
/usr/lib/.build-id/59/7dcb14aa82c529da84249429b4ed20645a6726
/usr/lib/.build-id/65
/usr/lib/.build-id/65/84cdc67b18e2f090783964843fa8ce4ce936f5
/usr/lib/.build-id/66
/usr/lib/.build-id/66/837f947aa2da4cf2502c05cc4fa23cd106aaf2
/usr/lib/.build-id/6d
/usr/lib/.build-id/6d/782558f8545aab135a6e475a6122b2fdee4fc0
/usr/lib/.build-id/6f
/usr/lib/.build-id/6f/99675814b78e41ba9c32f9b84b296ad3796d2e
/usr/lib/.build-id/70
/usr/lib/.build-id/70/f50f8b0b83d075aa1b11caae358bbf08a350e4
/usr/lib/.build-id/73
/usr/lib/.build-id/73/89df577ccf270ddef21399d31520017a670619
/usr/lib/.build-id/75
/usr/lib/.build-id/75/49fbad7719a406fc772d7fbb27583d82f1ce77
/usr/lib/.build-id/79
/usr/lib/.build-id/79/970e1fd59e1a3f166e43d16772c13346c1b338
/usr/lib/.build-id/7b
/usr/lib/.build-id/7b/3eb8b23ec634b5742408b0793a878484ed66e1
/usr/lib/.build-id/7d
/usr/lib/.build-id/7d/26b8931c6be97ea485c9ef677fd358ed429720
/usr/lib/.build-id/80
/usr/lib/.build-id/80/2e401d819f4efdd57fc645a80d8095507b24e7
/usr/lib/.build-id/80/809fbbe865792c2353fb1aadd65839eadee2cd
/usr/lib/.build-id/83
/usr/lib/.build-id/83/b857588b68a790bf349e9ca3b9b043439d0c3e
/usr/lib/.build-id/83/e70f5edfceb53f257c51f29721344e6cb3fbb7
/usr/lib/.build-id/85
/usr/lib/.build-id/85/c06b1fbd78a4db267b38f37947023bfaa203f1
/usr/lib/.build-id/89
/usr/lib/.build-id/89/70219de68001df4a9c180f72482545f0d849e4
/usr/lib/.build-id/8e
/usr/lib/.build-id/8e/2538ca511a7d9f7ba45f7ca0bb2745eb1d5a7d
/usr/lib/.build-id/93
/usr/lib/.build-id/93/954afadc74dab898c05aac2e5c4119897fb8cf
/usr/lib/.build-id/95
/usr/lib/.build-id/95/cc545587a94e6c337a2d8a90fe66b498626a30
/usr/lib/.build-id/9a
/usr/lib/.build-id/9a/924e2186cb3ab7cef11cd84b50d0a464df10a7
/usr/lib/.build-id/9b
/usr/lib/.build-id/9b/38703f797a8817fc6d31ab380559a0c4927fbb
/usr/lib/.build-id/9c
/usr/lib/.build-id/9c/91d22fa23f8620f8bc154088d92100da247169
/usr/lib/.build-id/a1
/usr/lib/.build-id/a1/c22e558cfd45d4fe68946e848bd1c0b660cf5c
/usr/lib/.build-id/a2
/usr/lib/.build-id/a2/fb8f1a68a6bed08b8afaae950689f35869b5d8
/usr/lib/.build-id/a3
/usr/lib/.build-id/a3/50d2843e4464197282c0b66b3b5570879b19d2
/usr/lib/.build-id/a4
/usr/lib/.build-id/a4/3929849687377e5642ba8d37d80a3c0cc30b15
/usr/lib/.build-id/a4/bd9923f92493044348ce050d8a2ce9c4bbc97f
/usr/lib/.build-id/a5
/usr/lib/.build-id/a5/c0278f8c405c6bd287fe310f84078b3d70954f
/usr/lib/.build-id/a6
/usr/lib/.build-id/a6/c0d36b095e1cbbd557fe015a7f2892c8679005
/usr/lib/.build-id/ac
/usr/lib/.build-id/ac/30a4e57e70ee410266d0782e9ca500b2d5e1dd
/usr/lib/.build-id/ac/74dbe15abae8cf9f310184d6cf6667e5fc65b0
/usr/lib/.build-id/ae
/usr/lib/.build-id/ae/05e6ff3b7bbba2b240670b3792ddf9f9e7ecbb
/usr/lib/.build-id/b0
/usr/lib/.build-id/b0/2afd7e672b31b8b32a7b0c668303d05ef10666
/usr/lib/.build-id/b2
/usr/lib/.build-id/b2/5a19be9b35eae28a2f2192ae292d2a9e82faaa
/usr/lib/.build-id/c0
/usr/lib/.build-id/c0/050161eec44dd381e7cd424de793783f5f7d92
/usr/lib/.build-id/c7
/usr/lib/.build-id/c7/0f47058fd3536f5eeb5a878a07576511132522
/usr/lib/.build-id/d0
/usr/lib/.build-id/d0/a4ef9210d6de7d74b5ef7226f74c72c0cdccfa
/usr/lib/.build-id/d2
/usr/lib/.build-id/d2/e490daca30ed422ffdb71cb561531b49c55dc0
/usr/lib/.build-id/d4
/usr/lib/.build-id/d4/5fcde0eb79a23076a0c4f66bbbf791017a54bf
/usr/lib/.build-id/d5
/usr/lib/.build-id/d5/ecb450fe1fe74c7dbb2a3d9a5209eca398e467
/usr/lib/.build-id/d6
/usr/lib/.build-id/d6/ef3ee5d6bb09d7a3056f177d6e80c56cd744b1
/usr/lib/.build-id/d8
/usr/lib/.build-id/d8/1c69d3c6ee8d55a9441b2cfb7ef4ac2fa112e1
/usr/lib/.build-id/de
/usr/lib/.build-id/de/59050e3e40380d4efb5c63ab9f2bd017c7a8df
/usr/lib/.build-id/df
/usr/lib/.build-id/df/c26de6f019a6f471db3b7e465de09a389002c2
/usr/lib/.build-id/e5
/usr/lib/.build-id/e5/ef910616d74fba63494be17f0d54f54ffa7109
/usr/lib/.build-id/e9
/usr/lib/.build-id/e9/83b7f922f640c80a0bd4c6db583b81a7cc0a1d
/usr/lib64/ocaml/rocq-runtime
/usr/lib64/ocaml/rocq-runtime/META
/usr/lib64/ocaml/rocq-runtime/boot
/usr/lib64/ocaml/rocq-runtime/boot/boot.cma
/usr/lib64/ocaml/rocq-runtime/boot/boot.cmi
/usr/lib64/ocaml/rocq-runtime/boot/boot.cmxs
/usr/lib64/ocaml/rocq-runtime/boot/boot__Env.cmi
/usr/lib64/ocaml/rocq-runtime/boot/boot__Path.cmi
/usr/lib64/ocaml/rocq-runtime/boot/boot__Usage.cmi
/usr/lib64/ocaml/rocq-runtime/boot/boot__Util.cmi
/usr/lib64/ocaml/rocq-runtime/checklib
/usr/lib64/ocaml/rocq-runtime/checklib/coq_checklib.cma
/usr/lib64/ocaml/rocq-runtime/checklib/coq_checklib.cmi
/usr/lib64/ocaml/rocq-runtime/checklib/coq_checklib.cmxs
/usr/lib64/ocaml/rocq-runtime/checklib/coq_checklib__Analyze.cmi
/usr/lib64/ocaml/rocq-runtime/checklib/coq_checklib__CheckFlags.cmi
/usr/lib64/ocaml/rocq-runtime/checklib/coq_checklib__CheckInductive.cmi
/usr/lib64/ocaml/rocq-runtime/checklib/coq_checklib__CheckLibrary.cmi
/usr/lib64/ocaml/rocq-runtime/checklib/coq_checklib__Check_stat.cmi
/usr/lib64/ocaml/rocq-runtime/checklib/coq_checklib__Coqchk_main.cmi
/usr/lib64/ocaml/rocq-runtime/checklib/coq_checklib__Mod_checking.cmi
/usr/lib64/ocaml/rocq-runtime/checklib/coq_checklib__Safe_checking.cmi
/usr/lib64/ocaml/rocq-runtime/checklib/coq_checklib__Validate.cmi
/usr/lib64/ocaml/rocq-runtime/checklib/coq_checklib__Values.cmi
/usr/lib64/ocaml/rocq-runtime/clib
/usr/lib64/ocaml/rocq-runtime/clib/cArray.cmi
/usr/lib64/ocaml/rocq-runtime/clib/cEphemeron.cmi
/usr/lib64/ocaml/rocq-runtime/clib/cList.cmi
/usr/lib64/ocaml/rocq-runtime/clib/cMap.cmi
/usr/lib64/ocaml/rocq-runtime/clib/cObj.cmi
/usr/lib64/ocaml/rocq-runtime/clib/cSet.cmi
/usr/lib64/ocaml/rocq-runtime/clib/cSig.cmi
/usr/lib64/ocaml/rocq-runtime/clib/cString.cmi
/usr/lib64/ocaml/rocq-runtime/clib/cThread.cmi
/usr/lib64/ocaml/rocq-runtime/clib/cUnix.cmi
/usr/lib64/ocaml/rocq-runtime/clib/clib.cma
/usr/lib64/ocaml/rocq-runtime/clib/clib.cmxs
/usr/lib64/ocaml/rocq-runtime/clib/diff2.cmi
/usr/lib64/ocaml/rocq-runtime/clib/dyn.cmi
/usr/lib64/ocaml/rocq-runtime/clib/exninfo.cmi
/usr/lib64/ocaml/rocq-runtime/clib/hMap.cmi
/usr/lib64/ocaml/rocq-runtime/clib/hashcons.cmi
/usr/lib64/ocaml/rocq-runtime/clib/hashset.cmi
/usr/lib64/ocaml/rocq-runtime/clib/heap.cmi
/usr/lib64/ocaml/rocq-runtime/clib/iStream.cmi
/usr/lib64/ocaml/rocq-runtime/clib/int.cmi
/usr/lib64/ocaml/rocq-runtime/clib/memprof_coq.cmi
/usr/lib64/ocaml/rocq-runtime/clib/monad.cmi
/usr/lib64/ocaml/rocq-runtime/clib/mutex_aux.cmi
/usr/lib64/ocaml/rocq-runtime/clib/neList.cmi
/usr/lib64/ocaml/rocq-runtime/clib/option.cmi
/usr/lib64/ocaml/rocq-runtime/clib/orderedType.cmi
/usr/lib64/ocaml/rocq-runtime/clib/polyMap.cmi
/usr/lib64/ocaml/rocq-runtime/clib/predicate.cmi
/usr/lib64/ocaml/rocq-runtime/clib/range.cmi
/usr/lib64/ocaml/rocq-runtime/clib/sList.cmi
/usr/lib64/ocaml/rocq-runtime/clib/segmenttree.cmi
/usr/lib64/ocaml/rocq-runtime/clib/store.cmi
/usr/lib64/ocaml/rocq-runtime/clib/terminal.cmi
/usr/lib64/ocaml/rocq-runtime/clib/trie.cmi
/usr/lib64/ocaml/rocq-runtime/clib/unicode.cmi
/usr/lib64/ocaml/rocq-runtime/clib/unicodetable.cmi
/usr/lib64/ocaml/rocq-runtime/clib/unionfind.cmi
/usr/lib64/ocaml/rocq-runtime/clib/writeOnceArray.cmi
/usr/lib64/ocaml/rocq-runtime/config
/usr/lib64/ocaml/rocq-runtime/config/byte
/usr/lib64/ocaml/rocq-runtime/config/byte/byte_config.cma
/usr/lib64/ocaml/rocq-runtime/config/byte/coq_byte_config.cmi
/usr/lib64/ocaml/rocq-runtime/config/config.cma
/usr/lib64/ocaml/rocq-runtime/config/config.cmxs
/usr/lib64/ocaml/rocq-runtime/config/coq_config.cmi
/usr/lib64/ocaml/rocq-runtime/coqargs
/usr/lib64/ocaml/rocq-runtime/coqargs/coqargs.cma
/usr/lib64/ocaml/rocq-runtime/coqargs/coqargs.cmi
/usr/lib64/ocaml/rocq-runtime/coqargs/coqargs.cmxs
/usr/lib64/ocaml/rocq-runtime/coqdeplib
/usr/lib64/ocaml/rocq-runtime/coqdeplib/coqdeplib.cma
/usr/lib64/ocaml/rocq-runtime/coqdeplib/coqdeplib.cmi
/usr/lib64/ocaml/rocq-runtime/coqdeplib/coqdeplib.cmxs
/usr/lib64/ocaml/rocq-runtime/coqdeplib/coqdeplib__Args.cmi
/usr/lib64/ocaml/rocq-runtime/coqdeplib/coqdeplib__Common.cmi
/usr/lib64/ocaml/rocq-runtime/coqdeplib/coqdeplib__Dep_info.cmi
/usr/lib64/ocaml/rocq-runtime/coqdeplib/coqdeplib__Error.cmi
/usr/lib64/ocaml/rocq-runtime/coqdeplib/coqdeplib__File_util.cmi
/usr/lib64/ocaml/rocq-runtime/coqdeplib/coqdeplib__Fl.cmi
/usr/lib64/ocaml/rocq-runtime/coqdeplib/coqdeplib__Lexer.cmi
/usr/lib64/ocaml/rocq-runtime/coqdeplib/coqdeplib__Loadpath.cmi
/usr/lib64/ocaml/rocq-runtime/coqdeplib/coqdeplib__Makefile.cmi
/usr/lib64/ocaml/rocq-runtime/coqdeplib/coqdeplib__Rocqdep_main.cmi
/usr/lib64/ocaml/rocq-runtime/coqworkmgrapi
/usr/lib64/ocaml/rocq-runtime/coqworkmgrapi/coqworkmgrApi.cma
/usr/lib64/ocaml/rocq-runtime/coqworkmgrapi/coqworkmgrApi.cmi
/usr/lib64/ocaml/rocq-runtime/coqworkmgrapi/coqworkmgrApi.cmxs
/usr/lib64/ocaml/rocq-runtime/debugger_support
/usr/lib64/ocaml/rocq-runtime/debugger_support/debugger_support.cma
/usr/lib64/ocaml/rocq-runtime/debugger_support/debugger_support.cmi
/usr/lib64/ocaml/rocq-runtime/debugger_support/debugger_support.cmxs
/usr/lib64/ocaml/rocq-runtime/dev
/usr/lib64/ocaml/rocq-runtime/dev/dev.cma
/usr/lib64/ocaml/rocq-runtime/dev/dev.cmxs
/usr/lib64/ocaml/rocq-runtime/dev/ml_toplevel
/usr/lib64/ocaml/rocq-runtime/dev/ml_toplevel/include
/usr/lib64/ocaml/rocq-runtime/dev/ml_toplevel/include_directories
/usr/lib64/ocaml/rocq-runtime/dev/ml_toplevel/include_printers
/usr/lib64/ocaml/rocq-runtime/dev/ml_toplevel/include_utilities
/usr/lib64/ocaml/rocq-runtime/dev/top_printers.cmi
/usr/lib64/ocaml/rocq-runtime/dev/vm_printers.cmi
/usr/lib64/ocaml/rocq-runtime/engine
/usr/lib64/ocaml/rocq-runtime/engine/eConstr.cmi
/usr/lib64/ocaml/rocq-runtime/engine/engine.cma
/usr/lib64/ocaml/rocq-runtime/engine/engine.cmxs
/usr/lib64/ocaml/rocq-runtime/engine/evar_kinds.cmi
/usr/lib64/ocaml/rocq-runtime/engine/evarnames.cmi
/usr/lib64/ocaml/rocq-runtime/engine/evarutil.cmi
/usr/lib64/ocaml/rocq-runtime/engine/evd.cmi
/usr/lib64/ocaml/rocq-runtime/engine/ftactic.cmi
/usr/lib64/ocaml/rocq-runtime/engine/logic_monad.cmi
/usr/lib64/ocaml/rocq-runtime/engine/namegen.cmi
/usr/lib64/ocaml/rocq-runtime/engine/nameops.cmi
/usr/lib64/ocaml/rocq-runtime/engine/polyFlags.cmi
/usr/lib64/ocaml/rocq-runtime/engine/profile_tactic.cmi
/usr/lib64/ocaml/rocq-runtime/engine/proofview.cmi
/usr/lib64/ocaml/rocq-runtime/engine/proofview_monad.cmi
/usr/lib64/ocaml/rocq-runtime/engine/termops.cmi
/usr/lib64/ocaml/rocq-runtime/engine/uState.cmi
/usr/lib64/ocaml/rocq-runtime/engine/univFlex.cmi
/usr/lib64/ocaml/rocq-runtime/engine/univGen.cmi
/usr/lib64/ocaml/rocq-runtime/engine/univMinim.cmi
/usr/lib64/ocaml/rocq-runtime/engine/univNames.cmi
/usr/lib64/ocaml/rocq-runtime/engine/univProblem.cmi
/usr/lib64/ocaml/rocq-runtime/engine/univSubst.cmi
/usr/lib64/ocaml/rocq-runtime/gramlib
/usr/lib64/ocaml/rocq-runtime/gramlib/gramlib.cma
/usr/lib64/ocaml/rocq-runtime/gramlib/gramlib.cmi
/usr/lib64/ocaml/rocq-runtime/gramlib/gramlib.cmxs
/usr/lib64/ocaml/rocq-runtime/gramlib/gramlib__Gramext.cmi
/usr/lib64/ocaml/rocq-runtime/gramlib/gramlib__Grammar.cmi
/usr/lib64/ocaml/rocq-runtime/gramlib/gramlib__LStream.cmi
/usr/lib64/ocaml/rocq-runtime/gramlib/gramlib__Plexing.cmi
/usr/lib64/ocaml/rocq-runtime/gramlib/gramlib__Stream.cmi
/usr/lib64/ocaml/rocq-runtime/interp
/usr/lib64/ocaml/rocq-runtime/interp/abbreviation.cmi
/usr/lib64/ocaml/rocq-runtime/interp/constrexpr.cmi
/usr/lib64/ocaml/rocq-runtime/interp/constrexpr_ops.cmi
/usr/lib64/ocaml/rocq-runtime/interp/constrextern.cmi
/usr/lib64/ocaml/rocq-runtime/interp/constrintern.cmi
/usr/lib64/ocaml/rocq-runtime/interp/decls.cmi
/usr/lib64/ocaml/rocq-runtime/interp/dumpglob.cmi
/usr/lib64/ocaml/rocq-runtime/interp/genintern.cmi
/usr/lib64/ocaml/rocq-runtime/interp/impargs.cmi
/usr/lib64/ocaml/rocq-runtime/interp/implicit_quantifiers.cmi
/usr/lib64/ocaml/rocq-runtime/interp/interp.cma
/usr/lib64/ocaml/rocq-runtime/interp/interp.cmxs
/usr/lib64/ocaml/rocq-runtime/interp/modintern.cmi
/usr/lib64/ocaml/rocq-runtime/interp/notation.cmi
/usr/lib64/ocaml/rocq-runtime/interp/notation_ops.cmi
/usr/lib64/ocaml/rocq-runtime/interp/notation_term.cmi
/usr/lib64/ocaml/rocq-runtime/interp/notationextern.cmi
/usr/lib64/ocaml/rocq-runtime/interp/numTok.cmi
/usr/lib64/ocaml/rocq-runtime/interp/primNotations.cmi
/usr/lib64/ocaml/rocq-runtime/interp/reserve.cmi
/usr/lib64/ocaml/rocq-runtime/interp/smartlocate.cmi
/usr/lib64/ocaml/rocq-runtime/kernel
/usr/lib64/ocaml/rocq-runtime/kernel/cClosure.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/cPrimitives.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/constant_typing.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/constr.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/context.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/conv_oracle.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/conversion.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/cooking.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/declarations.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/declareops.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/discharge.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/entries.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/environ.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/esubst.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/evar.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/float64.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/float64_common.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/genlambda.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/hConstr.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/indTyping.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/indtypes.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/inductive.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/inferCumulativity.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/kernel.cma
/usr/lib64/ocaml/rocq-runtime/kernel/kernel.cmxs
/usr/lib64/ocaml/rocq-runtime/kernel/mod_declarations.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/mod_subst.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/mod_typing.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/modops.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/names.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/nativecode.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/nativeconv.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/nativelambda.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/nativelib.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/nativelibrary.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/nativevalues.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/opaqueproof.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/pConstraints.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/parray.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/partial_subst.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/primred.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/pstring.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/qGraph.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/redFlags.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/reduction.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/relevanceops.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/retroknowledge.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/rtree.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/safe_typing.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/section.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/sorts.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/subtyping.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/term.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/transparentState.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/type_errors.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/typeops.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/uGraph.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/uVars.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/uint63.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/univ.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/values.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/vars.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/vconv.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/vm.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/vmbytecodes.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/vmbytegen.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/vmemitcodes.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/vmerrors.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/vmlambda.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/vmlibrary.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/vmopcodes.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/vmsymtable.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/vmvalues.cmi
/usr/lib64/ocaml/rocq-runtime/lib
/usr/lib64/ocaml/rocq-runtime/lib/acyclicGraph.cmi
/usr/lib64/ocaml/rocq-runtime/lib/aux_file.cmi
/usr/lib64/ocaml/rocq-runtime/lib/cAst.cmi
/usr/lib64/ocaml/rocq-runtime/lib/cDebug.cmi
/usr/lib64/ocaml/rocq-runtime/lib/cErrors.cmi
/usr/lib64/ocaml/rocq-runtime/lib/cWarnings.cmi
/usr/lib64/ocaml/rocq-runtime/lib/control.cmi
/usr/lib64/ocaml/rocq-runtime/lib/coqProject_file.cmi
/usr/lib64/ocaml/rocq-runtime/lib/dAst.cmi
/usr/lib64/ocaml/rocq-runtime/lib/deprecation.cmi
/usr/lib64/ocaml/rocq-runtime/lib/envars.cmi
/usr/lib64/ocaml/rocq-runtime/lib/feedback.cmi
/usr/lib64/ocaml/rocq-runtime/lib/flags.cmi
/usr/lib64/ocaml/rocq-runtime/lib/hook.cmi
/usr/lib64/ocaml/rocq-runtime/lib/instr.cmi
/usr/lib64/ocaml/rocq-runtime/lib/lib.cma
/usr/lib64/ocaml/rocq-runtime/lib/lib.cmxs
/usr/lib64/ocaml/rocq-runtime/lib/loc.cmi
/usr/lib64/ocaml/rocq-runtime/lib/newProfile.cmi
/usr/lib64/ocaml/rocq-runtime/lib/objFile.cmi
/usr/lib64/ocaml/rocq-runtime/lib/pp.cmi
/usr/lib64/ocaml/rocq-runtime/lib/pp_diff.cmi
/usr/lib64/ocaml/rocq-runtime/lib/quickfix.cmi
/usr/lib64/ocaml/rocq-runtime/lib/spawn.cmi
/usr/lib64/ocaml/rocq-runtime/lib/stateid.cmi
/usr/lib64/ocaml/rocq-runtime/lib/system.cmi
/usr/lib64/ocaml/rocq-runtime/lib/userWarn.cmi
/usr/lib64/ocaml/rocq-runtime/lib/util.cmi
/usr/lib64/ocaml/rocq-runtime/lib/xml_datatype.cmi
/usr/lib64/ocaml/rocq-runtime/library
/usr/lib64/ocaml/rocq-runtime/library/coqlib.cmi
/usr/lib64/ocaml/rocq-runtime/library/global.cmi
/usr/lib64/ocaml/rocq-runtime/library/globnames.cmi
/usr/lib64/ocaml/rocq-runtime/library/goptions.cmi
/usr/lib64/ocaml/rocq-runtime/library/lib.cmi
/usr/lib64/ocaml/rocq-runtime/library/libnames.cmi
/usr/lib64/ocaml/rocq-runtime/library/libobject.cmi
/usr/lib64/ocaml/rocq-runtime/library/library.cma
/usr/lib64/ocaml/rocq-runtime/library/library.cmxs
/usr/lib64/ocaml/rocq-runtime/library/library_info.cmi
/usr/lib64/ocaml/rocq-runtime/library/locality.cmi
/usr/lib64/ocaml/rocq-runtime/library/nametab.cmi
/usr/lib64/ocaml/rocq-runtime/library/rocqlib.cmi
/usr/lib64/ocaml/rocq-runtime/library/summary.cmi
/usr/lib64/ocaml/rocq-runtime/parsing
/usr/lib64/ocaml/rocq-runtime/parsing/cLexer.cmi
/usr/lib64/ocaml/rocq-runtime/parsing/extend.cmi
/usr/lib64/ocaml/rocq-runtime/parsing/g_constr.cmi
/usr/lib64/ocaml/rocq-runtime/parsing/g_prim.cmi
/usr/lib64/ocaml/rocq-runtime/parsing/notation_gram.cmi
/usr/lib64/ocaml/rocq-runtime/parsing/notgram_ops.cmi
/usr/lib64/ocaml/rocq-runtime/parsing/parsing.cma
/usr/lib64/ocaml/rocq-runtime/parsing/parsing.cmxs
/usr/lib64/ocaml/rocq-runtime/parsing/pcoq.cmi
/usr/lib64/ocaml/rocq-runtime/parsing/procq.cmi
/usr/lib64/ocaml/rocq-runtime/parsing/tok.cmi
/usr/lib64/ocaml/rocq-runtime/perf
/usr/lib64/ocaml/rocq-runtime/perf/coqperf.cma
/usr/lib64/ocaml/rocq-runtime/perf/coqperf.cmxs
/usr/lib64/ocaml/rocq-runtime/perf/perf.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/btauto
/usr/lib64/ocaml/rocq-runtime/plugins/btauto/btauto_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/btauto/btauto_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/btauto/btauto_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/btauto/btauto_plugin__G_btauto.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/btauto/btauto_plugin__Refl_btauto.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/cc
/usr/lib64/ocaml/rocq-runtime/plugins/cc/cc_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/cc/cc_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/cc/cc_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/cc/cc_plugin__G_congruence.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/cc_core
/usr/lib64/ocaml/rocq-runtime/plugins/cc_core/cc_core_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/cc_core/cc_core_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/cc_core/cc_core_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/cc_core/cc_core_plugin__Ccalgo.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/cc_core/cc_core_plugin__Ccprojectability.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/cc_core/cc_core_plugin__Ccproof.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/cc_core/cc_core_plugin__Cctac.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/derive
/usr/lib64/ocaml/rocq-runtime/plugins/derive/derive_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/derive/derive_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/derive/derive_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/derive/derive_plugin__Derive.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/derive/derive_plugin__G_derive.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/extraction
/usr/lib64/ocaml/rocq-runtime/plugins/extraction/extraction_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/extraction/extraction_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/extraction/extraction_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/extraction/extraction_plugin__Common.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/extraction/extraction_plugin__Extract_env.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/extraction/extraction_plugin__Extraction.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/extraction/extraction_plugin__G_extraction.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/extraction/extraction_plugin__Haskell.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/extraction/extraction_plugin__Json.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/extraction/extraction_plugin__Miniml.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/extraction/extraction_plugin__Mlutil.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/extraction/extraction_plugin__Modutil.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/extraction/extraction_plugin__Ocaml.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/extraction/extraction_plugin__Scheme.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/extraction/extraction_plugin__Table.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/firstorder
/usr/lib64/ocaml/rocq-runtime/plugins/firstorder/firstorder_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/firstorder/firstorder_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/firstorder/firstorder_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/firstorder/firstorder_plugin__G_ground.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/firstorder_core
/usr/lib64/ocaml/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin__Formula.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin__Ground.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin__Instances.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin__Rules.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin__Sequent.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin__Unify.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/funind
/usr/lib64/ocaml/rocq-runtime/plugins/funind/funind_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/funind/funind_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/funind/funind_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/funind/funind_plugin__Functional_principles_proofs.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/funind/funind_plugin__Functional_principles_types.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/funind/funind_plugin__G_indfun.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/funind/funind_plugin__Gen_principle.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/funind/funind_plugin__Glob_term_to_relation.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/funind/funind_plugin__Glob_termops.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/funind/funind_plugin__Indfun.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/funind/funind_plugin__Indfun_common.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/funind/funind_plugin__Invfun.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/funind/funind_plugin__Recdef.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__ComRewrite.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__Coretactics.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__Extraargs.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__Extratactics.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__G_auto.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__G_class.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__G_eqdecide.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__G_ltac.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__G_rewrite.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__G_tactic.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__Internals.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__Leminv.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__Pltac.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__Pptactic.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__Profile_ltac_tactics.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__Tacarg.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__Taccoerce.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__Tacentries.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__Tacenv.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__Tacexpr.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__Tacintern.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__Tacinterp.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__Tacsubst.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__Tactic_debug.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__Tactic_matching.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin__G_ltac2.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2bt.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2core.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2dyn.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2entries.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2env.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2expr.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2externals.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2extffi.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2extravals.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2ffi.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2intern.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2interp.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2match.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2print.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2qexpr.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2quote.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2stdlib.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2tactics.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2types.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2typing_env.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2val.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2_ltac1
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2_ltac1/ltac2_ltac1_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2_ltac1/ltac2_ltac1_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2_ltac1/ltac2_ltac1_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2_ltac1/ltac2_ltac1_plugin__G_ltac2_ltac1.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2_ltac1/ltac2_ltac1_plugin__Tac2core_ltac1.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2_ltac1/ltac2_ltac1_plugin__Tac2quote_ltac1.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2_ltac1/ltac2_ltac1_plugin__Tac2stdlib_ltac1.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/micromega
/usr/lib64/ocaml/rocq-runtime/plugins/micromega/micromega_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/micromega/micromega_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/micromega/micromega_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/micromega/micromega_plugin__Certificate.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/micromega/micromega_plugin__Coq_micromega.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/micromega/micromega_plugin__G_micromega.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/micromega/micromega_plugin__Itv.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/micromega/micromega_plugin__Linsolve.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/micromega/micromega_plugin__Persistent_cache.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/micromega/micromega_plugin__Polynomial.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/micromega/micromega_plugin__Simplex.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/micromega/micromega_plugin__Vect.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/micromega_core
/usr/lib64/ocaml/rocq-runtime/plugins/micromega_core/micromega_core_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/micromega_core/micromega_core_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/micromega_core/micromega_core_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/micromega_core/micromega_core_plugin__Micromega.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/micromega_core/micromega_core_plugin__Mutils.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/micromega_core/micromega_core_plugin__NumCompat.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/micromega_core/micromega_core_plugin__Sos.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/micromega_core/micromega_core_plugin__Sos_lib.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/micromega_core/micromega_core_plugin__Sos_types.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/nsatz
/usr/lib64/ocaml/rocq-runtime/plugins/nsatz/nsatz_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/nsatz/nsatz_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/nsatz/nsatz_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/nsatz/nsatz_plugin__G_nsatz.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/nsatz_core
/usr/lib64/ocaml/rocq-runtime/plugins/nsatz_core/nsatz_core_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/nsatz_core/nsatz_core_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/nsatz_core/nsatz_core_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/nsatz_core/nsatz_core_plugin__Ideal.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/nsatz_core/nsatz_core_plugin__Nsatz.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/nsatz_core/nsatz_core_plugin__Polynom.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/nsatz_core/nsatz_core_plugin__Utile.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/number_string_notation
/usr/lib64/ocaml/rocq-runtime/plugins/number_string_notation/number_string_notation_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/number_string_notation/number_string_notation_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/number_string_notation/number_string_notation_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/number_string_notation/number_string_notation_plugin__G_number_string.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/number_string_notation/number_string_notation_plugin__Number_string.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ring
/usr/lib64/ocaml/rocq-runtime/plugins/ring/ring_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/ring/ring_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ring/ring_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/ring/ring_plugin__G_ring.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ring/ring_plugin__Ring.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ring/ring_plugin__Ring_ast.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/rtauto
/usr/lib64/ocaml/rocq-runtime/plugins/rtauto/rtauto_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/rtauto/rtauto_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/rtauto/rtauto_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/rtauto/rtauto_plugin__G_rtauto.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/rtauto/rtauto_plugin__Proof_search.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/rtauto/rtauto_plugin__Refl_tauto.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ssreflect
/usr/lib64/ocaml/rocq-runtime/plugins/ssreflect/ssreflect_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/ssreflect/ssreflect_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ssreflect/ssreflect_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrast.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrbwd.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrcommon.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrelim.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrequality.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrfwd.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssripats.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrparser.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrprinters.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrtacs.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrtacticals.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrvernac.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrview.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ssrmatching
/usr/lib64/ocaml/rocq-runtime/plugins/ssrmatching/ssrmatching_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/ssrmatching/ssrmatching_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ssrmatching/ssrmatching_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/ssrmatching/ssrmatching_plugin__G_ssrmatching.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ssrmatching/ssrmatching_plugin__Ssrmatching.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/tauto
/usr/lib64/ocaml/rocq-runtime/plugins/tauto/tauto_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/tauto/tauto_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/tauto/tauto_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/tauto/tauto_plugin__Tauto.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p0
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p0/tuto0_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p0/tuto0_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p0/tuto0_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p0/tuto0_plugin__G_tuto0.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p0/tuto0_plugin__Tuto0_main.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p1
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p1/tuto1_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p1/tuto1_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p1/tuto1_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p1/tuto1_plugin__G_tuto1.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p1/tuto1_plugin__Inspector.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p1/tuto1_plugin__Simple_check.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p1/tuto1_plugin__Simple_declare.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p1/tuto1_plugin__Simple_print.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p2
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p2/tuto2_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p2/tuto2_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p2/tuto2_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p2/tuto2_plugin__Counter.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p2/tuto2_plugin__Custom.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p2/tuto2_plugin__G_tuto2.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p2/tuto2_plugin__Persistent_counter.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p3
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p3/tuto3_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p3/tuto3_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p3/tuto3_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p3/tuto3_plugin__Construction_game.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p3/tuto3_plugin__G_tuto3.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p3/tuto3_plugin__Tuto_tactic.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p4
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p4/tuto4_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p4/tuto4_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p4/tuto4_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p4/tuto4_plugin__Myexternals.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/zify
/usr/lib64/ocaml/rocq-runtime/plugins/zify/zify_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/zify/zify_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/zify/zify_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/zify/zify_plugin__G_zify.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/zify/zify_plugin__Zify.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping
/usr/lib64/ocaml/rocq-runtime/pretyping/arguments_renaming.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/cases.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/cbv.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/coercion.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/coercionops.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/combinators.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/constr_matching.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/detyping.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/evaluable.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/evarconv.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/evardefine.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/evarsolve.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/find_subterm.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/genarg.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/geninterp.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/gensubst.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/globEnv.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/glob_ops.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/glob_term.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/heads.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/inductiveops.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/keys.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/libBinding.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/locus.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/locusops.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/ltac_pretype.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/nativenorm.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/pattern.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/patternops.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/pretype_errors.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/pretyping.cma
/usr/lib64/ocaml/rocq-runtime/pretyping/pretyping.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/pretyping.cmxs
/usr/lib64/ocaml/rocq-runtime/pretyping/printingFlags.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/program.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/reductionops.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/retyping.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/structures.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/tacred.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/templateArity.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/typeclasses.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/typeclasses_errors.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/typing.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/unification.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/vnorm.cmi
/usr/lib64/ocaml/rocq-runtime/printing
/usr/lib64/ocaml/rocq-runtime/printing/genprint.cmi
/usr/lib64/ocaml/rocq-runtime/printing/ppconstr.cmi
/usr/lib64/ocaml/rocq-runtime/printing/ppextend.cmi
/usr/lib64/ocaml/rocq-runtime/printing/pputils.cmi
/usr/lib64/ocaml/rocq-runtime/printing/printer.cmi
/usr/lib64/ocaml/rocq-runtime/printing/printing.cma
/usr/lib64/ocaml/rocq-runtime/printing/printing.cmxs
/usr/lib64/ocaml/rocq-runtime/printing/proof_diffs.cmi
/usr/lib64/ocaml/rocq-runtime/proofs
/usr/lib64/ocaml/rocq-runtime/proofs/clenv.cmi
/usr/lib64/ocaml/rocq-runtime/proofs/goal_select.cmi
/usr/lib64/ocaml/rocq-runtime/proofs/logic.cmi
/usr/lib64/ocaml/rocq-runtime/proofs/miscprint.cmi
/usr/lib64/ocaml/rocq-runtime/proofs/proof.cmi
/usr/lib64/ocaml/rocq-runtime/proofs/proof_bullet.cmi
/usr/lib64/ocaml/rocq-runtime/proofs/proofs.cma
/usr/lib64/ocaml/rocq-runtime/proofs/proofs.cmxs
/usr/lib64/ocaml/rocq-runtime/proofs/refine.cmi
/usr/lib64/ocaml/rocq-runtime/proofs/subproof.cmi
/usr/lib64/ocaml/rocq-runtime/proofs/tacmach.cmi
/usr/lib64/ocaml/rocq-runtime/proofs/tactypes.cmi
/usr/lib64/ocaml/rocq-runtime/revision
/usr/lib64/ocaml/rocq-runtime/rocqnative
/usr/lib64/ocaml/rocq-runtime/rocqshim
/usr/lib64/ocaml/rocq-runtime/rocqshim/rocqshim.cma
/usr/lib64/ocaml/rocq-runtime/rocqshim/rocqshim.cmi
/usr/lib64/ocaml/rocq-runtime/rocqshim/rocqshim.cmxs
/usr/lib64/ocaml/rocq-runtime/rocqworker
/usr/lib64/ocaml/rocq-runtime/rocqworker.byte
/usr/lib64/ocaml/rocq-runtime/rocqworker_with_drop
/usr/lib64/ocaml/rocq-runtime/stm
/usr/lib64/ocaml/rocq-runtime/stm/asyncTaskQueue.cmi
/usr/lib64/ocaml/rocq-runtime/stm/dag.cmi
/usr/lib64/ocaml/rocq-runtime/stm/partac.cmi
/usr/lib64/ocaml/rocq-runtime/stm/proofBlockDelimiter.cmi
/usr/lib64/ocaml/rocq-runtime/stm/spawned.cmi
/usr/lib64/ocaml/rocq-runtime/stm/stm.cma
/usr/lib64/ocaml/rocq-runtime/stm/stm.cmi
/usr/lib64/ocaml/rocq-runtime/stm/stm.cmxs
/usr/lib64/ocaml/rocq-runtime/stm/stmargs.cmi
/usr/lib64/ocaml/rocq-runtime/stm/tQueue.cmi
/usr/lib64/ocaml/rocq-runtime/stm/vcs.cmi
/usr/lib64/ocaml/rocq-runtime/stm/workerPool.cmi
/usr/lib64/ocaml/rocq-runtime/sysinit
/usr/lib64/ocaml/rocq-runtime/sysinit/coqinit.cmi
/usr/lib64/ocaml/rocq-runtime/sysinit/coqloadpath.cmi
/usr/lib64/ocaml/rocq-runtime/sysinit/sysinit.cma
/usr/lib64/ocaml/rocq-runtime/sysinit/sysinit.cmxs
/usr/lib64/ocaml/rocq-runtime/tactics
/usr/lib64/ocaml/rocq-runtime/tactics/abstract.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/allScheme.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/auto.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/autorewrite.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/btermdn.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/cbn.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/class_tactics.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/contradiction.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/declareScheme.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/dn.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/eClause.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/eauto.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/elim.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/elimschemes.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/eqdecide.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/eqschemes.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/equality.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/evar_tactics.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/fixTactics.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/generalize.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/genredexpr.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/gentactic.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/hints.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/hipattern.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/ind_tables.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/indrec.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/induction.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/inv.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/ppred.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/redexpr.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/redops.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/rewrite.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/stdarg.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/tacticErrors.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/tacticals.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/tactics.cma
/usr/lib64/ocaml/rocq-runtime/tactics/tactics.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/tactics.cmxs
/usr/lib64/ocaml/rocq-runtime/tools
/usr/lib64/ocaml/rocq-runtime/tools/CoqMakefile.in
/usr/lib64/ocaml/rocq-runtime/tools/TimeFileMaker.py
/usr/lib64/ocaml/rocq-runtime/tools/coqdoc
/usr/lib64/ocaml/rocq-runtime/tools/coqdoc/coqdoc.css
/usr/lib64/ocaml/rocq-runtime/tools/coqdoc/coqdoc.sty
/usr/lib64/ocaml/rocq-runtime/tools/make-both-single-timing-files.py
/usr/lib64/ocaml/rocq-runtime/tools/make-both-time-files.py
/usr/lib64/ocaml/rocq-runtime/tools/make-one-time-file.py
/usr/lib64/ocaml/rocq-runtime/toplevel
/usr/lib64/ocaml/rocq-runtime/toplevel/ccompile.cmi
/usr/lib64/ocaml/rocq-runtime/toplevel/colors.cmi
/usr/lib64/ocaml/rocq-runtime/toplevel/common_compile.cmi
/usr/lib64/ocaml/rocq-runtime/toplevel/coqc.cmi
/usr/lib64/ocaml/rocq-runtime/toplevel/coqcargs.cmi
/usr/lib64/ocaml/rocq-runtime/toplevel/coqloop.cmi
/usr/lib64/ocaml/rocq-runtime/toplevel/coqrc.cmi
/usr/lib64/ocaml/rocq-runtime/toplevel/coqtop.cmi
/usr/lib64/ocaml/rocq-runtime/toplevel/g_toplevel.cmi
/usr/lib64/ocaml/rocq-runtime/toplevel/load.cmi
/usr/lib64/ocaml/rocq-runtime/toplevel/memtrace_init.cmi
/usr/lib64/ocaml/rocq-runtime/toplevel/toplevel.cma
/usr/lib64/ocaml/rocq-runtime/toplevel/toplevel.cmxs
/usr/lib64/ocaml/rocq-runtime/toplevel/vernac.cmi
/usr/lib64/ocaml/rocq-runtime/toplevel/workerLoop.cmi
/usr/lib64/ocaml/rocq-runtime/vernac
/usr/lib64/ocaml/rocq-runtime/vernac/assumptions.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/attributes.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/auto_ind_decl.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/canonical.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/classes.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/comArguments.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/comAssumption.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/comCoercion.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/comDefinition.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/comExtraDeps.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/comFixpoint.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/comHints.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/comInductive.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/comPrimitive.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/comRewriteRule.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/comSearch.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/comTactic.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/debugHook.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/declare.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/declareInd.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/declareUniv.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/declaremods.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/egramml.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/egramrocq.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/future.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/g_obligations.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/g_proofs.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/g_redexpr.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/g_vernac.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/himsg.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/indschemes.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/library.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/loadpath.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/metasyntax.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/mltop.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/opaques.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/ppvernac.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/prettyp.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/printmod.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/proof_using.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/pvernac.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/recLemmas.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/record.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/retrieveObl.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/search.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/synterp.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/tactic_option.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/topfmt.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/vernac.cma
/usr/lib64/ocaml/rocq-runtime/vernac/vernac.cmxs
/usr/lib64/ocaml/rocq-runtime/vernac/vernacControl.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/vernac_classifier.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/vernacentries.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/vernacexpr.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/vernacextend.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/vernacinterp.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/vernacoptions.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/vernacprop.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/vernacstate.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/vernactypes.cmi
/usr/lib64/ocaml/rocq-runtime/vm
/usr/lib64/ocaml/rocq-runtime/vm/coqrun.cma
/usr/lib64/ocaml/rocq-runtime/vm/coqrun.cmi
/usr/lib64/ocaml/rocq-runtime/vm/coqrun.cmxs
/usr/lib64/ocaml/stublibs/dllcoqperf_stubs.so
/usr/lib64/ocaml/stublibs/dllcoqrun_stubs.so
/usr/share/doc/rocq-runtime
/usr/share/doc/rocq-runtime/README.md
/usr/share/licenses/rocq-runtime
/usr/share/licenses/rocq-runtime/LICENSE
/usr/share/man/man1/rocq.1.gz
/usr/share/man/man1/rocqchk.1.gz
/usr/share/texlive/texmf-dist/tex/latex/misc
/usr/share/texlive/texmf-dist/tex/latex/misc/coqdoc.sty

Generated by rpm2html 1.8.1

Fabrice Bellet, Sun May 10 01:07:46 2026