rocq-runtime-9.3.0-2.fc46 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(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(GenConstr)
• 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(Hopcroft)
• 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__Tac2subst)
• ocaml(Ltac2_plugin__Tac2syn)
• 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__Ftactic)
• 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__RewriteStratAst)
• 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(Rocq_package)
• 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(Ssreflect_rewrite_plugin)
• ocaml(Ssreflect_rewrite_plugin__Ssrrewrite)
• 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(Vernacgoal)
• 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-a100
• /usr/bin/python3
• 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) = 3e03ad9a8eb814f73ced5ebd558074c5
• ocaml(Abstract) = 3db0ebcea1d272d993ee66f1e25d1613
• ocaml(AcyclicGraph) = 3a1c81067dc70d57791663452146237c
• ocaml(AllScheme) = 86c6f3d1a0741201e7d4a6a126a767c4
• ocaml(Arguments_renaming) = 6cac0a8b34d66a4a8d376d4cfdfbb781
• ocaml(Assumptions) = 6cf3d6f053dc994c8f5a907a0dbdfd6a
• ocaml(Asttypes) = 84c3bb90e4690818f538bd778d47b806
• ocaml(AsyncTaskQueue) = d857d85c726f8717d56a95c9a71373db
• ocaml(Attributes) = d096c8ac43d2cacd9448ba9dda56e93f
• ocaml(Auto) = 2713b687050fe07efaee2e7c03043ab6
• ocaml(Auto_ind_decl) = 5605eb40c4b39b9d183f6627fc73e07e
• ocaml(Autorewrite) = 76a0ccc50c69746e3049d3c28787cb12
• ocaml(Aux_file) = c2007f0e91b98178811410a4f7be3e24
• ocaml(Big_int_Z) = 9da002110bfe02e98c8f142c6f7dcd50
• ocaml(Boot) = f4d97e713a6c402b8fdc05370892f9c0
• ocaml(Boot__Env) = 40f0e5eeb9772e25a9a23798b7d8af94
• ocaml(Boot__Path) = 0506595f70d13318efeb83e8c83acf38
• ocaml(Boot__Usage) = f36579e92f4ad02ef5bcba239cef2a95
• ocaml(Boot__Util) = 60f9c252382a2b5b4c6216bf43e56074
• ocaml(Btauto_plugin) = a898c35732bad1cf79e48c8329bfe357
• ocaml(Btauto_plugin__Refl_btauto) = 1def2ac3e50a318176210eea54e6ba44
• ocaml(Btermdn) = 897bd1704f9e9815e22db79ff15a1774
• ocaml(Build_path_prefix_map) = 17a63dccc7a34c84db5fa108594069cf
• ocaml(CArray) = 5b32a33e358714547ce6daeba0f12ad1
• ocaml(CAst) = 82e224aeeb6ae623c7904d0bbaad5e31
• ocaml(CClosure) = 2b5384ff89e439db35135c23f2fa8b35
• ocaml(CDebug) = 450ef430d34972b281d4a0e01c850b22
• ocaml(CEphemeron) = c8ec9684138eae94f9ada62543edc0cf
• ocaml(CErrors) = 32af6018e35ca19e3149465d5ad6363b
• ocaml(CLexer) = 5b17b1276fd8e2bb4eb3977e6aefa7c5
• ocaml(CList) = 0882adb5c5a227e92b2a3a07183e83e6
• ocaml(CMap) = 837039a181f86e448f1157c634bb474a
• ocaml(CObj) = fefc53898cfbaa52c2502f3190ad9218
• ocaml(CPrimitives) = fcbd9bc226240bcc66f9d02e729dd746
• ocaml(CSet) = ab57beff06a6f9226fecced1557e3fe1
• ocaml(CSig) = 8f279bf05864a1b5c1556eda0a6a6b61
• ocaml(CString) = 23fe1bf405354c32f5969b0c163307f1
• ocaml(CThread) = 2181b493c2a74663b35cb6eec95e0ba1
• ocaml(CUnix) = 57f5c9158430515b08a4f211723449fc
• ocaml(CWarnings) = 36b4497d4030f555feabc400b882bd5e
• ocaml(CamlinternalFormat) = 7befae1426868940d5cb072b5eb42b62
• ocaml(CamlinternalFormatBasics) = 5cba8713ea434e43a50cd422bda47dda
• ocaml(CamlinternalLazy) = 39aa2e9bf7e25b383556f7748b45c72f
• ocaml(CamlinternalMod) = 35f37f6a40dd41769a0e040d26ca6d6a
• ocaml(Canonical) = 5b958a4299ed461142ca65f7fbbb846e
• ocaml(Cases) = f0f07b7446321e2332a781f866137054
• ocaml(Cbn) = 6506cc6d5e406dd5fe90af3d22a311d9
• ocaml(Cbv) = c37c532b427c49c64ea0067c21db280f
• ocaml(Cc_core_plugin) = 5008fc268e0aeb962a484f8824d656a8
• ocaml(Cc_core_plugin__Ccalgo) = c22aa428adac2d0f1bc67fb84208c497
• ocaml(Cc_core_plugin__Ccprojectability) = 00d0ed4cc220fe2d805c4c8849490857
• ocaml(Cc_core_plugin__Ccproof) = ee6241b54fe4d0fed94316898aa7403d
• ocaml(Cc_core_plugin__Cctac) = ad8cb7d7352aa12f6c8105309f398853
• ocaml(Cc_plugin) = fa878db0c2ecfbdc0547984e7dea33bf
• ocaml(Ccompile) = 664fa698bb7851f6656561a03c043cbd
• ocaml(Class_tactics) = ae99954ea5016e18f77d3319742139e4
• ocaml(Classes) = 73b5b0b52b49b168efc41fed3a9e1cf2
• ocaml(Clenv) = a266a491c2b3a5445ecd8e9c2baf0d04
• ocaml(Clflags) = 06dc53fbfc3a29476f3b5c57cc184172
• ocaml(Cmi_format) = 727e7c35092afc0b2d4cbd6d8e021283
• ocaml(Coercion) = dd51bc4b7a99585a17152e60d76e5f26
• ocaml(Coercionops) = aac5a27f5af3a417823235d0e9b28a45
• ocaml(Colors) = c3905a5680ecb64d80ec7bbafa5ecd67
• ocaml(ComArguments) = 78b77c0288b5a3c2ac51cb7d4aa3db5f
• ocaml(ComAssumption) = 5ba0561fdff3e536ad749523301497f6
• ocaml(ComCoercion) = c29e85aa8f396a6212a9dd5aaae590fe
• ocaml(ComDefinition) = 62013f88b366052920d32321d99dacfe
• ocaml(ComExtraDeps) = 133c16ed86d98deb2b70c0c5a1ffef50
• ocaml(ComFixpoint) = 624bcd4234368c659e2f3be8d499c843
• ocaml(ComHints) = 67be751e3a02dfec828ca17d862201cb
• ocaml(ComInductive) = 9ea7ca741c9792df189d630353cb5d9d
• ocaml(ComPrimitive) = b09b38c6dad583c47ebf5526258c093b
• ocaml(ComRewriteRule) = 1778dfb92e96ddd8a8ee1bd6d7e9fb1f
• ocaml(ComSearch) = 0b2e8ee3b45b86e845dedc5e7941583a
• ocaml(ComTactic) = 6c9bc0064139e529de96f208a359d1e5
• ocaml(Combinators) = ab222fcdc4bd472a592d696a59292641
• ocaml(Common_compile) = d0bf92558c786749ce41abc42d4e1462
• ocaml(Compenv) = 442a6303ba470f6994376b1562d4b4b9
• ocaml(Config) = a89ea1ef7095df41e649de7dd71ad982
• ocaml(Constant_typing) = b16eed60821115f2e960ec23e3c8b63a
• ocaml(Constr) = df7e2a4da7f89a30b66b29cd31a81888
• ocaml(Constr_matching) = 1ecb58f18dbfac9ec7147766e1d56888
• ocaml(Constrexpr) = 7a7f3d903c551e3eaef7fb6d96693d83
• ocaml(Constrexpr_ops) = 17394f095c0b1e74ed54f59818e05883
• ocaml(Constrextern) = 8fb56712f9175aceff3ae2edea4ff2f7
• ocaml(Constrintern) = ba9c4f4923d82fed5289f9ceb43e2ac1
• ocaml(Context) = 8d2945b2f4eecda30c01c56695ce63cf
• ocaml(Contradiction) = 8a2e318b17207272d7efc3ddac4cb16a
• ocaml(Control) = 01e0463502fedbe82c8d6f90ca7a6337
• ocaml(Conv_oracle) = f0b49e1c643fc060f06db164e70be4b7
• ocaml(Conversion) = 53077d23a51b48b1ef6e37c986a651b9
• ocaml(Cooking) = 5ae23316d7ee355df199f57c65e4053e
• ocaml(CoqProject_file) = 0a4ad9d94c518732392ad439748356a9
• ocaml(Coq_checklib) = 2a01f7303c49edef72de77687ed90e2d
• ocaml(Coq_checklib__Analyze) = 0f443f55e83dd73472aaa84c9cbe1268
• ocaml(Coq_checklib__CheckFlags) = d6973e3c44f8edc58d62b06f13f33947
• ocaml(Coq_checklib__CheckInductive) = b1b490aa1088cc2f01ec4286fe2f739c
• ocaml(Coq_checklib__CheckLibrary) = 62955af07c2723bc775a3493693cc74b
• ocaml(Coq_checklib__Check_stat) = 6e96e5a30d9e748ad95f9c0c0f542ffd
• ocaml(Coq_checklib__Mod_checking) = a1a74d91e23a2a0c61595af71d13b93d
• ocaml(Coq_checklib__Safe_checking) = 166c52e2116cfcb4faeebc20adb0e6f3
• ocaml(Coq_checklib__Validate) = 31936aa730ede570943107b95c53937c
• ocaml(Coq_checklib__Values) = 99587482c4746aa56b10c783218bfe44
• ocaml(Coq_config) = 64d9dcc32fd72183f547b88896dd24eb
• ocaml(Coqargs) = 5ff368f45565ef1fd079f9ea6a40ef68
• ocaml(Coqcargs) = 31110b606dc3e5ceb89921a889590913
• ocaml(Coqdeplib) = 3b3ba740d9fabcbaf811791f04e651cb
• ocaml(Coqdeplib__Args) = a161c435ff741a3d87987eaca817ed5d
• ocaml(Coqdeplib__Common) = 83bb526688a99e9276793b97e60db176
• ocaml(Coqdeplib__Dep_info) = 6a96973c18c245f3ac906130e1307949
• ocaml(Coqdeplib__Error) = 9e6af8cb59587cbda40d4a9876441aa2
• ocaml(Coqdeplib__File_util) = 77cacded7f8695d0fe4eca681a0000e2
• ocaml(Coqdeplib__Fl) = 7f93cdaf9ae9b29bcf560ec4b1368531
• ocaml(Coqdeplib__Lexer) = fb53a7cc47d35814e303031fbece6c3b
• ocaml(Coqdeplib__Loadpath) = db5238e33c0a38351822c1205fda635e
• ocaml(Coqdeplib__Makefile) = a51b9424d0899ecd606895f5e98c875a
• ocaml(Coqinit) = af1a26291b7646fefe3764b9fe7e39c3
• ocaml(Coqloadpath) = 32745135dfe8a7887ce188a6380ba1bd
• ocaml(Coqloop) = 2b286e8f790645863e9221583abcddf5
• ocaml(Coqrc) = 8b864aa19146e96b64177830ccd0c099
• ocaml(Coqtop) = 8a6890ced3aa1d990b292f9b14b852bd
• ocaml(CoqworkmgrApi) = 0303812f0bc2e40262377d7a727b4d4b
• ocaml(DAst) = 4a34d00f14b1fb3b6d87933b2b8c3e86
• ocaml(Dag) = 93ad85e0a9f92f2c241946be044b70de
• ocaml(Data_types) = d266299998caa3e47beb52432207d50d
• ocaml(DebugHook) = f4f7d4f36c40a91d2e60a625d1ca9482
• ocaml(Declarations) = 8521f113298c72a3ac5812b04d721bda
• ocaml(Declare) = 3f1ce37307f93dd30c543d372511a159
• ocaml(DeclareInd) = a3db4e3643fe7d11d4e81f1c9e632ea7
• ocaml(DeclareScheme) = 23f9bd6e0012ca89029b8c04f6dbf465
• ocaml(DeclareUniv) = b525c2dddae1dd78593b5f7e35c41fa0
• ocaml(Declaremods) = 6b00c70539ea383b38e2df724d4cb3f7
• ocaml(Declareops) = a99b75d69019ee043efbedadfe8ac1c1
• ocaml(Decls) = e97b7adef1c5e743459eb583c29b8c27
• ocaml(Deprecation) = 72daf5c2e1d0c43ae081ad46abb47f05
• ocaml(Derive_plugin) = 531eded1c4e33b430f1edab7cf92f39b
• ocaml(Derive_plugin__Derive) = 241dd04b2b414f5c1624ea9513bd90ee
• ocaml(Detyping) = 9dff3fe155c27f0c2b5ac53061238651
• ocaml(Diff2) = 69bada9b51ba3a56b0469c102397d3c2
• ocaml(Discharge) = 5916dc4a7bcec5010cb4f68bed89f3f3
• ocaml(Dn) = 6d6cdd6bd4237efa56f781a415bae887
• ocaml(Dumpglob) = 323600dcfa4238640095ae88a231257e
• ocaml(Dyn) = 635870118eb7d264e928960d419746e1
• ocaml(Dynlink) = 04a4608c31d5414c15167aa05423343d
• ocaml(EClause) = cdae7e08c42ae77150a1dd341030f782
• ocaml(EConstr) = e9226e00fab8941c23ab132865c11b85
• ocaml(Eauto) = 83221c115fbb0d124b5c075f65965f52
• ocaml(Egramml) = e7284692f3686842c7a9194b919bfed0
• ocaml(Egramrocq) = e7837e28a53c4c0730f199bb303cd43b
• ocaml(Elim) = 7b1f70178a66565335a9b9bb7c2fa7c7
• ocaml(Elimschemes) = 86060302d571f728fe4141158e044916
• ocaml(Entries) = 9cd182b90ab7967de91d5ad6dee53084
• ocaml(Env) = ce446975d8bb8fca5c8cab5430ebbe58
• ocaml(Envars) = ccef56ade890607251a63150639459c7
• ocaml(Environ) = e5180a43ac8ee7cafa84c0687733819b
• ocaml(Eqdecide) = ec15db25f2a00933991e39a1a045401c
• ocaml(Eqschemes) = 63f4418dc9fefb61912bdf8f1f2e1c26
• ocaml(Equality) = fed2eb5a0abaae0dbeb72435cf887ee5
• ocaml(Esubst) = 2b6a6d04176e94afe28661c93ba73295
• ocaml(Evaluable) = fb9a1da1e08b3e15c5bfd09ba521028b
• ocaml(Evar) = 5fa86a4867772f87a88c7e8b8006502d
• ocaml(Evar_kinds) = 3bf90fcdc984cd3bcb963f26db452a18
• ocaml(Evar_tactics) = 2e27de5cea4892b49fc7a8f230cd3279
• ocaml(Evarconv) = c0b8fb77f35300884203d6dbda97b958
• ocaml(Evardefine) = 85604def8b1715650729adca91805f61
• ocaml(Evarnames) = f5d62721c7fe8ab8552f38a2a7e0b495
• ocaml(Evarsolve) = 9ed6979c8a0d19c774b2c9340c4a4bf3
• ocaml(Evarutil) = 7cfd7e4d455dda25be2065706b76c97e
• ocaml(Evd) = 1fc7255729e920de2e3957a23b1d0990
• ocaml(Exninfo) = 8b1c1f5a459f237a6eefbdc05e3c0c3a
• ocaml(Extend) = 9876c628441ab0440578998b39329d42
• ocaml(Extraction_plugin) = e32377a97ac510edef83869ea50bad69
• ocaml(Extraction_plugin__Common) = 9c35fe65f80ae0607d805dad718d6175
• ocaml(Extraction_plugin__Extract_env) = 11c31087356c1112452357a66d52d410
• ocaml(Extraction_plugin__Extraction) = 4ef3dcd014dcff442a726a544bf70b78
• ocaml(Extraction_plugin__Haskell) = 3d81a44dca2cf5b2f6f2590c0e8e0971
• ocaml(Extraction_plugin__Json) = 7d1fb4ea7da1003ebbcb4df57586fb45
• ocaml(Extraction_plugin__Miniml) = 495d2b4ee56d64c1b2ec466b16d4ff36
• ocaml(Extraction_plugin__Mlutil) = 535ea1b61d269dff1f537fb1696db8c3
• ocaml(Extraction_plugin__Modutil) = 383859057f43e126b1e368dc3dc03256
• ocaml(Extraction_plugin__Ocaml) = 40c0c73216c31ce7aae4aaa86f55f349
• ocaml(Extraction_plugin__Scheme) = be542bc24ede12d57b0a06957f7784f9
• ocaml(Extraction_plugin__Table) = 75c9272e479975c8fbd1db8e42d075a1
• ocaml(Feedback) = 4f92b417796d05824661283b9659f4c5
• ocaml(Find_subterm) = a1d84b653f42b7d08a1341cfb772f00a
• ocaml(Findlib) = 1b0811e75e5bbadb5e395761f4803f4b
• ocaml(Firstorder_core_plugin) = fec159343c5551bf68c4f6f086016025
• ocaml(Firstorder_core_plugin__Formula) = c153c16d9b4f0424ed2c10d5c8d49ef2
• ocaml(Firstorder_core_plugin__Ground) = 98f4c072a95c4dcd6a0d9b6cce54afbc
• ocaml(Firstorder_core_plugin__Instances) = 548ccd56c0bac24ca4a8abe9e05cd45d
• ocaml(Firstorder_core_plugin__Rules) = 577959dd9311c65bba9511fa4ea83713
• ocaml(Firstorder_core_plugin__Sequent) = aa69d8b9ab947959d8620fbcf8cffdd9
• ocaml(Firstorder_core_plugin__Unify) = 376ecd9fc023d3498a7099f449d25abd
• ocaml(Firstorder_plugin) = 79828095e4c214af613d0c38e2fbef2d
• ocaml(FixTactics) = ad5e01e31798419d0dc3b07cbda70cef
• ocaml(Fl_metascanner) = 78c4d683804858fa509104de11c8b57a
• ocaml(Fl_metatoken) = 2c8d37da38d7744002094a323ec4f8d9
• ocaml(Fl_package_base) = 0d62177de3f8f40d822d731255ccffaf
• ocaml(Flags) = 30184ee5771a3332dff406c069f65359
• ocaml(Float64) = 5f3685872420eb559610ca8cc70758b1
• ocaml(Float64_common) = 91e85657f424d38fc4f7c19628540518
• ocaml(Format_doc) = 1a853d410bfa54de418a18cd588fe8c3
• ocaml(Funind_plugin) = acff96e1b566211dbd5726750b8ee701
• ocaml(Funind_plugin__Functional_principles_proofs) = a15cf9f36d2b848d5ebfd0f6fd035424
• ocaml(Funind_plugin__Functional_principles_types) = 20207a3b3e556e5b883d16bbbe299d7a
• ocaml(Funind_plugin__Gen_principle) = 6a5639bf0bca5fc5896d6f6a40d69f99
• ocaml(Funind_plugin__Glob_term_to_relation) = 0c26d0431989e745bf7723478198f905
• ocaml(Funind_plugin__Glob_termops) = 228ee60e4fc4d79480ed99a67ee76cdb
• ocaml(Funind_plugin__Indfun) = 1efca0af542c7bf419714d0327fd8b7d
• ocaml(Funind_plugin__Indfun_common) = 8c23f4c30a7f185059ddf776c44b1421
• ocaml(Funind_plugin__Invfun) = 93d4710763fcd5aa49e1e498e767e85c
• ocaml(Funind_plugin__Recdef) = 097431e919f556083e50a8088f5079a7
• ocaml(Future) = 1544d268ac0c284d35f88f75a8085dff
• ocaml(G_constr) = 4a8ae42232001991a9b691f954e0923c
• ocaml(G_proofs) = 78e52cdceb2a11d4a10405ce4101e1e3
• ocaml(G_redexpr) = 3192af7b0c6b5e5569c8b442f5675abe
• ocaml(G_toplevel) = b80448a5f8b0c2b45c28bedd044bb86f
• ocaml(G_vernac) = 904602837c0a8db0fb80dc0f6096da55
• ocaml(GenConstr) = 65185ffc24047593f5828e87adcc4f30
• ocaml(Genarg) = 88e393e1c2f9aca258b430b0f1b841f0
• ocaml(Generalize) = 505f577f32107030488b32358777548b
• ocaml(Genintern) = 05ae6bed42ee5297e64dc8d526bc4bf0
• ocaml(Geninterp) = ac861fa0d06a02796607603f22e236f6
• ocaml(Genlambda) = 3a9d6fcb230e2cb024d4f285735f61f4
• ocaml(Genprint) = 36b2ecd578db621d3346f6fdaeabfc25
• ocaml(Genredexpr) = d02dff5fec1e5e8b047de5fd572f7369
• ocaml(Gensubst) = 9d3145c75eb312d6bd3dc7ce5412758a
• ocaml(Gentactic) = 12f2422df644958857b64d3bd3374853
• ocaml(GlobEnv) = dbba7ed119f8fb171e47eb4ecd93aa04
• ocaml(Glob_ops) = dcc3162bf72caaecb1d9d437fa9517f0
• ocaml(Glob_term) = 38c273ab1345450687b92e6b1eeaa56c
• ocaml(Global) = 3d0f26e83fb0160390b5c3b62f70acdf
• ocaml(Globnames) = f2e3eb0708d0d5ba33c09ea42df932eb
• ocaml(Goal_select) = 7abbae8558695ebf7cf7d0bdbb3746ef
• ocaml(Goptions) = 7abf8e9f44c84283abaf24a1df9a916a
• ocaml(Gramlib) = 39dac03c4686a39022523f13c7386381
• ocaml(Gramlib__Gramext) = 02ce9dbbdaefb67b4f538dd8cc1d27ff
• ocaml(Gramlib__Grammar) = bd0560c25a0e110a446a815d111d0a6a
• ocaml(Gramlib__LStream) = 139addcd3080e14c25c60843c2a76637
• ocaml(Gramlib__Plexing) = a1f80e6c5a86fed3acdfccaea6cf1761
• ocaml(Gramlib__Stream) = 051b6e25e750f1de37a7706827c2ab45
• ocaml(HConstr) = 25245590b3006d9bd12d35bdf00b0d41
• ocaml(HMap) = 37c2a395025500674728a6ef0a486832
• ocaml(Hashcons) = 6f55751bed5c20cdac5336a90cab41b5
• ocaml(Hashset) = 8d0a557f8649d7eeae2802c1e49e95e0
• ocaml(Heads) = 69ba7bd674044474bee2d27da708f09a
• ocaml(Heap) = 537d18654f73f81f96142dcfe572ed59
• ocaml(Himsg) = 1647523a6f2187422a9bbdbb7084fe1b
• ocaml(Hints) = 88d72a3cf954d7652421c09361cd331f
• ocaml(Hipattern) = 84738080445efdfaaf7cb79486404e95
• ocaml(Hook) = 4a72c7621b630b54725e8ae286e175fa
• ocaml(Hopcroft) = 89d0ac960ca606d36e60c5e6ca9dac95
• ocaml(IStream) = 682ff6824b27e67750c44c60190cb441
• ocaml(Ident) = 384a9338d15781bf37212ce3cfd033cb
• ocaml(Identifiable) = 3c7ba31da6292c7ed926b7fadbe655aa
• ocaml(Impargs) = 667aa33867e71f407a7a482e35134ddd
• ocaml(Implicit_quantifiers) = 77b610e0e9f9933b5d2c360a683c5389
• ocaml(IndTyping) = 67aea16976b28abcb804eabca4d8d9ee
• ocaml(Ind_tables) = 9ff9385213b7a98e5f06e4d97c82d05a
• ocaml(Indrec) = 2205656bd960168da61a6883e300d08e
• ocaml(Indschemes) = 6354a9b4b23c54c7aba6aa4b409b88ac
• ocaml(Indtypes) = 676719019f22b2ced11d4df602bcb384
• ocaml(Induction) = b48ed5639f2ca93c6d2b591e12a7a325
• ocaml(Inductive) = fe84aedd83057340966d4dc048c9392f
• ocaml(Inductiveops) = 427e20b64b51df944a24f7f03d837320
• ocaml(InferCumulativity) = 9c2f8df44d274baec19be4e1fab40b61
• ocaml(Instr) = ff8b3e60640d1ce38ab256a871a387b0
• ocaml(Int) = 7b2f710437857c7085efa8a2273eebfb
• ocaml(Inv) = cbb73948213ed49b6366f0f47f691277
• ocaml(Keys) = b8e6deba31766085a4182c33dbc88240
• ocaml(Lib) = 4ddc5f734c0016fbc530a51cdf176988
• ocaml(LibBinding) = e403f6d5bec07274c67c8a284fc286be
• ocaml(Libnames) = f65a6ef5bc0c311c53d8d866962ec512
• ocaml(Libobject) = 4d70e8d3496b69e8eae49b646fa96bb9
• ocaml(Library) = fbe2936bd35d7b884d81e28c63ce52ae
• ocaml(Library_info) = 1ed89bb906f8237af7380487798f4eb1
• ocaml(Load) = 3c5a15453c9399e4c4b291414d61b219
• ocaml(Load_path) = 73bdece741485debc05bc796fc46bb27
• ocaml(Loadpath) = 8de81b7cac0219b4ea5383cb0a1191d6
• ocaml(Loc) = 21a354265d941cf38dbb2a6fd6c1695a
• ocaml(Locality) = 048b3e5671573bdd7ffd94f14b5795b6
• ocaml(Location) = 51a5b26cac9b3515839b2a2679b6099c
• ocaml(Locus) = 662cb9155d877e0f698fac2add14a5e5
• ocaml(Locusops) = 26d4afe9bec44727166a2e59077fd9f6
• ocaml(Logic) = fff4ee7f63a989749ea1fd3be22480e1
• ocaml(Logic_monad) = 47f00e57a2bdb32115067e85add08eed
• ocaml(Longident) = 95a4bd2a3e0c7bef7e71005b1ec0c6f7
• ocaml(Ltac2_ltac1_plugin) = 9913d38e5e00cea94740dea133ff4579
• ocaml(Ltac2_ltac1_plugin__Tac2quote_ltac1) = 80079358c16709660c86fe8d6431b48f
• ocaml(Ltac2_plugin) = c85c1be53eb2904a69d2dbd20924646a
• ocaml(Ltac2_plugin__G_ltac2) = c8f3956dd2b7f381edbdbd6e9ad5235e
• ocaml(Ltac2_plugin__Tac2bt) = 346d03c1c8b12b7005f52629cbf676f2
• ocaml(Ltac2_plugin__Tac2core) = 6a9c5bfbfc1403c3f51698e21bca19e0
• ocaml(Ltac2_plugin__Tac2dyn) = 71b2e98930ad85ca58b5a68c1ad19d40
• ocaml(Ltac2_plugin__Tac2entries) = a4a55b80a2d1fa4a17de62e33640a15a
• ocaml(Ltac2_plugin__Tac2env) = 90c1f921142335db6de7da757b61b8c4
• ocaml(Ltac2_plugin__Tac2expr) = 9b209386e57c98370112578602d80b81
• ocaml(Ltac2_plugin__Tac2externals) = 4308b56da7035996f07369d4814b393c
• ocaml(Ltac2_plugin__Tac2extffi) = a758c5d18854132440cbabd4adbec9ca
• ocaml(Ltac2_plugin__Tac2ffi) = 9479948813ef1adcdac83721ff6c5f6f
• ocaml(Ltac2_plugin__Tac2intern) = 2a130d3a93af196e68c87cb73d9f9d33
• ocaml(Ltac2_plugin__Tac2interp) = 3dab439fd4686c786e5cc419f16c1984
• ocaml(Ltac2_plugin__Tac2match) = 5e1a69eea0f0fb53ee8886bd1897e38c
• ocaml(Ltac2_plugin__Tac2print) = ce356b7d2d0b277abbff4d548c530933
• ocaml(Ltac2_plugin__Tac2qexpr) = b2bea0ff8ec85b4ce377ceece3386882
• ocaml(Ltac2_plugin__Tac2quote) = 8629eb0434ba1e8ac2341e280d44a239
• ocaml(Ltac2_plugin__Tac2stdlib) = 58c5d7aee7d405912bda59d940b8e17e
• ocaml(Ltac2_plugin__Tac2subst) = c602d3f7c0b853c3d923d585e861316d
• ocaml(Ltac2_plugin__Tac2syn) = d2bc8f47cebcb5276d85be16f866e198
• ocaml(Ltac2_plugin__Tac2tactics) = e5af0e8b85e9f9cd3d5fc2f177b30d89
• ocaml(Ltac2_plugin__Tac2types) = 98b0a9a9be711b628ed584f57bcd5df4
• ocaml(Ltac2_plugin__Tac2typing_env) = 93d43d7fc8aa5e4079821d18a7454759
• ocaml(Ltac2_plugin__Tac2val) = 37a72d019ffb89442166decf81f04ce8
• ocaml(Ltac_plugin) = 83ee9e9a446caed2aa25318334ada535
• ocaml(Ltac_plugin__ComRewrite) = a242cba7e7ea6a1744cd8bd5ad2e71ea
• ocaml(Ltac_plugin__Extraargs) = 0c1ee21480abca4d50aff7e12df436c0
• ocaml(Ltac_plugin__Ftactic) = 35157a9a2ff60b1caa9aca138c56af7c
• ocaml(Ltac_plugin__G_ltac) = ad6bd8802116d38bd75c6931e68f4c0a
• ocaml(Ltac_plugin__Internals) = 69fc2cd5e06764c96b5828c15f762396
• ocaml(Ltac_plugin__Leminv) = d4614ec83f962908cb293f6346792c7f
• ocaml(Ltac_plugin__Pltac) = 2206aab32aff29b4adde49845f98a2d3
• ocaml(Ltac_plugin__Pptactic) = e19d0cf2731098e2868b06783b01989d
• ocaml(Ltac_plugin__RewriteStratAst) = fc1d3d9aaa3483a1cefaad4bdc93edbe
• ocaml(Ltac_plugin__Tacarg) = 5bc4f3686e6e89fa003449618789b635
• ocaml(Ltac_plugin__Taccoerce) = 0a9760182fbcdf48ce464cffed7d1177
• ocaml(Ltac_plugin__Tacentries) = 74c1295ee81bf61fd938e749a0eb8d50
• ocaml(Ltac_plugin__Tacenv) = e4ff8762620fa51abbb79796f4b3967f
• ocaml(Ltac_plugin__Tacexpr) = 7162909939077763bec2154af664a78a
• ocaml(Ltac_plugin__Tacintern) = bd4f2a127cb6dd211fcd24f6da707069
• ocaml(Ltac_plugin__Tacinterp) = 849639172dbb14c67a004609113af70d
• ocaml(Ltac_plugin__Tacsubst) = fe183b58c7730cafb109ee5a9a620391
• ocaml(Ltac_plugin__Tactic_debug) = c12c13f6d4f36da1a8309b7e44f886d1
• ocaml(Ltac_plugin__Tactic_matching) = 610a5e2add3bea8ee1b38d456dfede06
• ocaml(Ltac_pretype) = b43f8c5ee8ea3be7096b0dc74b94c291
• ocaml(Memprof_coq) = f25531b1080c5c16c70e47930142772d
• ocaml(Memtrace_init) = 58d04398643b281f0869a6c18c285ffc
• ocaml(Metasyntax) = 32b63c7b72329c2efbbb8f6e67f9f263
• ocaml(Micromega_core_plugin) = 3201f6d62ad5f9037cde547e9c7acdeb
• ocaml(Micromega_core_plugin__Micromega) = de335da3ca00d63c8912a113e53cae34
• ocaml(Micromega_core_plugin__Mutils) = c11d59c174cbc6f06e40b3ca4fcf0a35
• ocaml(Micromega_core_plugin__NumCompat) = a43ca4b61be994fe306a5627fa745d4e
• ocaml(Micromega_core_plugin__Sos_lib) = f975a1285c10aac16439602ec7eab50d
• ocaml(Micromega_core_plugin__Sos_types) = 092786202a8a60beeaffbfb6f6cade0a
• ocaml(Micromega_plugin) = 205a7a948b9d600b16fc00642bfaac64
• ocaml(Micromega_plugin__Certificate) = 695b6c88287b5e4311af0b6b8852f55d
• ocaml(Micromega_plugin__Coq_micromega) = eae2b6926adbbecfe70dfd99c8e056e2
• ocaml(Micromega_plugin__Linsolve) = 38ab8141de1c979333a4f9f35b43cb95
• ocaml(Micromega_plugin__Persistent_cache) = e393f23dd28f0b8666566049bc59dd8e
• ocaml(Micromega_plugin__Polynomial) = 60721fba80a8733bf246da682c08e5b4
• ocaml(Micromega_plugin__Simplex) = c8a900835cd4544deed452bcddf47282
• ocaml(Micromega_plugin__Vect) = 1bd2980aaf4e5df01bb934b5685c5ce1
• ocaml(Misc) = 0d02979d540c22b19f23b073524960d2
• ocaml(Miscprint) = ff3208a4deddade7c537d6c419c72303
• ocaml(Mltop) = 21c1265f6e7aabd6aa26403cb7152184
• ocaml(Mod_declarations) = e06d4cfe63987297168195f5a42ab7d4
• ocaml(Mod_subst) = b0c9ab5b36b023d2036647e944dd9356
• ocaml(Mod_typing) = 1b108aeec516cb8fca80a8e25b549bc0
• ocaml(Modintern) = 368fbd1f348bd8900f578304869c1e50
• ocaml(Modops) = 9d0f3b89cf6b7882f243783dc6107fca
• ocaml(Monad) = 3f0799e4953828a3e9354d0beaa1e703
• ocaml(Mutex_aux) = 9782d688445355c8e376c88b4100c2c5
• ocaml(Namegen) = 18f3bfb71aaec79b1158ae8a56366025
• ocaml(Nameops) = 4272a54aca0340870e6fe2b4ebe68722
• ocaml(Names) = 6ff356060ad11a920d51e22e47bb3159
• ocaml(Nametab) = e847fd8676e93b44f5fa69c39e76c599
• ocaml(Nativecode) = ea7b5a4f6f62ac7367e268129708ea2b
• ocaml(Nativeconv) = 61023ed44972b65e69302394cbbc0d5d
• ocaml(Nativelambda) = e0573f2339b6e69762b53915a51b0d6e
• ocaml(Nativelib) = 0e5239edd969afbab4f4ea299ff5b9ee
• ocaml(Nativelibrary) = 0d41916489c474e221e28016fb54477d
• ocaml(Nativenorm) = 5991bb8872c163315ece382848d942ef
• ocaml(Nativevalues) = 4b04d4a8d1eb6002d624698d2834b8cc
• ocaml(NeList) = c3b4b70eb47ab02a25b9fe8168cd599d
• ocaml(NewProfile) = 747facb9cd5e64b105c891715e6e8c69
• ocaml(Notation) = cb333ce6768929a6af12ce3d388d400a
• ocaml(Notation_gram) = ef8ceea2cfacfec9396148205b7c56da
• ocaml(Notation_ops) = 555e46352ac96131bd3aa7d790ecc06e
• ocaml(Notation_term) = 74bca4d5b7c1745664a67e6086d915ce
• ocaml(Notationextern) = aabbc58844f0b1eae295f0eb8c759612
• ocaml(Notgram_ops) = 22562720feb2d0980d15f1a886febcd5
• ocaml(Nsatz_core_plugin) = 39ae3bc27ba2f544e94b60f557101470
• ocaml(Nsatz_core_plugin__Ideal) = d7e93564bb07505146dede688f62022f
• ocaml(Nsatz_core_plugin__Nsatz) = 59a554cc7c2f28f134b9680211b1281e
• ocaml(Nsatz_core_plugin__Polynom) = 0a0b33048d521de58677aae89da71e39
• ocaml(Nsatz_core_plugin__Utile) = 29bc23633d876d42c4bc50bb52835309
• ocaml(Nsatz_plugin) = 7f39f377450040c9a376fc9c62df288a
• ocaml(NumTok) = a03d26633b04837d96c66c2dcc514747
• ocaml(Number_string_notation_plugin) = b4f2909aa71e21d43e14030acfd2b670
• ocaml(Number_string_notation_plugin__Number_string) = 398fa42ca02392c0057e812ee5bec0d0
• ocaml(ObjFile) = 3053bb8a7f0f2db606e9d72cf2016133
• ocaml(Opaqueproof) = f4384254b46adcb7536aef12bb130221
• ocaml(Opaques) = 2fed74753de63f376bba69c415901f2f
• ocaml(Oprint) = 41100dc27016daa02bb188695d01f273
• ocaml(Option) = 92a29a188ae235a287ebc379e4dd25a4
• ocaml(OrderedType) = b1372ffa9e46e6f95b2ac14239a8456f
• ocaml(Outcometree) = e06da280e0e94a919ab84e78620428c2
• ocaml(PConstraints) = 17189f9dd87392f08b12ae19f620b927
• ocaml(Parray) = c91aee66f0a62119d8324dff17c9a4b8
• ocaml(Parsetree) = 2c395b2cb558b295c123ddd00749d7d9
• ocaml(Partac) = a9fbf090ccb5f96f9ad30b4ed0965ec5
• ocaml(Partial_subst) = 293aaba2bff2483262e01afda5396a0a
• ocaml(Path) = 28571ebf710fe2a4e1508233722e3a57
• ocaml(Pattern) = a75f78f4302f2c5bcd55f129bf898963
• ocaml(Patternops) = 2e137c1609f907bc38e06cd1f2c70fb3
• ocaml(Perf) = d6cc427bc06a72de18140a50a353b06e
• ocaml(PolyFlags) = 1dc8f7830e4c0fd285c43e4f2c0f0292
• ocaml(PolyMap) = 629deea55fa3971f3a60fb50351278e0
• ocaml(Pp) = 2c38bf624e0ffbba3e2389beec2065bb
• ocaml(Pp_diff) = 2b6ed2a56506a1ba1dd583fd85114b20
• ocaml(Ppconstr) = 6cd6f071807ba8e835c00aca9e733daf
• ocaml(Ppextend) = 662fc821755e15498da49cfd31a1b6f7
• ocaml(Ppred) = 62bbe8d2ef098df4a01141c9fd4b0419
• ocaml(Pputils) = a210565da1673e06ae71f20b9f782229
• ocaml(Ppvernac) = 863547569230b806ba65f0f01b9751bc
• ocaml(Predicate) = 0c221b82d5cdae9cbeeea482f4dc5d9d
• ocaml(Prettyp) = 6ac158ab7b8b38fafb313ab329242cd7
• ocaml(Pretype_errors) = 615dd6abbb54534b6a65dfd590f8ab30
• ocaml(Pretyping) = 703c857eaf94c8a0fcabaa76ddc09dbe
• ocaml(PrimNotations) = 0464fd5c3ca69ca578c6d33585074937
• ocaml(Primitive) = 61bc56d5729acca0db75e86a73414d62
• ocaml(Primred) = 17d6c841fe4ae6e4dcb63f13fdac8b24
• ocaml(Printer) = 056058ba08cd785dd54ada500090215e
• ocaml(PrintingFlags) = c0e8c81b3a9a7d0cf9def9fa1962e107
• ocaml(Printmod) = cac311b01d156e0ebf19ea1fb28a18c9
• ocaml(Procq) = ab96378ae424307582c134492929c08e
• ocaml(Profile_tactic) = 3575d2703c6d7faa9c6aba6d63a1171e
• ocaml(Program) = db14026fe4644dc9d44a44d3029e69d0
• ocaml(Proof) = 4382068327590952b0858326ff4b1e76
• ocaml(Proof_bullet) = 863864a9146305d98c8f0e3df1ab4392
• ocaml(Proof_diffs) = 77bb24586136aa0dade0d17203567fd7
• ocaml(Proof_using) = 20abe9e9c09484adc8306b17bd0e1a09
• ocaml(Proofview) = 400cf377a782a1f712ede78f3e39fae9
• ocaml(Proofview_monad) = 3a39c693a2ed79183f754ae14b8bf9e3
• ocaml(Pstring) = a4657eedcbcee758e124eaf4bdbd082f
• ocaml(Pvernac) = 61ac6edba9e34c62faf47b6f1e8a3a2a
• ocaml(Q) = 659754a9895bf87cdc992c6ffcc4b20a
• ocaml(QGraph) = 690eb78a9a96b073877b0c3bb0af7ea6
• ocaml(Quickfix) = 6411323f133a4e6c78dfb40797324ae3
• ocaml(Range) = 6ed92645e449c3ef676dfc9a6be1f0c9
• ocaml(RecLemmas) = 3bbd24d131e004f176e88462e16a2f15
• ocaml(Record) = 66e6dcf4cfe8411c0228cd57128316d2
• ocaml(RedFlags) = 5dbe773f4b767c2f5775347d0b9b214f
• ocaml(Redexpr) = adb59667c8e3fe25336d34acf959f228
• ocaml(Redops) = efc902fc6d2a2345c0361b2c1aa0baaa
• ocaml(Reduction) = b8c6a69007180ca7ebc8a7cf747fca05
• ocaml(Reductionops) = c2bf4b555a27f2d7f9dc6a8293cab305
• ocaml(Refine) = 6c2baaf941b98db95f0e53e4fa51cd0e
• ocaml(Relevanceops) = 5b5e4b46f82acc09ee30a6464c08d4be
• ocaml(Reserve) = c76ac0c4b7603aa4b9528aebee49a039
• ocaml(RetrieveObl) = 8f11e35e0971485cd42685d860ea790f
• ocaml(Retroknowledge) = b955e58fb3fc105283e5619028171464
• ocaml(Retyping) = d99907bd3f2674f22a3723537e312008
• ocaml(Rewrite) = 6336e73fcd5f2d14455bf68fac602e92
• ocaml(Ring_plugin) = 4ac790d60349779bbe9e1667d30ccf7c
• ocaml(Ring_plugin__Ring) = 192d5249b2039f4834b9414f103fe27f
• ocaml(Ring_plugin__Ring_ast) = a335a821932ffe61cbe0ded357d9e6d9
• ocaml(Rocq_package) = f79cf03db912ca8db1c54eb87b455f8c
• ocaml(Rocqlib) = f2301bfd86f788929cd744488e8b290c
• ocaml(Rtauto_plugin) = 4ab59950a066db48e1f4f8d478c5e685
• ocaml(Rtauto_plugin__Proof_search) = 77c63c69325a6e3470f8d216b881a2ed
• ocaml(Rtauto_plugin__Refl_tauto) = 69de4e9deba81928773143090c4cd593
• ocaml(Rtree) = 683dc5c1cae8cd670dfc3f71811fd518
• ocaml(SList) = 4bc007590fe5ee6fa7d6f33af5ae66c9
• ocaml(Safe_typing) = 277376bfd1a2aa3a20598c8f6822b0af
• ocaml(Search) = 489bf5e63683aa205a4ecec67574963c
• ocaml(Section) = 87eff8fdd3cf9756c1d705fc3df3d684
• ocaml(Segmenttree) = db935701afb99fb41779e42b0570f32c
• ocaml(Shape) = b28b8301b24f6231950e7868a59a4e1a
• ocaml(Smartlocate) = df7322ea7cd6ca95a554d8797728822d
• ocaml(Sorts) = 26710e3b924fa33ceb0d42818a1d43d6
• ocaml(Spawn) = 7b2414fa666c9b7dc1a7b08236fd40b5
• ocaml(Spawned) = 3f8699948a312ecfdc3d2e579045543d
• ocaml(Ssreflect_plugin) = d0468b4d302a32ee781851b172eba3b0
• ocaml(Ssreflect_plugin__Ssrast) = 82fe2d04f95f0c459db44b83af94db02
• ocaml(Ssreflect_plugin__Ssrbwd) = afce914fbccd8a406e488ed849d12d20
• ocaml(Ssreflect_plugin__Ssrcommon) = 06ec82db5e60200723607bb438f8f4e4
• ocaml(Ssreflect_plugin__Ssrelim) = 41e0f86dc415ac75e9a844b23f662dd6
• ocaml(Ssreflect_plugin__Ssrequality) = b77af692990e20e51eb26d7bec74bba4
• ocaml(Ssreflect_plugin__Ssrfwd) = 7ad2dd27f47e63babc2d3b1a5b11efff
• ocaml(Ssreflect_plugin__Ssripats) = fbaf51fafbcbb3bf52e5d6f2af3d159c
• ocaml(Ssreflect_plugin__Ssrparser) = 503b626c01c93fc2526cf4ec4b2e7c0f
• ocaml(Ssreflect_plugin__Ssrprinters) = 6d786cbfcf92e84d012704b7683b51de
• ocaml(Ssreflect_plugin__Ssrtacs) = 20c4ab95145ee49016c3c4c997ea4d4c
• ocaml(Ssreflect_plugin__Ssrtacticals) = df8a5c47e6f2598b07f1f3aa3be21fca
• ocaml(Ssreflect_plugin__Ssrview) = f7e4b3c4a88f4fb658d8d6c38ace6bbe
• ocaml(Ssreflect_rewrite_plugin) = 211da6e7c0ed1dfddebc80bb32702fbb
• ocaml(Ssrmatching_plugin) = d96290de069eb528f6fba3bb3358eae3
• ocaml(Ssrmatching_plugin__G_ssrmatching) = 43a662f27c8410c1960bb524a5acdf5c
• ocaml(Ssrmatching_plugin__Ssrmatching) = 25d47184dafc403d8f1d0362057a1327
• ocaml(Stateid) = e83e79a53b2cea898a60ab1fd4dd9c36
• ocaml(Stdarg) = afe9c8512f7e8ec803407b35eeaa5525
• ocaml(Stdlib) = 5debf066d2f080eabc33d8b71099252f
• ocaml(Stdlib__Arg) = 7e3499feceb334dcdbfc9de5cbbe5720
• ocaml(Stdlib__Array) = 09ad905d6230fc4f28ae1b69e8675e79
• ocaml(Stdlib__Bigarray) = 904d1271afeb602c556bf1e0f0f8809c
• ocaml(Stdlib__Bool) = 5ae91427633ceab91f24029f0410dfd9
• ocaml(Stdlib__Buffer) = c0940caa52bfb8d306ed2ca69af87ed6
• ocaml(Stdlib__Bytes) = 6fa82d0a58c0eb4ca469f084a70f9a7e
• ocaml(Stdlib__Callback) = 42025ff5ce6207abf8a8d25ca781e771
• ocaml(Stdlib__Char) = de356fade697b3b5bc1222daedbf67b4
• ocaml(Stdlib__Complex) = 7a66a05174368cc820464e6c12a3693c
• ocaml(Stdlib__Condition) = 7a45bec6dbadb9a2653333bf8ee1606d
• ocaml(Stdlib__Digest) = 2b70a92ff90913804cdc1343b1592e27
• ocaml(Stdlib__Domain) = d11ad689f3e35d9892101961a1201121
• ocaml(Stdlib__Either) = e4e548dbb128df23a9325d9cba39fc2f
• ocaml(Stdlib__Ephemeron) = b18622341371e45469e1be04e45ec480
• ocaml(Stdlib__Filename) = 49e046b4f3cb36713e404a980d6fecce
• ocaml(Stdlib__Float) = 800a4b64830048ea38a2f4bea3c77e64
• ocaml(Stdlib__Format) = 5b2f2a54d0831d599db87620d18b8ca1
• ocaml(Stdlib__Fun) = a85d85ba4df5274da68ea85f367a289e
• ocaml(Stdlib__Gc) = 37e5209d1fcf5e8dce14d0ae4850e089
• ocaml(Stdlib__Hashtbl) = 6df0309fbcf3f1661d9e3d07a603aa3e
• ocaml(Stdlib__Int) = 5e2a4d5bb778a7e299ca9d72ed5fcc54
• ocaml(Stdlib__Int32) = 6583ec691ad5b5d0403bb4dba14ff95a
• ocaml(Stdlib__Int64) = 6c1bd23e0da837071a98f3330e9f1242
• ocaml(Stdlib__Lazy) = 9888b2ba7f344f43c41116cffda5081a
• ocaml(Stdlib__Lexing) = 738e4c77ef59ce13f6f1eeecd20678b3
• ocaml(Stdlib__List) = 81a27a0a9af489e91fa1d99f325067c2
• ocaml(Stdlib__Map) = a9944feda56cab2432578db95de546a3
• ocaml(Stdlib__Marshal) = f0b9263e97f9cffe012fc7066989ec9d
• ocaml(Stdlib__Mutex) = bd8525fb671da46bc9b6403559d7e872
• ocaml(Stdlib__Nativeint) = 5a73f569861cc3c66639bcda63a82510
• ocaml(Stdlib__Obj) = 26b40efd5c9a30f8c9c87c6133b5adbf
• ocaml(Stdlib__Printexc) = 3eb12037663b6b68977615f9862f8f66
• ocaml(Stdlib__Printf) = 3303d43852c2d96a670040b4fc4aefc6
• ocaml(Stdlib__Queue) = e259a6289d4b4587c82128e5e4a93d77
• ocaml(Stdlib__Random) = 956621158e7602665cb7b17716307400
• ocaml(Stdlib__Result) = e05eccba6c8a9e6816ad890e6e983d48
• ocaml(Stdlib__Scanf) = 33191b548042a7e51d81e7bc6af87e60
• ocaml(Stdlib__Seq) = b55b17884ef0dff6295517debe21f111
• ocaml(Stdlib__Set) = 878d51b56f0f7be3121d17ee49b6ece5
• ocaml(Stdlib__Stack) = 8c1adfb915ebcf7ee8b1cee69ad6daba
• ocaml(Stdlib__String) = 10f6a338df78df4f5987192086ffa3c9
• ocaml(Stdlib__Sys) = fb4c43482366ca204eebf7f3838d5a55
• ocaml(Stdlib__Uchar) = ffc32f05aeea05f14986ec532040e8b1
• ocaml(Stdlib__Weak) = 3a74e684389751cdee8098f5290a5966
• ocaml(Stm) = c38727a85d3dbd37529b1fcfecf1b8a3
• ocaml(Stmargs) = 462b764f9d9861951fc67898db91fdbe
• ocaml(Store) = 1de301fb58a4f4a9e1840d4a1ecfbf59
• ocaml(Str) = 3f9db3742f7cbfffc4548c52060fe4e8
• ocaml(Structures) = 628255ec4bb61881d89ea8046c32d149
• ocaml(Subproof) = b27f6d43df29d22869785937291c1c4a
• ocaml(Subst) = 606ff9923d3a48209170ec5a40976beb
• ocaml(Subtyping) = e70e6d6d5af4004675d7bab3ddb7cfa4
• ocaml(Summary) = 6a7114aca867d1ad371626e1bb9fab63
• ocaml(Synterp) = f4317d40af47f5f20e0017d048e8c98d
• ocaml(System) = ce68bf520dd74f867cc2d612958c2d08
• ocaml(TQueue) = f5dd9e61590dabf692140761335b6d05
• ocaml(Tacmach) = 852d5df3058387ec950990857f64ce69
• ocaml(Tacred) = 12221273941aa755aa34081d618b1e17
• ocaml(TacticErrors) = 102ab3b200c64589cbb505dd8a4f447e
• ocaml(Tactic_option) = f15d4794e8f4563392667669008a55b1
• ocaml(Tacticals) = 53d2984af5cb58214ad2d8a1cc78bba5
• ocaml(Tactics) = b28bb263084d86b540ee20b1cc12d15c
• ocaml(Tactypes) = 759daa62c8b4c56a65acfd7a651465cf
• ocaml(Tauto_plugin) = 918e0931c7f126c9e170eada82956641
• ocaml(TemplateArity) = 3d68ded8517eadbec9626c1041aa57a9
• ocaml(Term) = 6f94d16e283ac657432c0853c11322cd
• ocaml(Terminal) = f585b9629763d534f04addb6a54b1b92
• ocaml(Termops) = bfeefcaec4f33db22fed70a8151675b4
• ocaml(Thread) = 66bcd6ecb19be0095ebf5c8ed8a06f20
• ocaml(Tok) = 6fe05d553a0bb6fad673cb6a299801ea
• ocaml(Top_printers) = 0864d6d7f7d2a81596f01cf91f05c804
• ocaml(Topfmt) = 2d63271d97e59c69ea1e35c4be32395c
• ocaml(Toploop) = 0306af3bed0f47279c3f9f537f5c2692
• ocaml(TransparentState) = 8a1bc70ed7bf1337d0d663c0eb3bcb15
• ocaml(Trie) = 77dae95cd8ced6de91a944ccc80883c7
• ocaml(Tuto0_plugin) = 98bdc56d15b5bbc517025b43b94da4fa
• ocaml(Tuto0_plugin__Tuto0_main) = fcc3e4d0f7b1d44ce8cb90386c2a8d46
• ocaml(Tuto1_plugin) = 2c22f978ebb0f899a918fef075722aea
• ocaml(Tuto1_plugin__Inspector) = 2e59db5dd3d56912b5e7ac625ca61fbb
• ocaml(Tuto1_plugin__Simple_check) = c431e2d13db4c9bda8f81cf6fecab5db
• ocaml(Tuto1_plugin__Simple_declare) = 0d89e89dda845a19c474d7237fe07583
• ocaml(Tuto1_plugin__Simple_print) = ff2cbed7ed26f971d34b69b76250902b
• ocaml(Tuto2_plugin) = 1b262f332fc647494f840761b34da900
• ocaml(Tuto2_plugin__Counter) = 54706070f98f4e39dadb05e7b5064398
• ocaml(Tuto2_plugin__Custom) = aac9f3cb2f5254dd83298e0c66b4f3c4
• ocaml(Tuto2_plugin__Persistent_counter) = 3cd0f91503285b5c552d5d1869663487
• ocaml(Tuto3_plugin) = 825675f658e21cfe295cdaf265fb962f
• ocaml(Tuto3_plugin__Construction_game) = 303adec0ea2eafb495f92022ee296b8c
• ocaml(Tuto3_plugin__Tuto_tactic) = fd74e5fa8827ea560d7561b398229aab
• ocaml(Tuto4_plugin) = ee6f712d426c5b3bef435e3a182feb7b
• ocaml(Type_errors) = 507657e99d59c1af7d131504a4ef9a70
• ocaml(Type_immediacy) = e4bd8d9064df3fd32bee7c871fb495f7
• ocaml(Typeclasses) = 62b60543da7a4733ec2d8d5d7ecf3959
• ocaml(Typeclasses_errors) = 65574b5b3b51c6af9250bd6d7ecd5d9e
• ocaml(Typeops) = b122bac4631dd809b0285d3d9b24670a
• ocaml(Types) = ee8cb6960cb32ea9e92d4f73174cce37
• ocaml(Typing) = c6b149fb93959d728d46d2e37f462f84
• ocaml(UGraph) = 847dc13f1dc5b23f29a2fe7698dac495
• ocaml(UState) = b047a7952475c86d216d865c5cf169c8
• ocaml(UVars) = ee0a36bf3925debbcee7bbce521a08be
• ocaml(Uint63) = 9876a8b5a0ed526272adc8f269a8c8ab
• ocaml(Unicode) = a85dac65c40c8014b41dfbcadafe3ed1
• ocaml(Unicodetable) = 9b0791030b54609388bfa856c0d58db3
• ocaml(Unification) = 1a2dc1d6e76abc046eeccf7cecc2d3c4
• ocaml(Unionfind) = b23c4b3cf8231679fa6c9a94a6fec7e1
• ocaml(Unit_info) = 11cc0f955fa64ad827b34bfd76aa3d6e
• ocaml(Univ) = 014bbaf5e3dce5f203de6bbadbd5a875
• ocaml(UnivFlex) = f8b4b578e6d27536b25744c6babf53f0
• ocaml(UnivGen) = bee27bd313ff1357c94cbcfe7a2e27f4
• ocaml(UnivMinim) = b5bbf8a504a7ce1b1172b0f6cf7f9397
• ocaml(UnivNames) = 12e0b79d0f9a6f775b03eee74024e38e
• ocaml(UnivProblem) = 0c6f193c8861ee0bdbce58b9f490ba28
• ocaml(UnivSubst) = 1afc6e306f124f54b3a13293319e3ee2
• ocaml(Unix) = 36d29544e3f6b937c99c905deed806c2
• ocaml(UserWarn) = 80a8a1827c08955c83db2604b85ec40d
• ocaml(Util) = 219a82943a407209300fd2eca83af94c
• ocaml(Values) = 45cafd9cf84d283e233b8fe611baf6fe
• ocaml(Vars) = 1e95c11b5e18846dd821c05a30968f5f
• ocaml(Vconv) = e0ddf383f5667cffe06a2b8a8168d58e
• ocaml(Vcs) = 70ea92953d49948117fd7d240a855f4c
• ocaml(Vernac) = c9b4d72fa9e659d66de3dc2bec4413f5
• ocaml(VernacControl) = e2467eb531095ff481324435d2234da7
• ocaml(Vernac_classifier) = b90e0b164295119bef4cdc6583b29f74
• ocaml(Vernacentries) = 7fcd8e6c6d54d9fe0f0ebd990ea5ddac
• ocaml(Vernacexpr) = 20e73fa2d8787db109b6df4bed580521
• ocaml(Vernacextend) = 44769021730903410fff4e3bfa5288d7
• ocaml(Vernacgoal) = c4ea0685ce9f271c61c08329a6481bf8
• ocaml(Vernacinterp) = 4b6dc18510e310d54b363526173371fc
• ocaml(Vernacoptions) = 0731e636cf4772f7c005f47ebf522302
• ocaml(Vernacprop) = f0905e855409e152232502d7cdac545a
• ocaml(Vernacstate) = db8c404ed28f3fba3b8c001030bb0cda
• ocaml(Vernactypes) = bc9e1224f160eaeb3f62603434987ffc
• ocaml(Vm) = 9e14d72de258c845c4939b4b9eef9541
• ocaml(Vmbytecodes) = 954d046ce5da1dfc961fa06f2aedfded
• ocaml(Vmbytegen) = 140da042b17c3ef75f50b07170a3de0a
• ocaml(Vmemitcodes) = c45c237e191360276a3adb6914c2eec1
• ocaml(Vmerrors) = c9c112ea4817ab7910d9c4b8a4c7dd70
• ocaml(Vmlambda) = b7a28b4b401a3fdc2ba0dddc05ecdc2f
• ocaml(Vmlibrary) = 44844e47de8a1eaf70ec7dcf925166d6
• ocaml(Vmopcodes) = 7a5d219e38d56f8304834b93cf550f76
• ocaml(Vmsymtable) = abb37004426b6dcbbe3f978d55a7dccc
• ocaml(Vmvalues) = 07525957dc2974edc153df8656298456
• ocaml(Vnorm) = dc73e60f1da5141c844beed88dc591dd
• ocaml(Warnings) = 0cdc54c744998eb6c79312371851e8ba
• ocaml(WorkerPool) = 1c5bb8fdd244a7294e28cb8001308334
• ocaml(WriteOnceArray) = 14a1f30bda227a8fa2000e7e2ab978bb
• ocaml(Xml_datatype) = 1fc2a66ce0e39b30eb800beefd4367e7
• ocaml(Z) = 6f4dc1533ce2000c365adfd65d52b204
• ocaml(Zify_plugin) = 98e07f2e6d79a604ea4ce6a2f294b78a
• ocaml(Zify_plugin__Zify) = 96fadef910b5b4a558fe5ec25f884784
• rocq(ppc-64) = 9.3.0-2.fc46
• 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

* Sun Sep 27 2026 Jerry James <loganjerry@gmail.com> - 9.3.0-2
  - Disable native compilation for aarch64
* Sun Sep 27 2026 Jerry James <loganjerry@gmail.com> - 9.3.0-1
  - Version 9.3.0
  - Drop upstreamed dune patch
* Tue Sep 15 2026 Richard W.M. Jones <rjones@redhat.com> - 9.2.0-4
  - OCaml 5.5.1 rebuild
* Thu Jul 16 2026 Fedora Release Engineering <releng@fedoraproject.org> - 9.2.0-3
  - Rebuilt for https://fedoraproject.org/wiki/Fedora_45_Mass_Rebuild
* Thu Jul 09 2026 Jerry James <loganjerry@gmail.com> - 9.2.0-2
  - OCaml 5.5.0 rebuild
  - Add patch to adapt to dune 3.24
  - Fix rocq.xml
* 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/00
/usr/lib/.build-id/00/a07092755b278823b8b27dfae07cc30504a31d
/usr/lib/.build-id/05
/usr/lib/.build-id/05/a24391cace77460bb6caf5a43223ebe4020e96
/usr/lib/.build-id/07
/usr/lib/.build-id/07/52725c4aa44d726b81067be9b1c89da3c41f3e
/usr/lib/.build-id/08
/usr/lib/.build-id/08/d056751d51df535250c32f90f013ddc831c7da
/usr/lib/.build-id/0c
/usr/lib/.build-id/0c/4acca54a4709e182b4a13d58c5ac787237d0da
/usr/lib/.build-id/0e
/usr/lib/.build-id/0e/b50167c74476e5726ad45c584809be6210af97
/usr/lib/.build-id/15
/usr/lib/.build-id/15/3a9b023df329e32489a3967156e90843034054
/usr/lib/.build-id/15/cd920aab65e9913adee8cc76d394dc8d2fadfb
/usr/lib/.build-id/18
/usr/lib/.build-id/18/a37d4a503873edf5a145d556a0908607d57864
/usr/lib/.build-id/1b
/usr/lib/.build-id/1b/8524222cacfef8872e57e87be1ec389bab87d5
/usr/lib/.build-id/1f
/usr/lib/.build-id/1f/bfb539568e83e9ed84f7e50ce8457240c47e2e
/usr/lib/.build-id/21
/usr/lib/.build-id/21/f24eb51b0979df4f6c6116812f8ee671047537
/usr/lib/.build-id/24
/usr/lib/.build-id/24/039b37ac0aa4be61a2087749d4970639b20c3d
/usr/lib/.build-id/24/8bcb7c8687d0c0cd413938eda74040090ba4dc
/usr/lib/.build-id/26
/usr/lib/.build-id/26/0b0dfb597fbe4856052fd307833e9b5d3225aa
/usr/lib/.build-id/26/2f8ad99b119ccbdabebefd435626d80032d9c0
/usr/lib/.build-id/2b
/usr/lib/.build-id/2b/d610012ab669817e8b84543976470437244be4
/usr/lib/.build-id/33
/usr/lib/.build-id/33/ae70e11d4d4411bc7d28cc30dad0a1724d3b63
/usr/lib/.build-id/35
/usr/lib/.build-id/35/146e1e5831cdbe8c730f5cfe245f8b984447f4
/usr/lib/.build-id/39
/usr/lib/.build-id/39/c2f258c8dd96bf53022a13b01eba4cd6b8acf9
/usr/lib/.build-id/40
/usr/lib/.build-id/40/23162751d0bd4d7ecc270b30153de504e941db
/usr/lib/.build-id/40/d7bf4473acfeacf21bb8777fb73c8d69793b34
/usr/lib/.build-id/49
/usr/lib/.build-id/49/759f58a32bef85409d90cd4d1eb799734fcf35
/usr/lib/.build-id/4b
/usr/lib/.build-id/4b/8c091d69bfd2bf8b18fbc7efb14c2bb6806bd6
/usr/lib/.build-id/54
/usr/lib/.build-id/54/0f38ed32c19fe5481b0c28eb4b47367c762805
/usr/lib/.build-id/55
/usr/lib/.build-id/55/5b23dabafb8b46f6f15cb20926a7787df9c87f
/usr/lib/.build-id/58
/usr/lib/.build-id/58/7f047ea2e3e0833b89e55ddb30991e8c9574b8
/usr/lib/.build-id/5e
/usr/lib/.build-id/5e/7fe34edfeaa99263f91693a09a528b8ff45f8a
/usr/lib/.build-id/5f
/usr/lib/.build-id/5f/5799ce11e7ab66dcdf54ea594d0aa40ca77a43
/usr/lib/.build-id/61
/usr/lib/.build-id/61/58baf286171604b4ba3feed4d69fe99c656ae2
/usr/lib/.build-id/70
/usr/lib/.build-id/70/97900877cf52465fd48b130e19f495ee6e98e5
/usr/lib/.build-id/70/9eb7c668490c6461541acc3c2402386ee5831c
/usr/lib/.build-id/75
/usr/lib/.build-id/75/770dbff042c8f3fb564b45105ff6e7b686e7a8
/usr/lib/.build-id/79
/usr/lib/.build-id/79/e1e4838339b147e81605b8d695fbd3854c6273
/usr/lib/.build-id/84
/usr/lib/.build-id/84/74a94affd8c9fd758b4eb6de0471cffcb121bf
/usr/lib/.build-id/8a
/usr/lib/.build-id/8a/e362bb558da1ddeb745b0d9d9655886272d587
/usr/lib/.build-id/98
/usr/lib/.build-id/98/103222a8e6bfbef68c9ca9b750e121cc5f0b44
/usr/lib/.build-id/9d
/usr/lib/.build-id/9d/30dd726706d39309675b0095b89fe6100c87fb
/usr/lib/.build-id/9e
/usr/lib/.build-id/9e/78a64bf90fe620a13184fbecb1e44977bd7e41
/usr/lib/.build-id/a2
/usr/lib/.build-id/a2/2cf4961c9a27537777718996571b030df3095c
/usr/lib/.build-id/ab
/usr/lib/.build-id/ab/6c5a5c8fc07f71c9391ed80ca71149f58c1ef2
/usr/lib/.build-id/ac
/usr/lib/.build-id/ac/e9028712d2814d87eabdd2444b073e52974163
/usr/lib/.build-id/ad
/usr/lib/.build-id/ad/d4ad47854c2ef5b60eaa7621139485a7cf73ee
/usr/lib/.build-id/af
/usr/lib/.build-id/af/b7ab733e65462c4173c7f357e2261c62b44351
/usr/lib/.build-id/b2
/usr/lib/.build-id/b2/070cef0fe9046cd70a9b23049f3e80cfedfc10
/usr/lib/.build-id/bb
/usr/lib/.build-id/bb/8cd04454aa6de360cb9161e6b2ef7862e7bd96
/usr/lib/.build-id/bb/e41470153a3d720758de43c06eca0a46b06475
/usr/lib/.build-id/bc
/usr/lib/.build-id/bc/2c2ec0fc2e4464e9de596c43f615a835aba9f0
/usr/lib/.build-id/bd
/usr/lib/.build-id/bd/910d8a652381c5e5499ba02a6fd212779b9991
/usr/lib/.build-id/be
/usr/lib/.build-id/be/18e5bb9a488efb5ac1d92be4a2e62b33560174
/usr/lib/.build-id/be/f24d7318d6d6eaf5a7337e9aae4d57c68096fc
/usr/lib/.build-id/c6
/usr/lib/.build-id/c6/adcacd1e1e0eea6f2a504b2b3b3302e3a69ada
/usr/lib/.build-id/c8
/usr/lib/.build-id/c8/2813c8f7d674c51ac9c8cfd2705548bd6044c9
/usr/lib/.build-id/cb
/usr/lib/.build-id/cb/c07385b322560ef38006b8b444b18ac9427761
/usr/lib/.build-id/de
/usr/lib/.build-id/de/094fc8cf27e5d22c9300c07f4183b2c33ec0b8
/usr/lib/.build-id/e1
/usr/lib/.build-id/e1/7b4df763aad373b757821049ed24dae252ef46
/usr/lib/.build-id/e2
/usr/lib/.build-id/e2/f42c89c81e9c5b64c4f2f41c37a253a8cdbcb6
/usr/lib/.build-id/e7
/usr/lib/.build-id/e7/7b068e2bc8c50815ab283dbcc245f2e517c0dd
/usr/lib/.build-id/eb
/usr/lib/.build-id/eb/40f8b48790bc26d717d97a950c7f494b6cf409
/usr/lib/.build-id/f2
/usr/lib/.build-id/f2/8a611ebf4ae4804764aea8bf0d91ed500b952e
/usr/lib/.build-id/f5
/usr/lib/.build-id/f5/32ca5916c7f840e884b12d3ea0d85449127b32
/usr/lib/.build-id/f5/c65f67ce879af69858e926cbc76a030ef3531d
/usr/lib/.build-id/fb
/usr/lib/.build-id/fb/0b58164a23d6ccb7ca02d353c9a830b98b5244
/usr/lib/.build-id/fe
/usr/lib/.build-id/fe/a1abd026de3d5b80a5017f3e15cfd9734ba679
/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/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/hopcroft.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/rocq_package.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__Ftactic.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__RewriteStratAst.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__Tac2subst.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2syn.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/ssreflect_rewrite
/usr/lib64/ocaml/rocq-runtime/plugins/ssreflect_rewrite/ssreflect_rewrite_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/ssreflect_rewrite/ssreflect_rewrite_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ssreflect_rewrite/ssreflect_rewrite_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/ssreflect_rewrite/ssreflect_rewrite_plugin__Ssrrewrite.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/genConstr.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/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_diffs.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/vernacgoal.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, Mon Sep 28 00:57:02 2026