rocq-runtime-9.3.0-1.fc44 RPM for s390x

From Fedora 44 updates for s390x / Packages / 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(s390-64)
• tex(coqdoc.sty)

Requires

• /usr/bin/ocamlrun
• /usr/bin/python3
• ld64.so.1()(64bit)
• ld64.so.1(GLIBC_2.3)(64bit)
• libc.so.6()(64bit)
• libc.so.6(GLIBC_2.10)(64bit)
• libc.so.6(GLIBC_2.11)(64bit)
• libc.so.6(GLIBC_2.15)(64bit)
• libc.so.6(GLIBC_2.16)(64bit)
• libc.so.6(GLIBC_2.17)(64bit)
• libc.so.6(GLIBC_2.2)(64bit)
• libc.so.6(GLIBC_2.25)(64bit)
• libc.so.6(GLIBC_2.28)(64bit)
• libc.so.6(GLIBC_2.3)(64bit)
• libc.so.6(GLIBC_2.3.2)(64bit)
• libc.so.6(GLIBC_2.3.4)(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.4)(64bit)
• libc.so.6(GLIBC_2.42)(64bit)
• libc.so.6(GLIBC_2.6)(64bit)
• libc.so.6(GLIBC_2.9)(64bit)
• libgmp.so.10()(64bit)
• libm.so.6()(64bit)
• libm.so.6(GLIBC_2.2)(64bit)
• libm.so.6(GLIBC_2.29)(64bit)
• libm.so.6(GLIBC_2.35)(64bit)
• libm.so.6(GLIBC_2.38)(64bit)
• ocaml(Abbreviation) = 9cf44fb6ff2d20c7eccbbaa9e96863ad
• ocaml(Abstract) = 1fe709c5d435b69f744398bbbb9150f4
• ocaml(AcyclicGraph) = b16f2d994cdb319ba7f964f444cf51d8
• ocaml(AllScheme) = 035387b97096eb56ec27f2a2154c0c97
• ocaml(Arguments_renaming) = 1dd0376a5fe27100a7d8ff9e3c5ca7bd
• ocaml(Assumptions) = 7e015016bb781dff84facc859b58f49a
• ocaml(Asttypes) = e507ef6e691c55af686b09bd398e52fe
• ocaml(AsyncTaskQueue) = c2c76e34bd65fad7f95570f1f5d3810d
• ocaml(Attributes) = af7f0b62b9b5f9713a05ffbd3de2cada
• ocaml(Auto) = 1fdca9ac9970b82ee88d60ca82f042e7
• ocaml(Auto_ind_decl) = a2bfb7f4e025eec4432fef709823ff72
• ocaml(Autorewrite) = c591160914bfbf0d70293ce954dfad28
• ocaml(Aux_file) = d9640d620fbe5a0ef45e1d4815f5f435
• ocaml(Big_int_Z) = d6cb9e1c54060ad10e28f7ba86ae266a
• ocaml(Boot) = c10d1826ec03550bc542cef705e8a113
• ocaml(Boot__Env) = 6761f5c82d57f92b184c43064da1a433
• ocaml(Boot__Path) = db34ea431173f9ae4c5adf48124456ea
• ocaml(Boot__Usage) = 38a803d96d64d1260891320e63e0a08b
• ocaml(Boot__Util) = 7ba9a906ee0085778ce0b96e0afcfde3
• ocaml(Btauto_plugin) = 021f47edaa1c3dcd96029f3b21dd4a96
• ocaml(Btauto_plugin__Refl_btauto) = be5da81a805eef6699b550beda20b54e
• ocaml(Btermdn) = 8146f6b770e8db4c9e674d8e101ac18c
• ocaml(Build_path_prefix_map) = e0f5cdd3ea76275f8c562bce411ee08b
• ocaml(CArray) = a2e455be7013ec529edc7deeb9c88dcd
• ocaml(CAst) = 5db7eec6e137b01f88931386bce5df29
• ocaml(CClosure) = 444b7b36f608b852bb62340375fda73b
• ocaml(CDebug) = 7f2e1a015766edd1310ed03bf997b5bf
• ocaml(CEphemeron) = 7cae4867455538660558bdff12463859
• ocaml(CErrors) = bd91d2bb56c786c56b4cda125dafe139
• ocaml(CLexer) = 7ccd1beb5d55a32e3ff30248d4902e15
• ocaml(CList) = 9a2830c6a7f1e5138c25f4567f0e7335
• ocaml(CMap) = 5f7c442caf34e8f6d203e5efc874beae
• ocaml(CObj) = 2adb6c04a1dd1ddff801b115e6e3dfd6
• ocaml(CPrimitives) = 15b90926f6b8cfb6e5a3321d1aff45e4
• ocaml(CSet) = 92792c4e2644daca0e24011d944d1afa
• ocaml(CSig) = 7b8c866b8f6c445149b9b6a78c95825c
• ocaml(CString) = b82669584282e80562f014e128422312
• ocaml(CThread) = c04f6295803e585cd503bd0078828dee
• ocaml(CUnix) = f6850de84f62fe0043b8f44ae8b780c8
• ocaml(CWarnings) = 721884d23b5ee7aed4350427cb5784ca
• ocaml(CamlinternalFormat) = 70bcbb90ec668384a2248434bb2eb1ab
• ocaml(CamlinternalFormatBasics) = bb23651112c1e05c61498d902472830d
• ocaml(CamlinternalLazy) = 321f83e197d23ef3129f66a139b9829f
• ocaml(CamlinternalMod) = 091e0f55942111b1b8c378809123a052
• ocaml(Canonical) = f3478e74c5185f99240b1263e076c327
• ocaml(Cases) = bbd86b48051633ed3d9e9ba9bb6f279b
• ocaml(Cbn) = fd99d700926cf5458b8033afe0856ee5
• ocaml(Cbv) = 3de2249c11fcc7c4a9c700604649f799
• ocaml(Cc_core_plugin) = 7221186ffe2b1d4feeb3b619e5518b5b
• ocaml(Cc_core_plugin__Ccalgo) = 4d93c09ce8a0c7fd90859e8ad2cdad35
• ocaml(Cc_core_plugin__Ccprojectability) = c4289030d1c36c36e8d79daac523018a
• ocaml(Cc_core_plugin__Ccproof) = d2eabaaf196b6e773f81789e36f1ecbe
• ocaml(Cc_core_plugin__Cctac) = aad06ee1826dc47d5338041121b4dbd6
• ocaml(Cc_plugin) = ace7197075e417f45053eabc4ecb5148
• ocaml(Ccompile) = 848d594b5b3157579a921350c6c6c085
• ocaml(Class_tactics) = 5d6d2c4f82a04be229a64f18d80680e3
• ocaml(Classes) = 7d602543316b57521526f1f0fdd56ec9
• ocaml(Clenv) = 4a469e5c8eee13e13d72186f075e0e93
• ocaml(Clflags) = 1e5696f0c01b2a0894699729b9bf930a
• ocaml(Cmi_format) = af4e87c82d2bb018b25d798368662790
• ocaml(Coercion) = c61ee923c72a3fd1a83b27a5db418b56
• ocaml(Coercionops) = 6466349f8b87c7029eac8b5a0fd61f88
• ocaml(Colors) = f64d1bac25e83f529dca98fcd2183c24
• ocaml(ComArguments) = c1a69f04e56d4502c578d0273bc68fa0
• ocaml(ComAssumption) = 0a1c66c3a76438698d666126c4f3cd7c
• ocaml(ComCoercion) = 4d9e1b6d251790ccfa5e4b0a3d1ed253
• ocaml(ComDefinition) = 7b2219cebc82d672375cb6eeabf4b0f8
• ocaml(ComExtraDeps) = 52ee313e0b138b852182cecd6fee3450
• ocaml(ComFixpoint) = cc3cb436ef1e6ecb5df7f29e29e1bb1f
• ocaml(ComHints) = 1c0fab03af327b097ac8633f77c89972
• ocaml(ComInductive) = e362d7ce140df965d0a04464d56390b1
• ocaml(ComPrimitive) = 88f8aff5bb1fc9aa5ec3a37e54b76fa6
• ocaml(ComRewriteRule) = d733cbe58c03e372bebc6bcf5bea34a0
• ocaml(ComSearch) = 67fd9a54c25c49ccf25f60c52d0d27bd
• ocaml(ComTactic) = 8ca732406b6e1f9c10d7e3773f3a8eee
• ocaml(Combinators) = 22fbdfa96a350dd3e0ee046f87c197b3
• ocaml(Common_compile) = 8b9f1ab2504e41a1a73402d8199ec792
• ocaml(Compenv) = c5b2a25f63b81e35600f80ebdc868b4b
• ocaml(Constant_typing) = 0db4a9797673fb7d5043deee2ed7e3f0
• ocaml(Constr) = 4b32f93115f2d88db9c87127d75769b2
• ocaml(Constr_matching) = 41aac11572ea8b00c96e6d9c26e01aa5
• ocaml(Constrexpr) = bc83f2525098ba20b8418bd81e5caad4
• ocaml(Constrexpr_ops) = 51f64f68443c51a622a0e20273f493de
• ocaml(Constrextern) = 6bf0e9fbed50b120aad2dd5eadc34cd3
• ocaml(Constrintern) = 7bd8e82f911ab4b3a646b5525c9ed1c3
• ocaml(Context) = 1900cd050b654b69ef102eb709c88caa
• ocaml(Contradiction) = 8e034f9e7d0046332456a0b0a32d0533
• ocaml(Control) = da458f2d7dfca053cc19f9408a6f4932
• ocaml(Conv_oracle) = 2a21865d41f4f5895d52892e18b24284
• ocaml(Conversion) = 954b0a4fd8fb4663556d723d3d4b5453
• ocaml(Cooking) = fb0ba5e9e1400aedca409577e28e1df5
• ocaml(CoqProject_file) = 4ca7cef8431b02e302d0b59749f5bd5c
• ocaml(Coq_checklib) = 2baf09a1c451962aa0d821a3fdd11db5
• ocaml(Coq_checklib__Analyze) = 83361539cce55e3551b4cf869801cbcf
• ocaml(Coq_checklib__CheckFlags) = 818722f884c0349a836e17cb47531d59
• ocaml(Coq_checklib__CheckInductive) = c3469410f15d895461abbe70d1ac92a2
• ocaml(Coq_checklib__CheckLibrary) = a0e3431075358c60eba8e86dfb321367
• ocaml(Coq_checklib__Check_stat) = 9fcf18b84a4c3cff5c374ac0383f5f22
• ocaml(Coq_checklib__Mod_checking) = c2c35d746e4882c16491768619d2e38c
• ocaml(Coq_checklib__Safe_checking) = 0864facc432b5acdc74a454e2e48aaac
• ocaml(Coq_checklib__Validate) = ad1a44e6c3fd2bd40f5ee2efa483b7c8
• ocaml(Coq_checklib__Values) = 0e0d1b05633b37f4cda113582947eb1a
• ocaml(Coq_config) = e30efdf14dacb1c54a655e581ffcdb61
• ocaml(Coqargs) = ecfb91a850101eb97dc81732ae84e86d
• ocaml(Coqcargs) = 43aba1cb34ed646a89726402fa8a1def
• ocaml(Coqdeplib) = 9691a482b51456c82d6ef9fd3de101f6
• ocaml(Coqdeplib__Args) = 0b99f39470466d526ec761cc17c94e50
• ocaml(Coqdeplib__Common) = 207121249d8528c3517737b72e168dfd
• ocaml(Coqdeplib__Dep_info) = 89c764c25108ff3133b41039e41e4912
• ocaml(Coqdeplib__Error) = 49bebf4041d6ef12512330d49c2f3543
• ocaml(Coqdeplib__File_util) = 4d2dda781d192a22777292eefa85eaf2
• ocaml(Coqdeplib__Fl) = 2a6a849b34ab36eb546766001bb63e20
• ocaml(Coqdeplib__Lexer) = 1ff75d9dd2278ec587cd211413707a3b
• ocaml(Coqdeplib__Loadpath) = 705b588e4a420b024c81d31c8fdc7c70
• ocaml(Coqdeplib__Makefile) = a654c740c362576d61ce0b4b924453eb
• ocaml(Coqinit) = bdc3c413f67b3f8a4dfb0a5134242628
• ocaml(Coqloadpath) = cfdcf87c77a8825a6eed649a39337559
• ocaml(Coqloop) = 7d1ba6f0887b4f9e0f56e40eb6f94221
• ocaml(Coqrc) = 45ccec5688f862bdaed8c239b882e172
• ocaml(Coqtop) = 2906ce1694d974148389c20f27a55c57
• ocaml(CoqworkmgrApi) = bf9291ab65d50704790e0ce2f6f3b962
• ocaml(DAst) = 814e2ae502b9a860936b4fbcb1e0d869
• ocaml(Dag) = 7e85dc3bd26aa26d7f1582df587d5618
• ocaml(Data_types) = 9f178cf8e1e58dacbc1ab559802bb5d5
• ocaml(DebugHook) = 4a0b419408abdbaad3466f51bd079051
• ocaml(Declarations) = 2020f6303d6660f8ff9b3c47303badf5
• ocaml(Declare) = 66e34416d03bb41240f40411ed38e81a
• ocaml(DeclareInd) = c7ea03c5ce4ce3c83b15a3e51bdf6e80
• ocaml(DeclareScheme) = f8ede817e0c7422ec27abd1a481c761c
• ocaml(DeclareUniv) = d912bc02bddeb432bfe9e5919c98bcab
• ocaml(Declaremods) = f75e6a72877ca0c4ae4bc71a57a9e3d8
• ocaml(Declareops) = c40181dcf34b9b34ea45e8662e0f82d9
• ocaml(Decls) = 4e031815a7e0c34694359deff5bb90ae
• ocaml(Deprecation) = dddaef8bc50838511419e34c165a260f
• ocaml(Derive_plugin) = cfa1f7052a4b7c1f11cf5d3c30e00cf2
• ocaml(Derive_plugin__Derive) = 605ddc573a9a8cedfe36f44b7ace8bf3
• ocaml(Detyping) = 4714ad9a423af755605075f48571c4ca
• ocaml(Diff2) = 8940429ed83ad199f81a27ff5df3fadc
• ocaml(Discharge) = d6c4fffdd90748bd0082030142951e02
• ocaml(Dn) = f8f3a88ab1ade13c85ae0378e1148817
• ocaml(Dumpglob) = a0c93da5700848011e7baca74ab0e5c1
• ocaml(Dyn) = 2cba2a29b3efe66c586cb9a0bf17d01a
• ocaml(Dynlink) = 08e1461841151b2dfdeeb2b217719fea
• ocaml(EClause) = 77c469bd20f07e04401f51970983f521
• ocaml(EConstr) = d30d3c7156c9819550dc84fd74a771ca
• ocaml(Eauto) = 5ea23617b8e5c516d979388841956039
• ocaml(Egramml) = d92454637f8c2118916f310d4c99a4ca
• ocaml(Egramrocq) = 95f9d9018e090f76d6138997e4adb2ee
• ocaml(Elim) = 4826af12d7e8519a5911ed8129d90983
• ocaml(Elimschemes) = 9406ef98f327b85e4e8f9cf53640895f
• ocaml(Entries) = f8df4ffa8ac955221d975721898b67da
• ocaml(Env) = 0cdf66ea216efe371c58a7976afe2075
• ocaml(Envars) = fc8d9acafb03dbdf0cf9bd347b88c21f
• ocaml(Environ) = 7b39e6e092f764aa971167c078961bfc
• ocaml(Eqdecide) = a3b731841197ccffa259f526f5ebbeed
• ocaml(Eqschemes) = ff6a4ff1ecfd532428bcdd797cd1716e
• ocaml(Equality) = 506452f66b3278db2452d04a02365250
• ocaml(Esubst) = 5a8ccc5153d1630a5ca9969e8efa9f01
• ocaml(Evaluable) = a4a1c357fe2461c80935fd620c6f3570
• ocaml(Evar) = d52407c6665e1ecd26d74ef23f4f2607
• ocaml(Evar_kinds) = c9920c5b07134fcb75eae45d4e1e7f91
• ocaml(Evar_tactics) = f0b4f9b52888ff343b1098741f1e9758
• ocaml(Evarconv) = 4cc22e25473f189f163843f77c36c84c
• ocaml(Evardefine) = 31a546efe2ada98d9363eb76e036cec5
• ocaml(Evarnames) = a146e7ecde52b78338b22b29e5515ed0
• ocaml(Evarsolve) = 989f4ee98203f1319f7b25904d560363
• ocaml(Evarutil) = fad47dc7e62b6f1f3654ef3ad163c602
• ocaml(Evd) = 708350d83a0770f5c614eb3ffb4d2894
• ocaml(Exninfo) = 95e7f938070548b5b5d750588295e6db
• ocaml(Extend) = 86ba3c22a704332b7877af311d96820e
• ocaml(Extraction_plugin) = 45385a433336b20d3b91e013e59f2671
• ocaml(Extraction_plugin__Common) = 4b563031277877ceb467bdc4aa00342c
• ocaml(Extraction_plugin__Extract_env) = 8097410498d2641135b112f2cf857b41
• ocaml(Extraction_plugin__Extraction) = 81dd183882c4d6b6060f9ae6234d7032
• ocaml(Extraction_plugin__Haskell) = 19b24a984b9a2d8103e00344669679ed
• ocaml(Extraction_plugin__Json) = 3f055245aee6263e6a57d0024e67f967
• ocaml(Extraction_plugin__Miniml) = 46b56a6a831e61daece9574e1e1d7e8e
• ocaml(Extraction_plugin__Mlutil) = a173bc88d4f22b14822dbfca7b830be4
• ocaml(Extraction_plugin__Modutil) = 74a116de51e13b3705c381d237d79e27
• ocaml(Extraction_plugin__Ocaml) = fc58dcd2d786ceb96993f142489a8498
• ocaml(Extraction_plugin__Scheme) = 3ecc9441c911e6c2cdc902aaa367b1ea
• ocaml(Extraction_plugin__Table) = 1eea9193d2464dae583e0dc1697636bc
• ocaml(Feedback) = 24f1dc234e7f470029126736ab45af56
• ocaml(Find_subterm) = 7edaf2da0bd744227d872e4bed7810d5
• ocaml(Findlib) = a5fc3db70ae71cda44eb0da93e094eb2
• ocaml(Firstorder_core_plugin) = 117b378e702191a4f2b1921366b5a21f
• ocaml(Firstorder_core_plugin__Formula) = 40abea18a8ce77fce7b7a9d20f482fdd
• ocaml(Firstorder_core_plugin__Ground) = d7e92442c3eb83be26f4ea75e1aeb02d
• ocaml(Firstorder_core_plugin__Instances) = 604cf266a5446c1b60c68314c5378c62
• ocaml(Firstorder_core_plugin__Rules) = 440245575dc830cbb4a97e493d667b07
• ocaml(Firstorder_core_plugin__Sequent) = 1a7668611c380ee0caf473e0fd88fb9a
• ocaml(Firstorder_core_plugin__Unify) = 81f6f41e436e290c2c4bdb5705c6f95f
• ocaml(Firstorder_plugin) = de43944fb21b3ca4a0fdc2c59c4173d1
• ocaml(FixTactics) = d58162c9092ee425ea3c0f904af63c74
• ocaml(Fl_metascanner) = f2833d59fc6fb9013774ad16022f6e1f
• ocaml(Fl_metatoken) = c52aa6baf9d82887fc926a04bacae69b
• ocaml(Fl_package_base) = b49943184674c704462363ed948c27f6
• ocaml(Flags) = b28ae67b193d650420c229dda08b0685
• ocaml(Float64) = e3af59c461d447770a9513d585363662
• ocaml(Float64_common) = 8bb3514a86d9aa53eca574fb5a08dba4
• ocaml(Format_doc) = e9bc76d69e0a38952eeb83c757a95d18
• ocaml(Funind_plugin) = 478d36ea9a949ae615ecf6f234e67878
• ocaml(Funind_plugin__Functional_principles_proofs) = f911c7fc057e587d771499763ed43f63
• ocaml(Funind_plugin__Functional_principles_types) = 2910c9598155e33b5bb508a6db066d81
• ocaml(Funind_plugin__Gen_principle) = d9542c2bfcb0133318d88d2788bd6b2a
• ocaml(Funind_plugin__Glob_term_to_relation) = 33cb02e69987b6a6aac938d76c158f4a
• ocaml(Funind_plugin__Glob_termops) = 547c9bac19cb41aa6279f1bf4c735e7a
• ocaml(Funind_plugin__Indfun) = 43021d108bc532fe2dfc4c0d3cbf2b85
• ocaml(Funind_plugin__Indfun_common) = 9e840b033c12e908a548dc4cfc972e71
• ocaml(Funind_plugin__Invfun) = eb706e966157c55e20bafc31e46c2f66
• ocaml(Funind_plugin__Recdef) = 7eb977ec8f99b78fe3e3a0654c19d036
• ocaml(Future) = 0834bf495a97d13fe3d43454740f6994
• ocaml(G_constr) = c89fe8462a50f674dc6bfeb21c37276a
• ocaml(G_proofs) = 59615fe4ce7af040c9c86f2b1b621001
• ocaml(G_redexpr) = bcedd738705776f5451470c348e71b4a
• ocaml(G_toplevel) = 7ae035ccb0eb11de7ba1e6c72bcf9d2f
• ocaml(G_vernac) = f9bfeea6e620cb10afaeb85c3cee041e
• ocaml(GenConstr) = ade9d441c6f261f78afea73007e2e1c6
• ocaml(Genarg) = 498c0195787ed32e112234c83a1310fc
• ocaml(Generalize) = 6e05cef191b674d950d6b88a70a8df81
• ocaml(Genintern) = ac8421dc97e31aa8ebd785cb56585dfa
• ocaml(Geninterp) = bfc0b896ec982e0404832dc051086d25
• ocaml(Genlambda) = 79459e62f73db29d5c369653dd9f2e18
• ocaml(Genprint) = e9f80fd9c5f7a1b05e1d072f7dc29368
• ocaml(Genredexpr) = acfd525e6ebb2b7137f047156d3bc921
• ocaml(Gensubst) = 43087f0bf7ca489173224593e0ace222
• ocaml(Gentactic) = a5ebe4efa650f0091eeee8c73eff6aee
• ocaml(GlobEnv) = 50d957dd29034d70112a2e80042b1210
• ocaml(Glob_ops) = 0a67d920a7e681863e07e2c5bc5da3fa
• ocaml(Glob_term) = 8a974a332a0a8fa6265703c34f0054b1
• ocaml(Global) = 1c849299ceabe6e95f68af28e2e6d2ee
• ocaml(Globnames) = be86d940873beef0b4d921f7c00b4a04
• ocaml(Goal_select) = dd33b16e4221bd23aa2f8bdb2f7ffe10
• ocaml(Goptions) = e9709690f9d527f52858d528cad74be3
• ocaml(Gramlib) = ae39fd0bb86764a48d691d550ddeb9d2
• ocaml(Gramlib__Gramext) = e49c510afe5490ea4e64d84dc46dd6a9
• ocaml(Gramlib__Grammar) = 76ee0883edbed60b2101f5da2fde5699
• ocaml(Gramlib__LStream) = 0a238c94060a3fa93fec47a9cd84dd48
• ocaml(Gramlib__Plexing) = 2d80ffbe42fb9df48d4f2092176ee5cd
• ocaml(Gramlib__Stream) = 4764be9973f4964bc0d6417ffa24b77b
• ocaml(HConstr) = 98e7bf62549a35f56cf9d4d6da3aff2d
• ocaml(HMap) = c40f093b7509a73d1434b94d6d0a2c70
• ocaml(Hashcons) = d9da5b4a5d48cabeddb2878692bf1fce
• ocaml(Hashset) = f2a941d55c9ded6be6c8f9026ec7a921
• ocaml(Heads) = 22765cb2c33609d56309cf0d27a38b84
• ocaml(Heap) = 4f083d427cb30e39d3d786a1cf292eaa
• ocaml(Himsg) = d24559c5346e170d28caded0b1697dd5
• ocaml(Hints) = e560e17e1fdbb9c66caa8352b0adce3d
• ocaml(Hipattern) = eb0da5e8126d401d54423090a97fe54f
• ocaml(Hook) = f86461414dc1ef72fcb0b45bed7f95ce
• ocaml(Hopcroft) = 3e4c6a5ab4c18b197dea1634b3895510
• ocaml(IStream) = 2da469b3f4ce192ed5a5dc8fab75ced2
• ocaml(Ident) = 61cbd919c8f6ef60ced7ecbe7fb6faf5
• ocaml(Identifiable) = 8621bc2814d3f193b9cab59619693489
• ocaml(Impargs) = 460cfd0d114bea7d0e992bfc61af00d5
• ocaml(Implicit_quantifiers) = 1adc5d8dae5c38ad82e914903d4098c2
• ocaml(IndTyping) = c6ec814c58f1be580d28f3768f60780d
• ocaml(Ind_tables) = 4f3ed2cc4accc519bf335a557ebf74ef
• ocaml(Indrec) = 1cf00e6f331c5bce9563d7845ee369c7
• ocaml(Indschemes) = 4342bef9bd7db3fecf6ed8f4cd65df52
• ocaml(Indtypes) = 34a160624ccafd12c1752d6459f53511
• ocaml(Induction) = 1a303680cac5f811546ee9173ce8fa25
• ocaml(Inductive) = 1bb30fe2335e1472c65154200983f0f5
• ocaml(Inductiveops) = 7d7927bc8ed0c67f3298e340c4b371ce
• ocaml(InferCumulativity) = 86a7e6a89279ae1a0fb54c684bfcd4f8
• ocaml(Instr) = 82b17b769bc0349c36beeb461e0ca02d
• ocaml(Int) = 19d2092c60e41becce6e12e7b808903a
• ocaml(Inv) = 7c2e50801c41a7f00cc6d02124f11f77
• ocaml(Keys) = 7af6000f112b260d3bf12f17de9b69b6
• ocaml(Lib) = 685e91c8b99f387480691839454cab35
• ocaml(LibBinding) = f2d830146334b92449a41b28cbe51226
• ocaml(Libnames) = 327c70c31cd420e9f4a1798e50adb4d5
• ocaml(Libobject) = a7b1be6b3986e3df683d849d6495ff37
• ocaml(Library) = 6a2f7f9357ac2c31cdcc6cece7bdd9b0
• ocaml(Library_info) = d2e990d9a75dd3857f3094388dfc3184
• ocaml(Load) = 58b0a34d7edbf60c52429b2ec0b1fd53
• ocaml(Load_path) = 311833dc50b7f0117c7580122e8b521b
• ocaml(Loadpath) = 0f7bea21e6abc54d328dee205dfef00d
• ocaml(Loc) = a935873bc45359e4ffcfc913b4aa3fdf
• ocaml(Locality) = 0b0715af09ba64e4cca27ca908696be5
• ocaml(Location) = 1f3b4a14027aa1c3d06755358fe40ab9
• ocaml(Locus) = 08f7d33dc6671585d6fb590a4605c05a
• ocaml(Locusops) = 67bd7a717f4fee694468f156825596e7
• ocaml(Logic) = 2a733130e47a3909068f860bde5280c1
• ocaml(Logic_monad) = 1c372699032ff5073b5654824c9b470b
• ocaml(Longident) = 4fec6bb94016657f43f91bd096f27b38
• ocaml(Ltac2_ltac1_plugin) = f36ee64104bf7571ca1347ac2369081a
• ocaml(Ltac2_ltac1_plugin__Tac2quote_ltac1) = af09c13f07a970ae407f38cf12f0ca85
• ocaml(Ltac2_plugin) = 434753973ab412a3a403c368d93a0f7c
• ocaml(Ltac2_plugin__G_ltac2) = 049bd7c0a9710687aabd9e613c938144
• ocaml(Ltac2_plugin__Tac2bt) = 1dbadd42d44107adc51a8cdd21ff64c1
• ocaml(Ltac2_plugin__Tac2core) = 9bef11cbd6d9df2144213243c45774ac
• ocaml(Ltac2_plugin__Tac2dyn) = 40861397f451347a7ed9d947f70da943
• ocaml(Ltac2_plugin__Tac2entries) = 4f8fac90e8a7220991648d388fa52222
• ocaml(Ltac2_plugin__Tac2env) = 2cdfd8cf38d21cf203a66c11ba9cbab6
• ocaml(Ltac2_plugin__Tac2expr) = d2d779be2e863c9225f1a556a0a18d63
• ocaml(Ltac2_plugin__Tac2externals) = b236e66483e704c39d2e97c00d072908
• ocaml(Ltac2_plugin__Tac2extffi) = 52d3cf43402e6e4bee646a8a2084e6be
• ocaml(Ltac2_plugin__Tac2ffi) = 4b4f9195d8e0f0511900b4ef18f18155
• ocaml(Ltac2_plugin__Tac2intern) = 0c9c6039ad3d0e4f38d92e356230bcb9
• ocaml(Ltac2_plugin__Tac2interp) = e5b459abda92d9af88e59ea356f27104
• ocaml(Ltac2_plugin__Tac2match) = 040799b2006f0369e7d5df3fcd550f11
• ocaml(Ltac2_plugin__Tac2print) = 941f4408101b7021ad6f4dede3cfab66
• ocaml(Ltac2_plugin__Tac2qexpr) = f72c5ac6b96beeadea6cbb5139d5baa4
• ocaml(Ltac2_plugin__Tac2quote) = 03fe4ae3345162f0850bb922fff8c5c9
• ocaml(Ltac2_plugin__Tac2stdlib) = d3183510898030a9000ad4e56eb30504
• ocaml(Ltac2_plugin__Tac2subst) = 4209e7fe0f6c1ee5076f2baf9360410a
• ocaml(Ltac2_plugin__Tac2syn) = acd16c71ee71516f88b078167b9f8226
• ocaml(Ltac2_plugin__Tac2tactics) = ddddee553ef288e8429cc16e00e274c5
• ocaml(Ltac2_plugin__Tac2types) = b97ea111d1a9b46adcfff65e725f487c
• ocaml(Ltac2_plugin__Tac2typing_env) = 4b59c9f053cc38f1187982a982b74996
• ocaml(Ltac2_plugin__Tac2val) = 836d15f344536b96e47f05c3b856dd3c
• ocaml(Ltac_plugin) = 594e2c148e06c9c50ba4c5c240f1ece9
• ocaml(Ltac_plugin__ComRewrite) = 13c449be2613d279d0b7cd5b20e5c0c1
• ocaml(Ltac_plugin__Extraargs) = 75b56b368c3e887ba35d57a1980eafd3
• ocaml(Ltac_plugin__Ftactic) = 14feab98dfdf89804829b0789f2710b4
• ocaml(Ltac_plugin__G_ltac) = 0312c534aeae8d8b1dc2cf34387209bf
• ocaml(Ltac_plugin__Internals) = e54f14ead27f7c405e0d416ee91e5264
• ocaml(Ltac_plugin__Leminv) = 87c79782b2a6aa3a6754a0f5b3618bd8
• ocaml(Ltac_plugin__Pltac) = 76fad7a905bbb8ec46fd97cbf9bf841a
• ocaml(Ltac_plugin__Pptactic) = 23525af700c50c24884c1230a4746f1c
• ocaml(Ltac_plugin__RewriteStratAst) = bbc98d1d7ef76ece452845d827e466b1
• ocaml(Ltac_plugin__Tacarg) = 30c7b1483e25baf1df936fcef3c09493
• ocaml(Ltac_plugin__Taccoerce) = 040a4831b81209ebe1ea0638d71c46a5
• ocaml(Ltac_plugin__Tacentries) = e4c94ce32b9dda91b288f77212743878
• ocaml(Ltac_plugin__Tacenv) = 5d388e3d2986e3501806e124a9ca4936
• ocaml(Ltac_plugin__Tacexpr) = a5ec6f5145277b28dc36b6a0cb141c53
• ocaml(Ltac_plugin__Tacintern) = e63f5a13d0e494985db2f0d40eb3a3e2
• ocaml(Ltac_plugin__Tacinterp) = 969bf4ffa07cc4c2a6b90ee343294ced
• ocaml(Ltac_plugin__Tacsubst) = d684081c0c323f25356974708431356c
• ocaml(Ltac_plugin__Tactic_debug) = 244ac445198e25bc74d35296ff0ef587
• ocaml(Ltac_plugin__Tactic_matching) = acb60228199ce00a7fbe8b479e2d8b4a
• ocaml(Ltac_pretype) = 4d792867c07e9757ddb4b288be8fcfc8
• ocaml(Memprof_coq) = f9c0e2bc673e324eddc2854d46d8f0c3
• ocaml(Memtrace_init) = 767bc231aec961de2ef9b3b9c923a001
• ocaml(Metasyntax) = 2137ba5ea17d61228fe715c07fb152af
• ocaml(Micromega_core_plugin) = 7431add2f7d94df09a1d16829af126c7
• ocaml(Micromega_core_plugin__Micromega) = 71eec3b72c1bc19482934ced988a0111
• ocaml(Micromega_core_plugin__Mutils) = 885ccb1a94fd8004bbe0eab9fa71f3c4
• ocaml(Micromega_core_plugin__NumCompat) = b4521a7b0c76da1f719112cab513ab9f
• ocaml(Micromega_core_plugin__Sos_lib) = 7984dbed222b5707b22935261e97a1bf
• ocaml(Micromega_core_plugin__Sos_types) = d35f96b164748f21c9464fc982deec04
• ocaml(Micromega_plugin) = a2028cada0a4dc8d4a36ba485208ccd7
• ocaml(Micromega_plugin__Certificate) = 0ff6bce9e4c0b3e61be7ba859ff9935b
• ocaml(Micromega_plugin__Coq_micromega) = c4823b25f85230dca9998147857ee9b4
• ocaml(Micromega_plugin__Linsolve) = c6bf4a1fed428bc78c04d0870bc55dfd
• ocaml(Micromega_plugin__Persistent_cache) = 8cdec97154e15e90f3ad9f9fd6819e56
• ocaml(Micromega_plugin__Polynomial) = 45d7375512df29400a8b8721e0f09e7e
• ocaml(Micromega_plugin__Simplex) = 27248d453e731e71110165b31132dbe1
• ocaml(Micromega_plugin__Vect) = ef45c5589b09036d2b04e4e340656cc8
• ocaml(Misc) = ea5241d01e1dabb94abc602b35e56ade
• ocaml(Miscprint) = ff2e29fe33b0f5f5800904d6733c724a
• ocaml(Mltop) = 6518190cd6947e12bec33edf84f6c82e
• ocaml(Mod_declarations) = d8b404b26edd394f3623b390a4100ce6
• ocaml(Mod_subst) = d1ff8101d7df005e9ad9d04cee68e0ce
• ocaml(Mod_typing) = 4d0f9d4576def0e85a519d765b7033d7
• ocaml(Modintern) = a7a65084b2a9d351ea8c2e206d1ccfd8
• ocaml(Modops) = bf165498c8d1b5302429fdf7ec4e465e
• ocaml(Monad) = 2bde140cae2e992b633c464725202d31
• ocaml(Mutex_aux) = 84cdbad35da10d625c4ac3e57b8d5bf7
• ocaml(Namegen) = 125189bcd6ee0604bc18d10acc081e97
• ocaml(Nameops) = 84ec0915f257bf5c997891c7676c0f69
• ocaml(Names) = c8b3b494943d72f8ddc24c0fe9db7a43
• ocaml(Nametab) = f570fc361f19c57e589848d6b2d7fd62
• ocaml(Nativecode) = c2ae0ae0a9db2f2681175b99e6536918
• ocaml(Nativeconv) = adbd4d60fb6e54a28b601abe3ae56f1a
• ocaml(Nativelambda) = 3887030302268d10c1e4326abddce444
• ocaml(Nativelib) = b07981bfab0190c99593d0e8c6b29dcc
• ocaml(Nativelibrary) = a1235b6433513e1c035312e3e3d1af27
• ocaml(Nativenorm) = 0824d2819cd92eaa6f1bb22bb7b31f41
• ocaml(Nativevalues) = a323e5aa34f222ba61fe8a1820fd8aaa
• ocaml(NeList) = 7fd80b98ad74757a38fb8feefb62c9a7
• ocaml(NewProfile) = 5a97506e95dcf885f957a37328516b99
• ocaml(Notation) = 180d299c3a755aa8c5b2cfa6a524a575
• ocaml(Notation_gram) = 52cefa108dcd212e429cacde6423a4fe
• ocaml(Notation_ops) = 1dfed412323093cde55fdbd8511e75d4
• ocaml(Notation_term) = c4ab3c9605469e54845dad11d6623ea9
• ocaml(Notationextern) = 4570f8e82f62b1ba721fac6fa49e522d
• ocaml(Notgram_ops) = 07657f9e8b10747d5d9eef6a7487831e
• ocaml(Nsatz_core_plugin) = 76d693b67dd1f6dbcb3a3cbabed1fe1b
• ocaml(Nsatz_core_plugin__Ideal) = a765a74ecb2f99dd029774554da4232f
• ocaml(Nsatz_core_plugin__Nsatz) = 5912b796099d238854e569c1567f43ae
• ocaml(Nsatz_core_plugin__Polynom) = 5ab4d812d86ac931b0eb8972d82a6634
• ocaml(Nsatz_core_plugin__Utile) = 7eeebf3221ebec1b72b4d8fca48d6cb4
• ocaml(Nsatz_plugin) = 0197dfd0d488dc3a12f6db250b8ad92a
• ocaml(NumTok) = 55b439d1cb77d460bbdfc7c64e303dea
• ocaml(Number_string_notation_plugin) = 5eb1faf58a1d0e41dfb791001450f53d
• ocaml(Number_string_notation_plugin__Number_string) = c950344882abc6932b2fc958ed7a9dfd
• ocaml(ObjFile) = 62b6a93227bb08f114290c8be4a4ed19
• ocaml(Opaqueproof) = ede9db29f670bb7b810d14576c3f9fa4
• ocaml(Opaques) = 05edfc4db50834c4603c4852b8c97b74
• ocaml(Oprint) = a9904171b8bf1832d4d8d6c06ba280db
• ocaml(Option) = 41b74a99c114f72e84a33073de712a98
• ocaml(OrderedType) = 028516fb8b4953517cfa25d8cafb99fd
• ocaml(Outcometree) = 793c2f1dc6a3183ed387453b3e75c9df
• ocaml(PConstraints) = a7235fc2297f95f2eed943f80bca5519
• ocaml(Parray) = ada8d69c7b1080d775636133f4554360
• ocaml(Parsetree) = a8e773e1784913e8af2f5f83ed53a93b
• ocaml(Partac) = b5aa49e8447f56224772f0a28da09664
• ocaml(Partial_subst) = d0a694f2626cecd5d818f389ea1954a2
• ocaml(Path) = d652fc6085398c2f07e51fed32d448b8
• ocaml(Pattern) = ddb2b7d57bcb4d7ea7c43951816540b2
• ocaml(Patternops) = a62e0785853341b3ddd3a862e254b94c
• ocaml(Perf) = f9658dac7d62890a1935a30afa3f96c9
• ocaml(PolyFlags) = 8398e1086f0ee914cfcb2df7139aa845
• ocaml(PolyMap) = 7c20f956cc0034d20d7e6b409315331f
• ocaml(Pp) = a3240b9aca1401ce479dc8d56de4079e
• ocaml(Pp_diff) = ad557b5b20afce42083bda5bb86c722a
• ocaml(Ppconstr) = 092b87ca5f74aecd08d303dece2e8571
• ocaml(Ppextend) = a76b74ec1bae29786d5ad76b2d767034
• ocaml(Ppred) = 352c0c70a3c0c782341946504bc61deb
• ocaml(Pputils) = 1f31aac5df48a49c47eff1749adfc03f
• ocaml(Ppvernac) = 40744ea50b5a3d5564df932849a62e4c
• ocaml(Predicate) = 8dab2e64145accdd2f7a4ca1384b7899
• ocaml(Prettyp) = f38ac774c1dddb29b889e320de364f86
• ocaml(Pretype_errors) = af643e117cef3a7aac1136bb1095ff39
• ocaml(Pretyping) = a38ae856b1feb1b127df5d9edda10951
• ocaml(PrimNotations) = e3cac4792d62c033092d9d57eb6d8db8
• ocaml(Primitive) = 691172872c2967e1d5ca29687c0c6b3f
• ocaml(Primred) = c00298cb79e92db04b44f566028c848b
• ocaml(Printer) = 6bb58c50cd30f7dd4a081d46daf9a443
• ocaml(PrintingFlags) = 55aec1659f77ab3288d66acdcaeaacb0
• ocaml(Printmod) = 288d01dc6967c75a14f9643fd682d5a2
• ocaml(Procq) = b65ad390d7aca18f1ba6f336951ac7c7
• ocaml(Profile) = c057f723b65cb54f6058b2938cfc50a4
• ocaml(Profile_tactic) = 8a1331b604898d4d03662fee4fb93f1f
• ocaml(Program) = 1208b6992814f140d0a37720290a52ab
• ocaml(Proof) = 19bc8910fb1589e88207536802c1246e
• ocaml(Proof_bullet) = 01803c01ffc808ce0dfa5035c149f22f
• ocaml(Proof_diffs) = 7618fc19c0d27f58e69e7fef96797991
• ocaml(Proof_using) = 9e73ad1e4f805d489e53a94dae81473b
• ocaml(Proofview) = 08229016065e42b49507a997dc5d2ae0
• ocaml(Proofview_monad) = 49a32db8cb9cabd853a53b313e527c7c
• ocaml(Pstring) = 713359389f44624c284e5e4d20a80627
• ocaml(Pvernac) = 9d2ae32d2786cb955671a1737da90129
• ocaml(Q) = 8b54816595b0494f1630c558d7f2fdec
• ocaml(QGraph) = 436abb5b3c9e6b1edd07087ef7883375
• ocaml(Quickfix) = 4f57bed2673ed2bb8e36676a3c011971
• ocaml(Range) = fbf9f69cba2fc8eb5627f4b598d45179
• ocaml(RecLemmas) = 2975020e0445a987467d4813c169846a
• ocaml(Record) = f1faf037821b46d0660ae69deb86e265
• ocaml(RedFlags) = 35d7ec16682cae3c3ecc2e9400cd2143
• ocaml(Redexpr) = f85baf38975dcb6ecd3178e1df5120a0
• ocaml(Redops) = c73784922d1e1040242a48fd4e2b34f5
• ocaml(Reduction) = 1b53b182309d6cdac82853d3ea965206
• ocaml(Reductionops) = cf8edd47054722edff63fd1f04a9cec6
• ocaml(Refine) = 5aee1bb676d86336030d2bb9054a3846
• ocaml(Relevanceops) = cd651d7e5416e12d6a23132c25b16bcc
• ocaml(Reserve) = bf55e58b2e00a20a7646747b37a0c90d
• ocaml(RetrieveObl) = 43c83e2e9a2bca0829b87e7dc9773e5d
• ocaml(Retroknowledge) = 02e91ec059c218c9e8341d8c9815044b
• ocaml(Retyping) = 38cd68ca027b2ed43d5afd9a73be89f7
• ocaml(Rewrite) = b17108efbf008d188458166383a725a4
• ocaml(Ring_plugin) = cc06a0dbb7faaa0affdb43d6e81922f0
• ocaml(Ring_plugin__Ring) = 9b4cce6734d8186b348df42193cef568
• ocaml(Ring_plugin__Ring_ast) = 123c6dd03f454017aa4b5ef2475a30f1
• ocaml(Rocq_package) = fc2013b4a062642b66f2e22b3aca9fb3
• ocaml(Rocqlib) = bb5d5a7ec57c706c31117ef98f0b2317
• ocaml(Rtauto_plugin) = bef1b1a95c817e3bc0983d58fab82ec3
• ocaml(Rtauto_plugin__Proof_search) = 2395ba64feb37e1b1843d6a0063fe396
• ocaml(Rtauto_plugin__Refl_tauto) = 48766f85ac788be9c183edf26877525e
• ocaml(Rtree) = a44d0710edb5a600fa7066b5349ac7b0
• ocaml(SList) = 8f839b11093748431b165456534a4cde
• ocaml(Safe_typing) = 1f7fd4a17c92c46ecc30090f16e27d30
• ocaml(Search) = b8ccf776895f350d8e568eae68a5b0c9
• ocaml(Section) = 006d834494223d68ea94952eb5898ead
• ocaml(Segmenttree) = 3542ef972686acbb94ada459284e6bb0
• ocaml(Shape) = 639524fde7fd305260a62f1e1cefbd0a
• ocaml(Smartlocate) = 65b69bfea564a56c1e81c9c20a502133
• ocaml(Sorts) = e0492c8578636d859c66fbfd5328ead5
• ocaml(Spawn) = e58a5144e73bf5ba67b7439648199d64
• ocaml(Spawned) = 890a65f8a9a58a413fdf47cf3bea91cb
• ocaml(Ssreflect_plugin) = df2edbd9591521138483880f58a1bde5
• ocaml(Ssreflect_plugin__Ssrast) = 6b851c6e5f9eb0521012a3f05c5fc48c
• ocaml(Ssreflect_plugin__Ssrbwd) = c807f9af56c055d26e8efbfd049eea35
• ocaml(Ssreflect_plugin__Ssrcommon) = 68bc9b7135ad110c4bd1ebbb620594d6
• ocaml(Ssreflect_plugin__Ssrelim) = 8fa5b31dae409b0f3e0ca2d71d185173
• ocaml(Ssreflect_plugin__Ssrequality) = 269cdcd42b614f3f85775b13986c494a
• ocaml(Ssreflect_plugin__Ssrfwd) = f027c37b2affe1112f66e603963888df
• ocaml(Ssreflect_plugin__Ssripats) = dfcefa40baea7357d58f65423f5b8ca9
• ocaml(Ssreflect_plugin__Ssrparser) = e4eb65248b4940a28fbd0b622182c93b
• ocaml(Ssreflect_plugin__Ssrprinters) = e507c85a74816a25e05e6f096be6a2f8
• ocaml(Ssreflect_plugin__Ssrtacs) = 02d93954d41ba7ddffa085f29db7d0fa
• ocaml(Ssreflect_plugin__Ssrtacticals) = 6b106f1bc8820ed8738ca585972ca541
• ocaml(Ssreflect_plugin__Ssrview) = 73785f4482f0991336f818486345e7ba
• ocaml(Ssreflect_rewrite_plugin) = 28f385ef3c13786b888434f041a65937
• ocaml(Ssrmatching_plugin) = 47740f9f41d7bde9b34c128f3187aea8
• ocaml(Ssrmatching_plugin__G_ssrmatching) = 56770d0c650f38cf9b51cf00745bd79d
• ocaml(Ssrmatching_plugin__Ssrmatching) = 702fd49c3df76e2f2183033697b865ee
• ocaml(Stateid) = ac360e8e16e5dcaf4ca372de5e192984
• ocaml(Stdarg) = bdf606301002d42f15297155c150fc31
• ocaml(Stdlib) = 7ff659a4a6b8ca32adc85623b24921e4
• ocaml(Stdlib__Arg) = c45f9dbce830bdf7c07d08fc27cae4b2
• ocaml(Stdlib__Array) = c1e9990cfc96f4a80be219086df84a1a
• ocaml(Stdlib__Bigarray) = 53e1fb135dc2b52a9be495706f0fe941
• ocaml(Stdlib__Bool) = 7d26c397d64c30c6bfc9fcc31bfd9e64
• ocaml(Stdlib__Buffer) = 199531813c148c733aa4841901f61885
• ocaml(Stdlib__Bytes) = 673437615face5d16342decc909aee70
• ocaml(Stdlib__Callback) = f81228af62f8d1689727fb188b982c9c
• ocaml(Stdlib__Char) = aab5b2646a35544343b9729f2a340b60
• ocaml(Stdlib__Complex) = 10107702cfc5d64ad493797d02699351
• ocaml(Stdlib__Condition) = 1c01c895aec3b63b8ab8cbe2aa66d19e
• ocaml(Stdlib__Digest) = 34f0d73da12b160ad2ec9f14ef6ccb12
• ocaml(Stdlib__Domain) = f4f911af3a887deb4246da1952f3bbde
• ocaml(Stdlib__Either) = d0d544d8ad6cd8d3916ef604e87e8b79
• ocaml(Stdlib__Ephemeron) = 0e97e578bba2a1892394a875582409b1
• ocaml(Stdlib__Filename) = dca44599068c4f1117dfeb6a2637f3f9
• ocaml(Stdlib__Float) = 982b5c7843be6c7a654d37077ab2df6f
• ocaml(Stdlib__Format) = 59fa71efaaaea19dea6b27602dcaaaa2
• ocaml(Stdlib__Fun) = 69dd52f26a432581d74d2acf8cbfdd4f
• ocaml(Stdlib__Gc) = 7001b1bdc5fa669e74321ebe814f5c3c
• ocaml(Stdlib__Hashtbl) = 962e9d183e8a207a666ca7506cf46032
• ocaml(Stdlib__Int) = 415d62528f7701118a1cda50878c4676
• ocaml(Stdlib__Int32) = eb4f33ed29b560525b336e79955fa30a
• ocaml(Stdlib__Int64) = 29e84e0d87545e4220cc5617eb2d20d5
• ocaml(Stdlib__Lazy) = d0b8d3be22a8b5bdfc9dda1877ae006f
• ocaml(Stdlib__Lexing) = 070822eb5537492e7ac0d885f1627b82
• ocaml(Stdlib__List) = 1f65c7c74ac3633417a8002cc6dd0e53
• ocaml(Stdlib__Map) = 2d8ea4e0be35a4403643e7043fc81316
• ocaml(Stdlib__Marshal) = b6dd359978d92b445715f8b6e7291756
• ocaml(Stdlib__Mutex) = be9647a85be946b28ceaaad8440df78c
• ocaml(Stdlib__Nativeint) = 3274bc361f120620f5df0ee8b898262b
• ocaml(Stdlib__Obj) = 70f3df7415d40eb721c8413fa408b7b6
• ocaml(Stdlib__Printexc) = e58645338ce0e91a971f2806d56d691b
• ocaml(Stdlib__Printf) = 689694603948509ee3d0b39b9ac66005
• ocaml(Stdlib__Queue) = 3b321c1bad5b935cfbf4767b238e4180
• ocaml(Stdlib__Random) = 56f5b48db4d9ef67c6b0228d4fe599b4
• ocaml(Stdlib__Result) = 57c890b1fb51649494b6cefd7d3ddc9b
• ocaml(Stdlib__Scanf) = 2e9739978caab34087dc83418ace9de6
• ocaml(Stdlib__Seq) = 1d1c31e02b77070ff0e51eaaab2af0cc
• ocaml(Stdlib__Set) = f1c0353417503cf69279f65dd7b31d22
• ocaml(Stdlib__Stack) = 8beb90704d5de14f0323d6421c8095d6
• ocaml(Stdlib__String) = 64f1c33cae78f3dd80ca58dbba3deaf9
• ocaml(Stdlib__Sys) = 06196acdacded24c46c02b8acd00223a
• ocaml(Stdlib__Uchar) = f6a44dd0c2e2c80b44deed7eb3c121ef
• ocaml(Stdlib__Weak) = d315fd61fbd009f4439cd0d03c62af48
• ocaml(Stm) = a9cc604f5964ec235a7e9d806104a8bf
• ocaml(Stmargs) = 1b963824eb7d6638699545d167312798
• ocaml(Store) = b9136c58a2dd4791fc1d21a39fb36017
• ocaml(Str) = 82bb8230a6bbf7cb2d8be245938b615a
• ocaml(Structures) = 99ba9ec577d88dad4832d647a0fdcec6
• ocaml(Subproof) = 77997f729bc8ea707a3dabdb438c471d
• ocaml(Subst) = b930cee1e6bdd0d12aaa3723dec0cbf8
• ocaml(Subtyping) = 076e0567f94adb4c45e466fa0114e676
• ocaml(Summary) = ca7e736988ee337c2e6af2ffafbfa693
• ocaml(Synterp) = d19cb256d4733b9eaecd85c11ba1df48
• ocaml(System) = da05553465ca18199cfa8093164a0cc6
• ocaml(TQueue) = 06f2f0c295a422dab7042027e9408739
• ocaml(Tacmach) = b1f779aa8da3961107288fddf853dba4
• ocaml(Tacred) = 6df185ce36d9d6c2c0790973b1562766
• ocaml(TacticErrors) = 3a4670e2c03c36db171b2e82bf3e2081
• ocaml(Tactic_option) = bbb86211c57b5c84c3696019981a9e1c
• ocaml(Tacticals) = de6be8e9e4b54022ca72f3d1cdd22efb
• ocaml(Tactics) = c5ad32a92fdc6e398cc25843b7ec5052
• ocaml(Tactypes) = 6346123a046b6e594d2089c928b438c9
• ocaml(Tauto_plugin) = 9ccf8b9a8e9b5f349fb354a6268da0e1
• ocaml(TemplateArity) = bb828ae60b490a4756b085ae669d817d
• ocaml(Term) = 2b30b78a0406e5c7f9054fab45677780
• ocaml(Terminal) = e6ddc9c8ac2d341ec485865bea78afaa
• ocaml(Termops) = cbb09da5301554267966cd1068c64be1
• ocaml(Thread) = 99d33b3840c6d249522009e7ea8cf472
• ocaml(Tok) = 7c84e933bab56e3b522985fc96cdffcb
• ocaml(Top_printers) = d1aa4f401dbe53287ee2d70af66bf87e
• ocaml(Topfmt) = 580b1b3b1cda8f0426e10ea2d9b4b3ed
• ocaml(Toploop) = c80e2fca60fda9d8dfe6e9bfde4f1118
• ocaml(TransparentState) = c77eeddd5f0812ba046879db87b684b7
• ocaml(Trie) = 49f3b048c4ef037dc20113ac2ad9654a
• ocaml(Tuto0_plugin) = 55bac9a5a042df8029066af4a5ecc9ab
• ocaml(Tuto0_plugin__Tuto0_main) = 501355a8e6223a4f8b30bcc5108f2dc0
• ocaml(Tuto1_plugin) = 00435ebd7722771ac79d9c776a1817c3
• ocaml(Tuto1_plugin__Inspector) = cec56edb003bd7f80868692373c20d80
• ocaml(Tuto1_plugin__Simple_check) = 63048f5db11fe7da7178d22904e13bb2
• ocaml(Tuto1_plugin__Simple_declare) = c869491e08240545b5e7f1a0f8861b8b
• ocaml(Tuto1_plugin__Simple_print) = 71d90168657b68c7f167b28fa68cac3e
• ocaml(Tuto2_plugin) = 184262ed8436fe96abc9a352ae926716
• ocaml(Tuto2_plugin__Counter) = adaec3cc229db9f72843af6871311eeb
• ocaml(Tuto2_plugin__Custom) = 35e76c5ea338b2ed2dd6799a746bbf6c
• ocaml(Tuto2_plugin__Persistent_counter) = 4d4990a44c8c04bbd27cc573d45d6caf
• ocaml(Tuto3_plugin) = 8d95e40d324b36be29469244aa44d456
• ocaml(Tuto3_plugin__Construction_game) = eaebf4f33828a839362d45d3070f3938
• ocaml(Tuto3_plugin__Tuto_tactic) = 616c53cd9d689f1cc1b1b764f990c021
• ocaml(Tuto4_plugin) = 6a376dcf2741cdebdb070a1441263c46
• ocaml(Type_errors) = 4b5ddc3b8506bd6493f812b18295dbaa
• ocaml(Type_immediacy) = e9c7b29e4682b2c8d33db46d874c4407
• ocaml(Typeclasses) = 02591846167bf6a5b2a04f71fbf8b123
• ocaml(Typeclasses_errors) = f494e18b533e58bce3342147fea03b0b
• ocaml(Typeops) = 987ffec4fe595af99492b727aa5e82e6
• ocaml(Types) = 9cd5e0c0403b733edee4d9c7b8a72d97
• ocaml(Typing) = 0206a863f2b459835582b6766883a0c5
• ocaml(UGraph) = 8f1fab3d7ae2480c51a17be9cf83e787
• ocaml(UState) = ff38032aef8d38f6407d88a6e18c2b70
• ocaml(UVars) = 4394845f4ccd76ef1a5e122b9a088dc3
• ocaml(Uint63) = 7dea127224220e1e5822638ceac8a7d9
• ocaml(Unicode) = 1dcf32c58474279195a1088f1570993e
• ocaml(Unicodetable) = 7978a3214251c9eae8c81d10e7e883a3
• ocaml(Unification) = fb3877defee56687cc67e322fea4f95b
• ocaml(Unionfind) = da600e6dc756b192efcd4d76cbc94ec4
• ocaml(Unit_info) = 3c074c0f4cbfe70413b3f89c1a0fbf56
• ocaml(Univ) = 3a702b869e104b8dae6ebd0c5b4be86d
• ocaml(UnivFlex) = 3f2516e92af8e41682b718f5e11cc4a0
• ocaml(UnivGen) = 319ca15f0fdd4d6d18ccb1cc0abb0c76
• ocaml(UnivMinim) = dbd6c03f3aeaafe730b42b12cca79225
• ocaml(UnivNames) = 29b9cd61dcf0e23b3b08a994fe950970
• ocaml(UnivProblem) = f7baa33a7bc8f61f048a5427b14e1d17
• ocaml(UnivSubst) = a788051fcf9f60d102c6787a15bfc838
• ocaml(Unix) = c1dc7711fef7c883b67ab33c46fd7030
• ocaml(UserWarn) = 4763877ccca8f405989fdfe0337c21bf
• ocaml(Util) = c9f8d7b5acde205a5d3eff397851b62d
• ocaml(Values) = 696451dda458a5396ea1e78d5be48ab2
• ocaml(Vars) = 8584088c92cd5d960fe7e51febd26e34
• ocaml(Vconv) = 59b361bf51d37e2e04b6011d260d7e5a
• ocaml(Vcs) = c21c4b1f7e473fefa3470cfd323e4ec5
• ocaml(Vernac) = 578b28d21e48e8daa69ade81b96d8334
• ocaml(VernacControl) = fa07740655b7d9bbeb181692020aef12
• ocaml(Vernac_classifier) = 1ea2c2b48918cc4d9985a771ac06de82
• ocaml(Vernacentries) = 0df38a640d1a3d8c087a8bc08bd11302
• ocaml(Vernacexpr) = 13dc7ae796637f86d8db39d06780eece
• ocaml(Vernacextend) = d3cce331c26a90b6d207dadd7667cdfb
• ocaml(Vernacgoal) = 77c020c11adf01b2410b0f1818410ef1
• ocaml(Vernacinterp) = 0cd759bfae2648a53f5fb765652da679
• ocaml(Vernacoptions) = 8e71dec05c5f9ffd5e1d287c07effb6d
• ocaml(Vernacprop) = 7b74fd596e38760e345e3369f78c7442
• ocaml(Vernacstate) = f2cfbb03b74107a46b7051ae1814583f
• ocaml(Vernactypes) = f408f57591b931532cb3dbe34916cfc5
• ocaml(Vm) = e1125464aa3af1d986db25fca47b1d9c
• ocaml(Vmbytecodes) = 101e482d430dfd1864e525e3f812cf80
• ocaml(Vmbytegen) = 7e9ceccb8e9bf6c6eab6a64d5d0c2d98
• ocaml(Vmemitcodes) = 291084b4a4970628aeddb6980a174371
• ocaml(Vmerrors) = 55c1afa5fc49e3a6786fe5548e84e74b
• ocaml(Vmlambda) = af857a2e5de65864f3f82dc4e3303d9c
• ocaml(Vmlibrary) = 0ccd6892ef68cf7fcb7d35f2fa364387
• ocaml(Vmopcodes) = 08d9af700e76e6c5b9dc8272952a751d
• ocaml(Vmsymtable) = 418ade7b3d5dbc66f10856e3e8872869
• ocaml(Vmvalues) = af3e9469e6583e9a07c69a236b483969
• ocaml(Vnorm) = 49d906b92455b4a4a61e3e43c3fb48f4
• ocaml(Warnings) = fb0409a10304c2fa86fc9e127c31ff52
• ocaml(WorkerPool) = e4a4344e47882d81661ed9eb7ec855f3
• ocaml(WriteOnceArray) = e6442549510daf391bca4f3c39b254f1
• ocaml(Xml_datatype) = 467b68b73cffd645333815d6b355f3c7
• ocaml(Z) = b8f36df41ec3ad4dd65a34f697424998
• ocaml(Zify_plugin) = 3726fda4ee09d032689f52a677c41d45
• ocaml(Zify_plugin__Zify) = 1d2b3fcbbd82a3dd2a77c874bcf10e8b
• rocq(s390-64) = 9.3.0-1.fc44
• 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

* Mon Oct 05 2026 Jerry James <loganjerry@gmail.com> - 9.3.0-1
  - Version 9.3.0
  - 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/05
/usr/lib/.build-id/05/b11aa7a7881dc79507ec512434e79a338ea861
/usr/lib/.build-id/0c
/usr/lib/.build-id/0c/2a622f679d8303d74ebc340c28cd6cdab749ed
/usr/lib/.build-id/10
/usr/lib/.build-id/10/9d5bb7e4356727b3e82b55a0082648bf21c6e3
/usr/lib/.build-id/14
/usr/lib/.build-id/14/3c7e2f319bab21373a24e10c4b37ef0a844b68
/usr/lib/.build-id/15
/usr/lib/.build-id/15/d7ace56adf6cb73ce54abf7ae6a94e7bc577d7
/usr/lib/.build-id/21
/usr/lib/.build-id/21/289120edc07ecbc8d1297f103fae8efe1e6882
/usr/lib/.build-id/23
/usr/lib/.build-id/23/6887ea6dfab391e333349db7970426f4400eeb
/usr/lib/.build-id/23/a1a48261e1a72297758fe7f6c5a039d8c3430a
/usr/lib/.build-id/25
/usr/lib/.build-id/25/0f0e3e5b7d64b271295a8244cab567761fa4c5
/usr/lib/.build-id/30
/usr/lib/.build-id/30/3b0808a6080749f0dd5e3d6f98fbd5f612cbd7
/usr/lib/.build-id/3a
/usr/lib/.build-id/3a/9237a78e261725206a574ac540678fa1f9fa9b
/usr/lib/.build-id/44
/usr/lib/.build-id/44/3dcfe78d98782c78f706e14e99ae9ff6840f91
/usr/lib/.build-id/46
/usr/lib/.build-id/46/6d69823b7a1a031db442527d2a39a107ad2a00
/usr/lib/.build-id/47
/usr/lib/.build-id/47/711e9d704c898e8a8d1dd6cb7c5245e61b8100
/usr/lib/.build-id/48
/usr/lib/.build-id/48/08a563120c5ff4c159ac394a89d7d04e34dc6d
/usr/lib/.build-id/4c
/usr/lib/.build-id/4c/ca1cee4ef81b7a02d156c24204e1d37c0eed4b
/usr/lib/.build-id/4d
/usr/lib/.build-id/4d/44b98b3baabd5623f5e37845beab30f178aae3
/usr/lib/.build-id/51
/usr/lib/.build-id/51/fb62f8b3a8d7d7509f507c7c05eb1fd12a0935
/usr/lib/.build-id/52
/usr/lib/.build-id/52/0966860641dbe4ea215c7a88c6d7ce3e90501f
/usr/lib/.build-id/54
/usr/lib/.build-id/54/f1edb8e3fe34d4dbd87b2aad043c80b114a334
/usr/lib/.build-id/60
/usr/lib/.build-id/60/730b6e4f2c44ebed0734035a72da2427708a76
/usr/lib/.build-id/65
/usr/lib/.build-id/65/5d1c07a591b4d054eeaf38962acb97fd921023
/usr/lib/.build-id/66
/usr/lib/.build-id/66/a2d535591c65d8d63b11a71b87bf6d24fc7156
/usr/lib/.build-id/6f
/usr/lib/.build-id/6f/180410641bd612218098b93fb973b353dd1894
/usr/lib/.build-id/72
/usr/lib/.build-id/72/0f1b93138696810055b780b11711eb2504a93f
/usr/lib/.build-id/72/7f71a13a2b85fe5382987ad565f143c8f17931
/usr/lib/.build-id/77
/usr/lib/.build-id/77/1de286091d45def7acf04abd6f6fe04ef7d5a2
/usr/lib/.build-id/7c
/usr/lib/.build-id/7c/9b47dd81288ccdac7ce220058f8256a8814dc2
/usr/lib/.build-id/7c/b3debe95ba2c950b1201f38ab2aec6b49cb1a8
/usr/lib/.build-id/8e
/usr/lib/.build-id/8e/b0a8f47de085cc102d703ca3529da449dfd02a
/usr/lib/.build-id/8f
/usr/lib/.build-id/8f/e9880589559d62f4ee1aebc39ee4694ef39298
/usr/lib/.build-id/93
/usr/lib/.build-id/93/645f555bf90937274933b88279dbd52f88e990
/usr/lib/.build-id/96
/usr/lib/.build-id/96/2440916037f929d9dd110e234237fb4c769d73
/usr/lib/.build-id/97
/usr/lib/.build-id/97/cab367e95ee6c4a805fd14d73431db60a2e4cd
/usr/lib/.build-id/a1
/usr/lib/.build-id/a1/30d0189aa7467a7a999e8425faead79acb6d0c
/usr/lib/.build-id/a1/a329aa116f37fded5fc141b00613fec3f4ced1
/usr/lib/.build-id/a4
/usr/lib/.build-id/a4/9766c79c0552d096e418eb2053ab5750bc75fb
/usr/lib/.build-id/a5
/usr/lib/.build-id/a5/ba6ad668ecfe86925bdabcba4ca564b32b7090
/usr/lib/.build-id/a5/cae789c133ed434da73939727f56420c6c54ff
/usr/lib/.build-id/a9
/usr/lib/.build-id/a9/dea1e5a5f33293b7d5d2c505a91b20cc98d628
/usr/lib/.build-id/aa
/usr/lib/.build-id/aa/a1318b62c8504b5b8dafe6b1389fd0f8452033
/usr/lib/.build-id/ac
/usr/lib/.build-id/ac/904b73c8b3b01d62ebcb3f3c6f680751acd90b
/usr/lib/.build-id/b1
/usr/lib/.build-id/b1/c29378baedef4618979677bb447aad6c4f87b3
/usr/lib/.build-id/b4
/usr/lib/.build-id/b4/26af184c4717c5c590eba588e6a6d9ec0dc11a
/usr/lib/.build-id/b5
/usr/lib/.build-id/b5/c8db9fd30eeea96e8a00012766b045066c5d69
/usr/lib/.build-id/bb
/usr/lib/.build-id/bb/69618e1e16c78653f9ea75e3556ca607c4ec97
/usr/lib/.build-id/bc
/usr/lib/.build-id/bc/036e2e40c6e0cbf39afbd461efabd1beaf7e75
/usr/lib/.build-id/c8
/usr/lib/.build-id/c8/a7bb318665b5107d65847badf8f7dcf808bf19
/usr/lib/.build-id/cc
/usr/lib/.build-id/cc/cb58e6ae1fec33c23655ce8b4cf5543a961763
/usr/lib/.build-id/ce
/usr/lib/.build-id/ce/90d8956957321f68412820e7f59b2f0cb9cd4f
/usr/lib/.build-id/cf
/usr/lib/.build-id/cf/d442f9cbcce5bc6bf4de2434fff1561d57028d
/usr/lib/.build-id/d2
/usr/lib/.build-id/d2/61a7ae3cab4c04a7b4aa8a9a877f64b9c9c33e
/usr/lib/.build-id/d3
/usr/lib/.build-id/d3/ab45f7a4fa562d0ac9f53ae532377f76efec7d
/usr/lib/.build-id/d3/dcb8ea09d1c70d2c21f6a0c0d6f4b27b1bb846
/usr/lib/.build-id/d7
/usr/lib/.build-id/d7/88e221cc66e754a634ac1f98bf0c390af091a9
/usr/lib/.build-id/d9
/usr/lib/.build-id/d9/bde7efb494098f207cccc8d685042b07cb5b75
/usr/lib/.build-id/e2
/usr/lib/.build-id/e2/abe21ec70bdeac23bd84698211eee15c65b997
/usr/lib/.build-id/ea
/usr/lib/.build-id/ea/1b2f4dc28deb5dba9b0cf205ef3ebf7eedec8c
/usr/lib/.build-id/ed
/usr/lib/.build-id/ed/41c328646059ed1062b969a5b929395f689de7
/usr/lib/.build-id/ef
/usr/lib/.build-id/ef/71649eb7a189f99243799be5e16d534bff7c0d
/usr/lib/.build-id/f2
/usr/lib/.build-id/f2/21f12daf7c1e0b3cce734d4472cf7c457ac942
/usr/lib/.build-id/fc
/usr/lib/.build-id/fc/551367e17babde7c5a521e4c84db0db9833e66
/usr/lib/.build-id/fd
/usr/lib/.build-id/fd/aa0006f2dba9b035a4585fe05ad1eceb6e885a
/usr/lib/.build-id/ff
/usr/lib/.build-id/ff/5f1d2b3a59f0b995758643985ba7249d3508d3
/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, Wed Oct 7 05:02:10 2026