rocq-runtime-9.2.0-2.fc45 RPM for aarch64

From Fedora Rawhide for aarch64 / r

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

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

Provides

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

Requires

• /usr/bin/ocamlrun-a100
• /usr/bin/python3
• glibc >= 2.43.9000-22
• ld-linux-aarch64.so.1()(64bit)
• ld-linux-aarch64.so.1(GLIBC_2.17)(64bit)
• libc.so.6()(64bit)
• libc.so.6(GLIBC_2.17)(64bit)
• libc.so.6(GLIBC_2.25)(64bit)
• libc.so.6(GLIBC_2.28)(64bit)
• libc.so.6(GLIBC_2.32)(64bit)
• libc.so.6(GLIBC_2.33)(64bit)
• libc.so.6(GLIBC_2.34)(64bit)
• libc.so.6(GLIBC_2.38)(64bit)
• libc.so.6(GLIBC_2.42)(64bit)
• libc.so.6(GLIBC_ABI_DT_RELR)(64bit)
• libgmp.so.10()(64bit)
• libm.so.6()(64bit)
• libm.so.6(GLIBC_2.17)(64bit)
• libm.so.6(GLIBC_2.29)(64bit)
• libm.so.6(GLIBC_2.35)(64bit)
• libm.so.6(GLIBC_2.38)(64bit)
• libm.so.6(GLIBC_2.44)(64bit)
• ocaml(Abbreviation) = 2866341c07206e251334a49e832c17fb
• ocaml(Abstract) = d349642c3b33fa719d8495f366c020bf
• ocaml(AcyclicGraph) = ce0c9bd3b201f36ced3b625547d079cc
• ocaml(AllScheme) = c0cc86235aa99661ae324b2533b2dcde
• ocaml(Arguments_renaming) = 64b2bf6ea1cb0256afb593021c356667
• ocaml(Assumptions) = 7c0bebdab4415e3988aa028be248db1b
• ocaml(Asttypes) = 84c3bb90e4690818f538bd778d47b806
• ocaml(AsyncTaskQueue) = d857d85c726f8717d56a95c9a71373db
• ocaml(Attributes) = 4aa844b07d604ffe7217729331bda291
• ocaml(Auto) = 1849ec5b6f24b1423e7621c0c4dc6380
• ocaml(Auto_ind_decl) = 776485563be43c55ef560b71bc1ee2b5
• ocaml(Autorewrite) = 428fed4af2fa5957e7050408802630e6
• ocaml(Aux_file) = d60f22ef456531964171264e605461e9
• ocaml(Big_int_Z) = 9da002110bfe02e98c8f142c6f7dcd50
• ocaml(Boot) = f4d97e713a6c402b8fdc05370892f9c0
• ocaml(Boot__Env) = 40f0e5eeb9772e25a9a23798b7d8af94
• ocaml(Boot__Path) = 0506595f70d13318efeb83e8c83acf38
• ocaml(Boot__Usage) = f36579e92f4ad02ef5bcba239cef2a95
• ocaml(Boot__Util) = 60f9c252382a2b5b4c6216bf43e56074
• ocaml(Btauto_plugin) = a898c35732bad1cf79e48c8329bfe357
• ocaml(Btauto_plugin__Refl_btauto) = 9340258b301d13e307830764e05b75bc
• ocaml(Btermdn) = b9c178e6c9bd209f2a0bc5a5262cf6a9
• ocaml(Build_path_prefix_map) = 17a63dccc7a34c84db5fa108594069cf
• ocaml(CArray) = 5b32a33e358714547ce6daeba0f12ad1
• ocaml(CAst) = 385fa113703c5cc4b2aac40286c513fd
• ocaml(CClosure) = c9285ea5ffdb8bdec971594e8314e54e
• ocaml(CDebug) = 450ef430d34972b281d4a0e01c850b22
• ocaml(CEphemeron) = c8ec9684138eae94f9ada62543edc0cf
• ocaml(CErrors) = 00ead52ef0b5e849f95268787cca60cd
• ocaml(CLexer) = 8731472584da9132dbbbea9e384c9143
• ocaml(CList) = 0882adb5c5a227e92b2a3a07183e83e6
• ocaml(CMap) = 8a56e198dd6e5a2f9a7b38c2abb1db60
• ocaml(CObj) = fefc53898cfbaa52c2502f3190ad9218
• ocaml(CPrimitives) = 83560da1532dd9fe868cd437983f2e90
• ocaml(CSet) = 29dbd5eead5024c34a1593aadc924d05
• ocaml(CSig) = 26c574d98d011351d971fbd27b9e8b09
• ocaml(CString) = 13b232370c07ef859b331ccc579a183e
• ocaml(CThread) = 2181b493c2a74663b35cb6eec95e0ba1
• ocaml(CUnix) = 57f5c9158430515b08a4f211723449fc
• ocaml(CWarnings) = 02eebb5695bd1c2c73b7403691062f22
• ocaml(CamlinternalFormat) = 7befae1426868940d5cb072b5eb42b62
• ocaml(CamlinternalFormatBasics) = 5cba8713ea434e43a50cd422bda47dda
• ocaml(CamlinternalLazy) = 39aa2e9bf7e25b383556f7748b45c72f
• ocaml(CamlinternalMod) = 35f37f6a40dd41769a0e040d26ca6d6a
• ocaml(Canonical) = 2983418a0f700a9210a60ad0f9b60714
• ocaml(Cases) = 987596b92b232df36ba778d054f9dc3d
• ocaml(Cbn) = 19d8caf3090ef84f58db14c193776b2b
• ocaml(Cbv) = 6dd06b7b7a406e61170373d83002e550
• ocaml(Cc_core_plugin) = 5008fc268e0aeb962a484f8824d656a8
• ocaml(Cc_core_plugin__Ccalgo) = 516a5332641362ea87541f42f083cb1b
• ocaml(Cc_core_plugin__Ccprojectability) = b29f45b2dd88e2376091b269b0e9d44c
• ocaml(Cc_core_plugin__Ccproof) = e2c9a2351bf4017e5e8ee04a368615d8
• ocaml(Cc_core_plugin__Cctac) = b9b2a7e7a0e3c0db58aefd0724fbfb9c
• ocaml(Cc_plugin) = fa878db0c2ecfbdc0547984e7dea33bf
• ocaml(Ccompile) = 664fa698bb7851f6656561a03c043cbd
• ocaml(Class_tactics) = 89eb41447895efc14e11d2d6edc2d5aa
• ocaml(Classes) = c79e3d4be48ea2070a1acc56a30927e1
• ocaml(Clenv) = b33e45659ab7e415a442f41e58d64d9b
• ocaml(Clflags) = 06dc53fbfc3a29476f3b5c57cc184172
• ocaml(Cmi_format) = 727e7c35092afc0b2d4cbd6d8e021283
• ocaml(Coercion) = 9206422ecc2f32c42ff6258ec7bb7d18
• ocaml(Coercionops) = 06e1440cf50f1a14bcd9e5acd6894057
• ocaml(Colors) = c3905a5680ecb64d80ec7bbafa5ecd67
• ocaml(ComArguments) = f8c1b503adf68e2f5e6862ac57fd9ae0
• ocaml(ComAssumption) = cacf46edc581ce6f49273b2ea34c4484
• ocaml(ComCoercion) = 6706aad15acbf1c999c900393f13bd37
• ocaml(ComDefinition) = eca99fbcbd120db98ef88d9f00fd3151
• ocaml(ComExtraDeps) = 8acceb9e5bd62889f38b45e6fb170898
• ocaml(ComFixpoint) = 29790a239dbf9ad724fb7d2d33b2c02b
• ocaml(ComHints) = 483dcd9bd0eebb0013aad08acf7bf036
• ocaml(ComInductive) = 7caca52e511795e66addee229c20c8e1
• ocaml(ComPrimitive) = bc3d5f4531b31f2f246708cb5bf1e538
• ocaml(ComRewriteRule) = fefca55aabbe39bad60e026f3791c0c1
• ocaml(ComSearch) = d6831b77e41611c71eadb86741ba5e3e
• ocaml(ComTactic) = 6f0fb33631f9361a7d79cdd36c36ec7c
• ocaml(Combinators) = be350be49019d5ea582baf2a168616da
• ocaml(Common_compile) = d0bf92558c786749ce41abc42d4e1462
• ocaml(Compenv) = 442a6303ba470f6994376b1562d4b4b9
• ocaml(Config) = a89ea1ef7095df41e649de7dd71ad982
• ocaml(Constant_typing) = ccf289ca59f1c75d69177747fd0e512e
• ocaml(Constr) = 9dadde4182692178010a5198af7d913d
• ocaml(Constr_matching) = 3871d3fb767fd1c453a00fbc6b32b062
• ocaml(Constrexpr) = 7eb6d536d5e863c0139648416fee691b
• ocaml(Constrexpr_ops) = e0fef7d760f52531cf8e514390dea612
• ocaml(Constrextern) = 102814bcccca1c298a751905b139100c
• ocaml(Constrintern) = 8d1737b938d83e64847c85c721441184
• ocaml(Context) = 4b00288eda58099636359976fb690e6b
• ocaml(Contradiction) = 698faf127528f981c0e6120a0db49efc
• ocaml(Control) = d783c66785d45e326f46961806c841cf
• ocaml(Conv_oracle) = 483252ac95333754084890d1b56ffc12
• ocaml(Conversion) = 986b7f42c233728daaf352167dda80f7
• ocaml(Cooking) = e46065361836085992529aba620b7dee
• ocaml(CoqProject_file) = ebc69a93e4ee839e0945746504493513
• ocaml(Coq_checklib) = 2a01f7303c49edef72de77687ed90e2d
• ocaml(Coq_checklib__Analyze) = 0f443f55e83dd73472aaa84c9cbe1268
• ocaml(Coq_checklib__CheckFlags) = 31c2af396c2c5dc9a14d085bbf27d1ef
• ocaml(Coq_checklib__CheckInductive) = dfaa89979cd5186ff2c0c60e41d52c9e
• ocaml(Coq_checklib__CheckLibrary) = d81141387664645c9decf49e1ec18d9d
• ocaml(Coq_checklib__Check_stat) = be0f17e1883b04aa73fdad55d6826b40
• ocaml(Coq_checklib__Mod_checking) = 42ab97cc29c8c085c21bacb87f9ac439
• ocaml(Coq_checklib__Safe_checking) = b95db74daca27f40d95393dc97c29fd3
• ocaml(Coq_checklib__Validate) = 31936aa730ede570943107b95c53937c
• ocaml(Coq_checklib__Values) = 99587482c4746aa56b10c783218bfe44
• ocaml(Coq_config) = e637fe8ad1c7762085636f5615d35265
• ocaml(Coqargs) = 48b36f75693d942df078fe1d3e3c4c07
• ocaml(Coqcargs) = a4116d7c193089721b5686b697df3788
• ocaml(Coqdeplib) = 3b3ba740d9fabcbaf811791f04e651cb
• ocaml(Coqdeplib__Args) = fe678482b11c9df91252e2f1e87cf92b
• ocaml(Coqdeplib__Common) = ad781270697381debb54e572bbb2c97e
• ocaml(Coqdeplib__Dep_info) = 5404995fc6efdaa91d2d3f88294e23de
• ocaml(Coqdeplib__Error) = 7499be48eba4f91bd0af5e972a69e9a5
• ocaml(Coqdeplib__File_util) = 9bbfd8523a68709dfe340904269fcaae
• ocaml(Coqdeplib__Fl) = 7f93cdaf9ae9b29bcf560ec4b1368531
• ocaml(Coqdeplib__Lexer) = e1e20c4225f7b14adfb67721a18f9d40
• ocaml(Coqdeplib__Loadpath) = afd18f9811e298147a006026924e7a09
• ocaml(Coqdeplib__Makefile) = a51b9424d0899ecd606895f5e98c875a
• ocaml(Coqinit) = ae3cef82fb7852621c09f5f5f4a88e6e
• ocaml(Coqloadpath) = 32745135dfe8a7887ce188a6380ba1bd
• ocaml(Coqloop) = 2b286e8f790645863e9221583abcddf5
• ocaml(Coqrc) = 8b864aa19146e96b64177830ccd0c099
• ocaml(Coqtop) = 8a6890ced3aa1d990b292f9b14b852bd
• ocaml(CoqworkmgrApi) = 0303812f0bc2e40262377d7a727b4d4b
• ocaml(DAst) = 0d6913c4d5836dd79b50f3ae7800623e
• ocaml(Dag) = 93ad85e0a9f92f2c241946be044b70de
• ocaml(Data_types) = d266299998caa3e47beb52432207d50d
• ocaml(DebugHook) = f4f7d4f36c40a91d2e60a625d1ca9482
• ocaml(Declarations) = 6565fde992dda095d8a344bbd4f7bb40
• ocaml(Declare) = c44b5595edc0aa524bf733cc0b0cc0a1
• ocaml(DeclareInd) = b91181a4ed145d1e4dd22fe04eadc0d7
• ocaml(DeclareScheme) = a6c14f2914c0a454df36c3254e86f492
• ocaml(DeclareUniv) = 329503a5a1d441afef8482312f9a1bb2
• ocaml(Declaremods) = 9674e5b99b801088aff92af8925cb586
• ocaml(Declareops) = 5cdd00607bedae0a4c4769361155e771
• ocaml(Decls) = cb80408cb21e0770c41117142d6a3a00
• ocaml(Deprecation) = eaef5db5db572270ea58333142cc7c25
• ocaml(Derive_plugin) = 531eded1c4e33b430f1edab7cf92f39b
• ocaml(Derive_plugin__Derive) = cd46f55dd7a59c3b3f331dc1617ef528
• ocaml(Detyping) = b4c8cfed2997917dbf37b3dae8c6a00b
• ocaml(Diff2) = 69bada9b51ba3a56b0469c102397d3c2
• ocaml(Discharge) = 5c9173d95478aa2a657ff65ed01cb50a
• ocaml(Dn) = 6d6cdd6bd4237efa56f781a415bae887
• ocaml(Dumpglob) = 6080e7fd8c6b3db64f94d34b580b5c94
• ocaml(Dyn) = 1410e5a9f98f9411c075d713305b4c26
• ocaml(Dynlink) = 04a4608c31d5414c15167aa05423343d
• ocaml(EClause) = 280b497f361e6aa4250aa59d6980dceb
• ocaml(EConstr) = 0f45e6ea34228b8ac4a6f13ffeb198bc
• ocaml(Eauto) = ffb32c2494bf7d8288ced0c4daebfe4b
• ocaml(Egramml) = 07b9ad25f9a66c17a0565208a9cacada
• ocaml(Egramrocq) = 1e8818eee062467855cffaacdf1df0fc
• ocaml(Elim) = 684b97c97eeb88d577235d3de0c4e7fe
• ocaml(Elimschemes) = 96f2986ed226deaae2f426e28ea29416
• ocaml(Entries) = 81371aa55de5718540cff21917f91637
• ocaml(Env) = ce446975d8bb8fca5c8cab5430ebbe58
• ocaml(Envars) = ccef56ade890607251a63150639459c7
• ocaml(Environ) = 333a65beee3fab8db793cb06ef9fa139
• ocaml(Eqdecide) = c39d847c3699af698e56eb07564cc228
• ocaml(Eqschemes) = 63f4418dc9fefb61912bdf8f1f2e1c26
• ocaml(Equality) = 05291c5e6eee2db27a39c8afddb774eb
• ocaml(Esubst) = bd721a72d48ad134792fe495afd30ce6
• ocaml(Evaluable) = a8a4833f67d86e5d772fd6d70f72da93
• ocaml(Evar) = ac2e8f4bba960dd78af41a3bad3f3238
• ocaml(Evar_kinds) = 1aa7bca6fcc10c8f32b49a3ca4b8fbf0
• ocaml(Evar_tactics) = b34fb1add2d876417c953db4e9637382
• ocaml(Evarconv) = 40707fbe7495060a801c64500b4980a4
• ocaml(Evardefine) = 480fc10472fe601d5a315385b97d60cb
• ocaml(Evarnames) = 4bc8d3c3d43662fa9999ef7f69f726a0
• ocaml(Evarsolve) = 37098b93d7555024a4b514ac28184e9c
• ocaml(Evarutil) = 22e74b8de163ca5ed50b21a30b8bc326
• ocaml(Evd) = 435ea1d729f8c665c3cacb64856a8cea
• ocaml(Exninfo) = 8b1c1f5a459f237a6eefbdc05e3c0c3a
• ocaml(Extend) = e41b32b8e9564e6947343503e735ed57
• ocaml(Extraction_plugin) = e32377a97ac510edef83869ea50bad69
• ocaml(Extraction_plugin__Common) = c9c02bc0d4ff4f4627e47fc125f91aa2
• ocaml(Extraction_plugin__Extract_env) = bf0be8abb805482e8643424af4e761d9
• ocaml(Extraction_plugin__Extraction) = 4ea3e133c56b0ddea5e02006778629f6
• ocaml(Extraction_plugin__Haskell) = d583126c5a2ab8110fca3bf9e89d91b0
• ocaml(Extraction_plugin__Json) = ed2e1f73082d6f8e3b7e5a5fc6ccf822
• ocaml(Extraction_plugin__Miniml) = 5c1ee61d15954f96026ad7ace68bbf7d
• ocaml(Extraction_plugin__Mlutil) = ada40c46faea011c7f57c34ee444e2ec
• ocaml(Extraction_plugin__Modutil) = 383859057f43e126b1e368dc3dc03256
• ocaml(Extraction_plugin__Ocaml) = bcd6660ad45bb4250857e9c99619716d
• ocaml(Extraction_plugin__Scheme) = f84598e340b27dd2a49acabb6096d461
• ocaml(Extraction_plugin__Table) = fb8ff25252ea80cf05117cfbdb92bc99
• ocaml(Feedback) = 96d63b0916cfd4f7ca48c7bba8ad140a
• ocaml(Find_subterm) = 7ad60a04ad7eae4539358621bb4ecb73
• ocaml(Findlib) = 1b0811e75e5bbadb5e395761f4803f4b
• ocaml(Firstorder_core_plugin) = fec159343c5551bf68c4f6f086016025
• ocaml(Firstorder_core_plugin__Formula) = 79b12a57d2b2de0855cac3bca02cf7df
• ocaml(Firstorder_core_plugin__Ground) = 8fde6cd817d9b15d1b99a898f8f27eb1
• ocaml(Firstorder_core_plugin__Instances) = 1321d2f2dc207539a61506e9a0677c9b
• ocaml(Firstorder_core_plugin__Rules) = 5b4c8fa9cd60b3f8ccc3bb2ea028f9fe
• ocaml(Firstorder_core_plugin__Sequent) = 71492f76b26fe3318a9e390ef54f2bce
• ocaml(Firstorder_core_plugin__Unify) = 66676b7d5f29386cc73eeed18bad5d68
• ocaml(Firstorder_plugin) = 79828095e4c214af613d0c38e2fbef2d
• ocaml(FixTactics) = 63270b418dd8dae4b3953f0bcffcd12d
• ocaml(Fl_metascanner) = 78c4d683804858fa509104de11c8b57a
• ocaml(Fl_metatoken) = 2c8d37da38d7744002094a323ec4f8d9
• ocaml(Fl_package_base) = 0d62177de3f8f40d822d731255ccffaf
• ocaml(Flags) = f546cda0ce1f65db7d055d5e47a1ff32
• ocaml(Float64) = 5f3685872420eb559610ca8cc70758b1
• ocaml(Float64_common) = 91e85657f424d38fc4f7c19628540518
• ocaml(Format_doc) = 1a853d410bfa54de418a18cd588fe8c3
• ocaml(Ftactic) = fc1b8d5652ed5b883c54789a6881cd7c
• ocaml(Funind_plugin) = acff96e1b566211dbd5726750b8ee701
• ocaml(Funind_plugin__Functional_principles_proofs) = 26d6dc2a9aa6a43497eb51e71ac0aa35
• ocaml(Funind_plugin__Functional_principles_types) = 959f787f50ca667bb76a1e9c689262bc
• ocaml(Funind_plugin__Gen_principle) = 9b28936bfc2cbfa14e81a48e7039f2d8
• ocaml(Funind_plugin__Glob_term_to_relation) = bf05c5ca86bd6f2a3a483c3fab004810
• ocaml(Funind_plugin__Glob_termops) = 0af96a09d3a5f568d1ed7c9c4cff23b4
• ocaml(Funind_plugin__Indfun) = 94cc2c4a37a0cc07b9dd2dcfb49788ca
• ocaml(Funind_plugin__Indfun_common) = cc7eef01a52b623a5c5194553df425f1
• ocaml(Funind_plugin__Invfun) = 25891fe5ed3b452db829b765ab18010f
• ocaml(Funind_plugin__Recdef) = d741df5f94976b7062534d1c64b13e7d
• ocaml(Future) = 1544d268ac0c284d35f88f75a8085dff
• ocaml(G_constr) = b9d31025ff3e9592ddff5b405b8c1018
• ocaml(G_proofs) = 7e3022b635dd4808626ba1f504e23d79
• ocaml(G_redexpr) = 3192af7b0c6b5e5569c8b442f5675abe
• ocaml(G_toplevel) = dd0c921bc4c511538e5b5534b33483fa
• ocaml(G_vernac) = 1cf7d6275005bdb5927a6cbcdf020071
• ocaml(Genarg) = 20bc2db04e9c5f1cc022baa5ac348884
• ocaml(Generalize) = 1099bf5cc10ea5446593ecde5597afef
• ocaml(Genintern) = 389f801b33b8b8f05a36afb7372c7f1c
• ocaml(Geninterp) = 3acfa814910ba60cd4a7c312aaca4c71
• ocaml(Genlambda) = 183fb5c4fdf9f526727a384411b1c16b
• ocaml(Genprint) = b4fc1f9d71eae7851eb9cbd339eb5741
• ocaml(Genredexpr) = 255e1831f6fb4a13f8c8952808f6de89
• ocaml(Gensubst) = 7807cc31a18148918322318456eeb27f
• ocaml(Gentactic) = 5de755a17799b4e886ad266f8c741b1b
• ocaml(GlobEnv) = e20b654fc9f42aa1ba364017b98ad7f3
• ocaml(Glob_ops) = e1320398ddf1690df06a7712965debac
• ocaml(Glob_term) = 11f12049a7da3c15fd9dd3aa875b6749
• ocaml(Global) = 8600c716d40c19284f61e4c22a76f230
• ocaml(Globnames) = 6b4f7c49d606305ff84bb1e05d6c9ca6
• ocaml(Goal_select) = 55277919ac691b58221d1c92107afc35
• ocaml(Goptions) = a5a75e0526da470e8424ad0ab1d41a32
• ocaml(Gramlib) = 39dac03c4686a39022523f13c7386381
• ocaml(Gramlib__Gramext) = 02ce9dbbdaefb67b4f538dd8cc1d27ff
• ocaml(Gramlib__Grammar) = b019a1bb55cea2351deb576b82c655b0
• ocaml(Gramlib__LStream) = f6ca7c9504172ae5cf7ee4483857b639
• ocaml(Gramlib__Plexing) = b951eafd52fc9f470d50bfe44bf6d602
• ocaml(Gramlib__Stream) = 051b6e25e750f1de37a7706827c2ab45
• ocaml(HConstr) = 707781a1aba853b7e212cbcbdabd7a2c
• ocaml(HMap) = f713ae884bfe31c066c7b998c721c469
• ocaml(Hashcons) = 6f55751bed5c20cdac5336a90cab41b5
• ocaml(Hashset) = 8d0a557f8649d7eeae2802c1e49e95e0
• ocaml(Heads) = fd205bfc3f6008cd2f6732a16467b096
• ocaml(Heap) = 537d18654f73f81f96142dcfe572ed59
• ocaml(Himsg) = eb06d5f662c31f17cad748f794fe9a35
• ocaml(Hints) = 36354995814199d0add131f31234da3a
• ocaml(Hipattern) = 2f22f9b91bfb58cab9632fd8b2d619a7
• ocaml(Hook) = 4a72c7621b630b54725e8ae286e175fa
• ocaml(IStream) = 682ff6824b27e67750c44c60190cb441
• ocaml(Ident) = 384a9338d15781bf37212ce3cfd033cb
• ocaml(Identifiable) = 3c7ba31da6292c7ed926b7fadbe655aa
• ocaml(Impargs) = 4f0a65cb36c0351da2389911ce2e98ca
• ocaml(Implicit_quantifiers) = 5918d92f4ffa23b9efd891e7976daa02
• ocaml(IndTyping) = 62cf38ef7040ef0509fd85b7fc21c092
• ocaml(Ind_tables) = cba428e89a97c204396b4f0841a8aad1
• ocaml(Indrec) = 5276840d88c717b672618ff1895e6c11
• ocaml(Indschemes) = 0644ba02801b4f0e96be3c9742028188
• ocaml(Indtypes) = ce4e28427bd43fa9a3e05d8d147ee529
• ocaml(Induction) = cb277f5d49e5111020a5a3cc16539b64
• ocaml(Inductive) = a6b79bf0ffafbc8c864b83204a4fa2f3
• ocaml(Inductiveops) = e60e4c6e6ad48132ef502257ecc8c8ec
• ocaml(InferCumulativity) = e8dad109fda165a0f91faaa09fbeb82d
• ocaml(Instr) = ff8b3e60640d1ce38ab256a871a387b0
• ocaml(Int) = 6d90e5f7db4cb744e44df7510c8a0c87
• ocaml(Inv) = 5605598c8542d5b2612cdd51d31c9dc1
• ocaml(Keys) = f322419a17bdfeae47c0ac501ba6f7dd
• ocaml(Lib) = bfa8dc88bb9bf9affec4f1588db78704
• ocaml(LibBinding) = c3c1452ed1ac68a801d713e3bdb73816
• ocaml(Libnames) = 1a4ee42579b33e74374696448228fb6f
• ocaml(Libobject) = 52338f382e5fe27320d4379b8b01e14d
• ocaml(Library) = 1bff0a8bbec259cbd5846e7f26e71189
• ocaml(Library_info) = 0bdd8f21391b24096777ed1344acbdd8
• ocaml(Load) = 3c5a15453c9399e4c4b291414d61b219
• ocaml(Load_path) = 73bdece741485debc05bc796fc46bb27
• ocaml(Loadpath) = 6e5716258597544dde8b5abb66c172d9
• ocaml(Loc) = 2af96156e647600dba688160d767ed1d
• ocaml(Locality) = 048b3e5671573bdd7ffd94f14b5795b6
• ocaml(Location) = 51a5b26cac9b3515839b2a2679b6099c
• ocaml(Locus) = 1477b2cd8dec8a2bb3e60cdb2c84700f
• ocaml(Locusops) = 4b5a614865fb35cba930d473839e8021
• ocaml(Logic) = 78aff31a617ad43d61e5b6dedc032f59
• ocaml(Logic_monad) = e38c7c42d61f18c4d72404b3db7e93ff
• ocaml(Longident) = 95a4bd2a3e0c7bef7e71005b1ec0c6f7
• ocaml(Ltac2_ltac1_plugin) = 9913d38e5e00cea94740dea133ff4579
• ocaml(Ltac2_ltac1_plugin__Tac2quote_ltac1) = b23c45af7b0b0c3c1721f6823fb69383
• ocaml(Ltac2_plugin) = c3f099ff910c5df0b88d05015039ab71
• ocaml(Ltac2_plugin__G_ltac2) = e89b1bf41fb3ecd7e9cdf300fca4dd87
• ocaml(Ltac2_plugin__Tac2bt) = 971d1b6ed041c38af16a12e92c1bc1ec
• ocaml(Ltac2_plugin__Tac2core) = 1b2e8f9d34dcda83c225189cfc8e7dee
• ocaml(Ltac2_plugin__Tac2dyn) = 656babd0059d0ec8f16f81a1e8add895
• ocaml(Ltac2_plugin__Tac2entries) = 0209ac9b6b3c0518c058df9594e9b58b
• ocaml(Ltac2_plugin__Tac2env) = 7e5f8bfd54358ce2d54eb939da5ec6fe
• ocaml(Ltac2_plugin__Tac2expr) = 07fc45ce517249b1eba61fa8d3a9650a
• ocaml(Ltac2_plugin__Tac2externals) = 47f40dd44a37305ea8577a44a47acc68
• ocaml(Ltac2_plugin__Tac2extffi) = e2c9d42870758e862c95a3b5c5993d04
• ocaml(Ltac2_plugin__Tac2ffi) = 37ed8350c3d13d8b0cc6d9acbb20f30b
• ocaml(Ltac2_plugin__Tac2intern) = bde0b8e123be8badc11ef32c8ebbe22c
• ocaml(Ltac2_plugin__Tac2interp) = e7e50ff1e4d594b0fae1c0f697914a84
• ocaml(Ltac2_plugin__Tac2match) = f6b3efc42387dff92e1a3ad3f55bb6a6
• ocaml(Ltac2_plugin__Tac2print) = a5ef7983cb01530fcbdbf075a6dd260c
• ocaml(Ltac2_plugin__Tac2qexpr) = d5adddb48f2ecf03b16a0932e7b01ec3
• ocaml(Ltac2_plugin__Tac2quote) = c17e6a283a0c1309df06f1d650028a68
• ocaml(Ltac2_plugin__Tac2stdlib) = 958c620cfb88badcf1e35377af9f0359
• ocaml(Ltac2_plugin__Tac2tactics) = c0444d67621d403296d18c642f2a397b
• ocaml(Ltac2_plugin__Tac2types) = cce6ea0beb3a7fa9b101083eeeb8bf80
• ocaml(Ltac2_plugin__Tac2typing_env) = 1eb41281847c65fff410f28568319665
• ocaml(Ltac2_plugin__Tac2val) = 9b357e794a8ff5e43e519a80863f024a
• ocaml(Ltac_plugin) = f2bc593250b8f3da448b3e0d61ac7803
• ocaml(Ltac_plugin__ComRewrite) = 851242cb1c6fc8dbcff0d46b373c58c4
• ocaml(Ltac_plugin__Extraargs) = 703337931ac2b9c87beab409235cbcbb
• ocaml(Ltac_plugin__G_ltac) = bb2a792c4743d025758e8def9d5c491a
• ocaml(Ltac_plugin__Internals) = 7ebefc0d7e5264d73037600570fe6adf
• ocaml(Ltac_plugin__Leminv) = b4e30ff9c6597d66b0de43a4a6217440
• ocaml(Ltac_plugin__Pltac) = c0dd739c0da492e8482771205a8c49b6
• ocaml(Ltac_plugin__Pptactic) = a14b7df0e2f652c8f96ec3cd388b67d8
• ocaml(Ltac_plugin__Tacarg) = 5af8cc6f64d949b27a516fe19017326c
• ocaml(Ltac_plugin__Taccoerce) = 34c47650b673d60c858757331c90c5ca
• ocaml(Ltac_plugin__Tacentries) = 907b6e51ad3178e6f954b17b5a76e1a3
• ocaml(Ltac_plugin__Tacenv) = 1da64318d3c4f1838a44e21f3d6c943b
• ocaml(Ltac_plugin__Tacexpr) = 96503c2cda3602d65dbc4b38c0f68f3f
• ocaml(Ltac_plugin__Tacintern) = da146156963bcdf94575b0cc266b64b0
• ocaml(Ltac_plugin__Tacinterp) = 781afdfac21a14e3776076667ff8ec68
• ocaml(Ltac_plugin__Tacsubst) = 881cc7f5f14ecf2d6a3e4cc220eccea5
• ocaml(Ltac_plugin__Tactic_debug) = 58cc4056879dd13f0a0471a2fead3278
• ocaml(Ltac_plugin__Tactic_matching) = 7f9ae839db28d65d7aa0594801a88726
• ocaml(Ltac_pretype) = c69ec9a62c71b059674119457459625b
• ocaml(Memprof_coq) = d0324ac7b8fb9708f11fddde0e662110
• ocaml(Memtrace_init) = 58d04398643b281f0869a6c18c285ffc
• ocaml(Metasyntax) = 3222ea2ec32e77ce09ffe01df7b934f4
• ocaml(Micromega_core_plugin) = 3201f6d62ad5f9037cde547e9c7acdeb
• ocaml(Micromega_core_plugin__Micromega) = de335da3ca00d63c8912a113e53cae34
• ocaml(Micromega_core_plugin__Mutils) = acdfbfeca19e1268028a73aa65356aa4
• ocaml(Micromega_core_plugin__NumCompat) = a43ca4b61be994fe306a5627fa745d4e
• ocaml(Micromega_core_plugin__Sos_lib) = f975a1285c10aac16439602ec7eab50d
• ocaml(Micromega_core_plugin__Sos_types) = 092786202a8a60beeaffbfb6f6cade0a
• ocaml(Micromega_plugin) = 205a7a948b9d600b16fc00642bfaac64
• ocaml(Micromega_plugin__Certificate) = 695b6c88287b5e4311af0b6b8852f55d
• ocaml(Micromega_plugin__Coq_micromega) = fc33e475fd1c16fd978b9f70d3f53a13
• ocaml(Micromega_plugin__Linsolve) = 38ab8141de1c979333a4f9f35b43cb95
• ocaml(Micromega_plugin__Persistent_cache) = e393f23dd28f0b8666566049bc59dd8e
• ocaml(Micromega_plugin__Polynomial) = 60721fba80a8733bf246da682c08e5b4
• ocaml(Micromega_plugin__Simplex) = c8a900835cd4544deed452bcddf47282
• ocaml(Micromega_plugin__Vect) = 1bd2980aaf4e5df01bb934b5685c5ce1
• ocaml(Misc) = 0d02979d540c22b19f23b073524960d2
• ocaml(Miscprint) = 1e2ba076ad7813409ea1e62f6e0b75a5
• ocaml(Mltop) = f1d4c85742216c4ff94743db0cefce26
• ocaml(Mod_declarations) = a4bb92788732bff3137cb6e05650d81d
• ocaml(Mod_subst) = 2ae3a7fa4a4cd916f9fa48e07e85ffb6
• ocaml(Mod_typing) = 0a02420f53bb18625a38d6868de6455b
• ocaml(Modintern) = 29a8e32ef064a37428cfb5d23f398d6e
• ocaml(Modops) = 60d6c99acb65743a89887ea54b032918
• ocaml(Monad) = 3f0799e4953828a3e9354d0beaa1e703
• ocaml(Mutex_aux) = 9782d688445355c8e376c88b4100c2c5
• ocaml(Namegen) = 3e91d2770d5ae953d1770ebdac2975b6
• ocaml(Nameops) = 4ef2bb396e5b7518eab60fdcc9994b9c
• ocaml(Names) = 148e9d5d2ba1c0a16d00e80d17fd6535
• ocaml(Nametab) = b390759ae2f5be12bb35882d3bf60d45
• ocaml(Nativecode) = fe56e91fd3a3c9864c5da07bd55882cd
• ocaml(Nativeconv) = fa8552c1d9c0b14005df307dc194784c
• ocaml(Nativelambda) = 340dbd6a9309fbfdef3304b9101e6001
• ocaml(Nativelib) = f21908f71586fb123e1744044a7eac16
• ocaml(Nativelibrary) = 0c322a6ac63edb958762af91910c2810
• ocaml(Nativenorm) = 8f70bfd46a5e42325ca1d92cf113a218
• ocaml(Nativevalues) = 6c52af047b1da04f7d32b88ffb5aa655
• ocaml(NeList) = c3b4b70eb47ab02a25b9fe8168cd599d
• ocaml(NewProfile) = 520c62d443e16a5cb5b6c5f2e20a3997
• ocaml(Notation) = 046c36b9fd2d8c8920c4e912f10dc4b6
• ocaml(Notation_gram) = 9a632b2940c3bf807ca70f79e118b591
• ocaml(Notation_ops) = cb14e05796fa8ed2b04734a069cf33f6
• ocaml(Notation_term) = 95033ba9e96ef7946542174bbec785f8
• ocaml(Notationextern) = bce482d868fa275de7fab507ce831a5a
• ocaml(Notgram_ops) = 22562720feb2d0980d15f1a886febcd5
• ocaml(Nsatz_core_plugin) = 39ae3bc27ba2f544e94b60f557101470
• ocaml(Nsatz_core_plugin__Ideal) = d7e93564bb07505146dede688f62022f
• ocaml(Nsatz_core_plugin__Nsatz) = 1bf3688a661936436929f7d70943b5b1
• ocaml(Nsatz_core_plugin__Polynom) = 0a0b33048d521de58677aae89da71e39
• ocaml(Nsatz_core_plugin__Utile) = 29bc23633d876d42c4bc50bb52835309
• ocaml(Nsatz_plugin) = 7f39f377450040c9a376fc9c62df288a
• ocaml(NumTok) = c0ec6aff568e9a756e939205fc54c27d
• ocaml(Number_string_notation_plugin) = b4f2909aa71e21d43e14030acfd2b670
• ocaml(Number_string_notation_plugin__Number_string) = 85ad8d4a95166dae0a0c8985e7179be1
• ocaml(ObjFile) = 2c13d8ad4646786734c912359c91a0ba
• ocaml(Opaqueproof) = 1aadd50f1d0bea28189a01fd2570f17f
• ocaml(Opaques) = 9c9d15c6b001f414b038d43103e22dbe
• ocaml(Oprint) = 41100dc27016daa02bb188695d01f273
• ocaml(Option) = 92a29a188ae235a287ebc379e4dd25a4
• ocaml(OrderedType) = b1372ffa9e46e6f95b2ac14239a8456f
• ocaml(Outcometree) = e06da280e0e94a919ab84e78620428c2
• ocaml(PConstraints) = d417f36ebf2f64643590cc1369e98261
• ocaml(Parray) = c91aee66f0a62119d8324dff17c9a4b8
• ocaml(Parsetree) = 2c395b2cb558b295c123ddd00749d7d9
• ocaml(Partac) = a9fbf090ccb5f96f9ad30b4ed0965ec5
• ocaml(Partial_subst) = 293aaba2bff2483262e01afda5396a0a
• ocaml(Path) = 28571ebf710fe2a4e1508233722e3a57
• ocaml(Pattern) = 9491074e4609bd07ec8f298ec0f34ba5
• ocaml(Patternops) = c7b6b5f8b87133c7cce4d12550db3b6e
• ocaml(Perf) = d6cc427bc06a72de18140a50a353b06e
• ocaml(PolyFlags) = 1dc8f7830e4c0fd285c43e4f2c0f0292
• ocaml(PolyMap) = 629deea55fa3971f3a60fb50351278e0
• ocaml(Pp) = 2c38bf624e0ffbba3e2389beec2065bb
• ocaml(Pp_diff) = 2b6ed2a56506a1ba1dd583fd85114b20
• ocaml(Ppconstr) = 1f433276e53953c64a1ac316137a75c4
• ocaml(Ppextend) = f985d871ca437650764a739a2cd92f4b
• ocaml(Ppred) = 62bbe8d2ef098df4a01141c9fd4b0419
• ocaml(Pputils) = 880fc6879edc3cc82f9c1d16c4dd5821
• ocaml(Ppvernac) = ccd72eaac80588013f14280b6fb0d232
• ocaml(Predicate) = 0c221b82d5cdae9cbeeea482f4dc5d9d
• ocaml(Prettyp) = 2b576581dcf6de0bfd04d8b88f16e71b
• ocaml(Pretype_errors) = ce1e45156a77ba0bdc8f1f69ab60c50e
• ocaml(Pretyping) = 292f8282cf9329eee641af9bb661b611
• ocaml(PrimNotations) = e1c6c3d5cb6ae436869f4632e92f8f30
• ocaml(Primitive) = 61bc56d5729acca0db75e86a73414d62
• ocaml(Primred) = c942088999a423ee70642acf40434ac0
• ocaml(Printer) = fda9c7b624f3b01b0ce6dff9ce30a725
• ocaml(PrintingFlags) = d882fcbd32c002aa6540fed5d2754d28
• ocaml(Printmod) = 75c4f1f44f39c95d49bf109b7017cffe
• ocaml(Procq) = 6e8494b4b5b05c849bf75fce646604ef
• ocaml(Profile_tactic) = aff075d289aa40aae9cd4031680754fb
• ocaml(Program) = df8fe07e0742fa27fe73347e53a30cfd
• ocaml(Proof) = b7b2e0982a12070e270779df993f1b1a
• ocaml(Proof_bullet) = be53f78bfc6022590142ea4084606323
• ocaml(Proof_diffs) = 20d5b9c2f14918af9b3677733a76f24e
• ocaml(Proof_using) = a0d5efd5ad4cd66bf8e36b6d380ba18f
• ocaml(Proofview) = 88e6fa76daaf1f3b3f7ad818a6c8b271
• ocaml(Proofview_monad) = c2da718229d2c166ed7368eb1b91157a
• ocaml(Pstring) = a4657eedcbcee758e124eaf4bdbd082f
• ocaml(Pvernac) = 68e36250b5dfc62e97aa882d5f16a2f8
• ocaml(Q) = 659754a9895bf87cdc992c6ffcc4b20a
• ocaml(QGraph) = a0f3170eb602a676cfd042aebb11b569
• ocaml(Quickfix) = a99365c9ce5cdad164252c7e05e04016
• ocaml(Range) = fd4c0f33c700ee2d3bc0cd2a9504ce03
• ocaml(RecLemmas) = e2f8f3528b56fe0fd538b8d6e0026b0c
• ocaml(Record) = 772f8512913af42ee8ceadc120e0dbf0
• ocaml(RedFlags) = e0b3bd029593004b900aaa26937f4f32
• ocaml(Redexpr) = d4c88a147d14fc15412b3f0fb228dbf1
• ocaml(Redops) = efc902fc6d2a2345c0361b2c1aa0baaa
• ocaml(Reduction) = b488ef6076462759638ebab55215e9fc
• ocaml(Reductionops) = d7ed95e99c180213c1c306f7234983dd
• ocaml(Refine) = 38ca27018fd66731e25f44ddf2805d74
• ocaml(Relevanceops) = 6fe408538a7a0490f3c5ceb9b2c3c5a9
• ocaml(Reserve) = 6a6a644640d87c656df7b77abdc9e6f7
• ocaml(RetrieveObl) = 48b74533620394c90ad3c5bb568efb6b
• ocaml(Retroknowledge) = 0ff314acfded9b1ae195b6f6a6d53479
• ocaml(Retyping) = 3f9620033761ab1bf29c6333790ced6c
• ocaml(Rewrite) = 9b149e4f82d56018b4f783caf71907a8
• ocaml(Ring_plugin) = 4ac790d60349779bbe9e1667d30ccf7c
• ocaml(Ring_plugin__Ring) = 97b071aaf194d54207b8104626f878bc
• ocaml(Ring_plugin__Ring_ast) = 7544d854e11a6478320e3dd4cfe60a5a
• ocaml(Rocqlib) = 73cf0ea7d7f16a1f1036ac19f1e92723
• ocaml(Rtauto_plugin) = 4ab59950a066db48e1f4f8d478c5e685
• ocaml(Rtauto_plugin__Proof_search) = 77c63c69325a6e3470f8d216b881a2ed
• ocaml(Rtauto_plugin__Refl_tauto) = 6bb42d60152757e54f4a9e6ed4343e58
• ocaml(Rtree) = cc005cc024069460855d05480a7fb91f
• ocaml(SList) = 4bc007590fe5ee6fa7d6f33af5ae66c9
• ocaml(Safe_typing) = bf6483aa16ee04ad735e67272a9300d5
• ocaml(Search) = 9fb3a577bfded349a9017b1fe5ac9ac9
• ocaml(Section) = d520bc068a4aa722a9a912c6ce232114
• ocaml(Segmenttree) = db935701afb99fb41779e42b0570f32c
• ocaml(Shape) = b28b8301b24f6231950e7868a59a4e1a
• ocaml(Smartlocate) = 89064a7b5b89a7b35036c02a00f92179
• ocaml(Sorts) = bff26bd11f9b46fa49d5f70ea2679f4d
• ocaml(Spawn) = 7b2414fa666c9b7dc1a7b08236fd40b5
• ocaml(Spawned) = 3f8699948a312ecfdc3d2e579045543d
• ocaml(Ssreflect_plugin) = d0468b4d302a32ee781851b172eba3b0
• ocaml(Ssreflect_plugin__Ssrast) = 0d11b4a5ec0598da8632c5b9043d5739
• ocaml(Ssreflect_plugin__Ssrbwd) = 8f9958d345a6b1c227a5760a46198563
• ocaml(Ssreflect_plugin__Ssrcommon) = b56474b2fc2f4cc25d878696071e14d6
• ocaml(Ssreflect_plugin__Ssrelim) = 64afacd508c2a5fc0593c2192b263a35
• ocaml(Ssreflect_plugin__Ssrequality) = d9b1b2b4cd11413882b7a88d84776794
• ocaml(Ssreflect_plugin__Ssrfwd) = ec28e1e3a70172b2d11ed4b1b1b96b08
• ocaml(Ssreflect_plugin__Ssripats) = 14ae30a863d03bf818c8e563191d5c88
• ocaml(Ssreflect_plugin__Ssrparser) = 0a6de46032e0ca2a5b0fbfb3bc6329c2
• ocaml(Ssreflect_plugin__Ssrprinters) = d90b81989c6f1b6e426cb9aae8de0af8
• ocaml(Ssreflect_plugin__Ssrtacticals) = 26004ceb0376dce10f9ede24569ab7f8
• ocaml(Ssreflect_plugin__Ssrview) = c97abf230fab720900e45773d72687e7
• ocaml(Ssrmatching_plugin) = d96290de069eb528f6fba3bb3358eae3
• ocaml(Ssrmatching_plugin__G_ssrmatching) = af2fb489968476655e360952b9363492
• ocaml(Ssrmatching_plugin__Ssrmatching) = 2ea7e719a0fd558ed0069dfab4a46598
• ocaml(Stateid) = 0e9825bc21db6ba7c8247cda75d5a6be
• ocaml(Stdarg) = 7f2b030272c7dc79a52c0dbfbd47c20c
• ocaml(Stdlib) = 5debf066d2f080eabc33d8b71099252f
• ocaml(Stdlib__Arg) = 7e3499feceb334dcdbfc9de5cbbe5720
• ocaml(Stdlib__Array) = 09ad905d6230fc4f28ae1b69e8675e79
• ocaml(Stdlib__Bigarray) = 904d1271afeb602c556bf1e0f0f8809c
• ocaml(Stdlib__Bool) = 5ae91427633ceab91f24029f0410dfd9
• ocaml(Stdlib__Buffer) = c0940caa52bfb8d306ed2ca69af87ed6
• ocaml(Stdlib__Bytes) = 6fa82d0a58c0eb4ca469f084a70f9a7e
• ocaml(Stdlib__Callback) = 42025ff5ce6207abf8a8d25ca781e771
• ocaml(Stdlib__Char) = de356fade697b3b5bc1222daedbf67b4
• ocaml(Stdlib__Complex) = 7a66a05174368cc820464e6c12a3693c
• ocaml(Stdlib__Condition) = 7a45bec6dbadb9a2653333bf8ee1606d
• ocaml(Stdlib__Digest) = 2b70a92ff90913804cdc1343b1592e27
• ocaml(Stdlib__Domain) = d11ad689f3e35d9892101961a1201121
• ocaml(Stdlib__Either) = e4e548dbb128df23a9325d9cba39fc2f
• ocaml(Stdlib__Ephemeron) = b18622341371e45469e1be04e45ec480
• ocaml(Stdlib__Filename) = 49e046b4f3cb36713e404a980d6fecce
• ocaml(Stdlib__Float) = 800a4b64830048ea38a2f4bea3c77e64
• ocaml(Stdlib__Format) = 5b2f2a54d0831d599db87620d18b8ca1
• ocaml(Stdlib__Fun) = a85d85ba4df5274da68ea85f367a289e
• ocaml(Stdlib__Gc) = 37e5209d1fcf5e8dce14d0ae4850e089
• ocaml(Stdlib__Hashtbl) = 6df0309fbcf3f1661d9e3d07a603aa3e
• ocaml(Stdlib__Int) = 5e2a4d5bb778a7e299ca9d72ed5fcc54
• ocaml(Stdlib__Int32) = 6583ec691ad5b5d0403bb4dba14ff95a
• ocaml(Stdlib__Int64) = 6c1bd23e0da837071a98f3330e9f1242
• ocaml(Stdlib__Lazy) = 9888b2ba7f344f43c41116cffda5081a
• ocaml(Stdlib__Lexing) = 738e4c77ef59ce13f6f1eeecd20678b3
• ocaml(Stdlib__List) = 81a27a0a9af489e91fa1d99f325067c2
• ocaml(Stdlib__Map) = a9944feda56cab2432578db95de546a3
• ocaml(Stdlib__Marshal) = f0b9263e97f9cffe012fc7066989ec9d
• ocaml(Stdlib__Mutex) = bd8525fb671da46bc9b6403559d7e872
• ocaml(Stdlib__Nativeint) = 5a73f569861cc3c66639bcda63a82510
• ocaml(Stdlib__Obj) = 26b40efd5c9a30f8c9c87c6133b5adbf
• ocaml(Stdlib__Printexc) = 3eb12037663b6b68977615f9862f8f66
• ocaml(Stdlib__Printf) = 3303d43852c2d96a670040b4fc4aefc6
• ocaml(Stdlib__Queue) = e259a6289d4b4587c82128e5e4a93d77
• ocaml(Stdlib__Random) = 956621158e7602665cb7b17716307400
• ocaml(Stdlib__Result) = e05eccba6c8a9e6816ad890e6e983d48
• ocaml(Stdlib__Scanf) = 33191b548042a7e51d81e7bc6af87e60
• ocaml(Stdlib__Seq) = b55b17884ef0dff6295517debe21f111
• ocaml(Stdlib__Set) = 878d51b56f0f7be3121d17ee49b6ece5
• ocaml(Stdlib__Stack) = 8c1adfb915ebcf7ee8b1cee69ad6daba
• ocaml(Stdlib__String) = 10f6a338df78df4f5987192086ffa3c9
• ocaml(Stdlib__Sys) = fb4c43482366ca204eebf7f3838d5a55
• ocaml(Stdlib__Uchar) = ffc32f05aeea05f14986ec532040e8b1
• ocaml(Stdlib__Weak) = 3a74e684389751cdee8098f5290a5966
• ocaml(Stm) = a147ac6f5850649f82fb7e994a2c349c
• ocaml(Stmargs) = 462b764f9d9861951fc67898db91fdbe
• ocaml(Store) = 1de301fb58a4f4a9e1840d4a1ecfbf59
• ocaml(Str) = b5c0844e743bd6ab6ab663d78320d76b
• ocaml(Structures) = c0b64cd89596f9c2add1c0cbf501fa18
• ocaml(Subproof) = 6fd89c1b5847e78a56cd7f8c87f375aa
• ocaml(Subst) = 606ff9923d3a48209170ec5a40976beb
• ocaml(Subtyping) = 995f83b3876060963c0d47fb1f65386f
• ocaml(Summary) = eba5dbcf0380a5a0175b6e2b4ef37bff
• ocaml(Synterp) = d04b79ca121c5f02e263fb6b00a4d228
• ocaml(System) = c99775fb648230fe0277be6fc1f560fc
• ocaml(TQueue) = f5dd9e61590dabf692140761335b6d05
• ocaml(Tacmach) = 3caff24ce522199377ed06f1f78c6846
• ocaml(Tacred) = fc826476111796ae05719a7f45b9d17f
• ocaml(TacticErrors) = 186fa0e25194c0270b0af7ddc28d4643
• ocaml(Tactic_option) = 903e29c22536f1d641b81fc4f1234fde
• ocaml(Tacticals) = b74df47a4e2c84d5f7adefcfb15c1c8f
• ocaml(Tactics) = 90200278890f08c1e71db6da9ed9f158
• ocaml(Tactypes) = a008b4a89d35e11ae902f494918e0362
• ocaml(Tauto_plugin) = 918e0931c7f126c9e170eada82956641
• ocaml(TemplateArity) = 91d03f02a66ace603df19f8b4fa6f886
• ocaml(Term) = f73d2d5d560684d4c4bc0a98ab57ba53
• ocaml(Terminal) = f585b9629763d534f04addb6a54b1b92
• ocaml(Termops) = fe256a798a72887abc49ab9ac3857576
• ocaml(Thread) = 66bcd6ecb19be0095ebf5c8ed8a06f20
• ocaml(Tok) = 3ffd6afd7e70452f6dc8715e8e920f5c
• ocaml(Top_printers) = 0e13cf3574600821a9a229a1ac57e7a0
• ocaml(Topfmt) = 43fa1cadd8b02dbf844a1e683ef269a3
• ocaml(Toploop) = 0306af3bed0f47279c3f9f537f5c2692
• ocaml(TransparentState) = 492fb566dd40324c3ac3c40c6a3eac3d
• ocaml(Trie) = 77dae95cd8ced6de91a944ccc80883c7
• ocaml(Tuto0_plugin) = 98bdc56d15b5bbc517025b43b94da4fa
• ocaml(Tuto0_plugin__Tuto0_main) = fcc3e4d0f7b1d44ce8cb90386c2a8d46
• ocaml(Tuto1_plugin) = 2c22f978ebb0f899a918fef075722aea
• ocaml(Tuto1_plugin__Inspector) = 2e59db5dd3d56912b5e7ac625ca61fbb
• ocaml(Tuto1_plugin__Simple_check) = 26c3aaab697e39029fe2053438577944
• ocaml(Tuto1_plugin__Simple_declare) = 1a9c5a18387f7f3df161da2b042ce703
• ocaml(Tuto1_plugin__Simple_print) = 7b804244772f2fe8812457b4d376e92e
• ocaml(Tuto2_plugin) = 1b262f332fc647494f840761b34da900
• ocaml(Tuto2_plugin__Counter) = 54706070f98f4e39dadb05e7b5064398
• ocaml(Tuto2_plugin__Custom) = aac9f3cb2f5254dd83298e0c66b4f3c4
• ocaml(Tuto2_plugin__Persistent_counter) = 3cd0f91503285b5c552d5d1869663487
• ocaml(Tuto3_plugin) = 825675f658e21cfe295cdaf265fb962f
• ocaml(Tuto3_plugin__Construction_game) = faf666d3d463b7e7f334086e6544bedf
• ocaml(Tuto3_plugin__Tuto_tactic) = dba5cb7a553ba8e47923099191c1c23f
• ocaml(Tuto4_plugin) = ee6f712d426c5b3bef435e3a182feb7b
• ocaml(Type_errors) = 0900c0a786876cf86bf2132b455a6392
• ocaml(Type_immediacy) = e4bd8d9064df3fd32bee7c871fb495f7
• ocaml(Typeclasses) = 0ce7badab68f775c8447bbb740e11c3a
• ocaml(Typeclasses_errors) = f3395c076f76826b544ad335d94b8a1f
• ocaml(Typeops) = 75a683b856b696dd76beddeb255d97cf
• ocaml(Types) = ee8cb6960cb32ea9e92d4f73174cce37
• ocaml(Typing) = 679c3972daf1d584878c6f3adf0be1e2
• ocaml(UGraph) = fd4fb27f84eb29897851009e5afeff5d
• ocaml(UState) = 2eb97c06d88ab64b5b1803ffdf5c4158
• ocaml(UVars) = 9173bf68da786badcc850fad917fa866
• ocaml(Uint63) = 9876a8b5a0ed526272adc8f269a8c8ab
• ocaml(Unicode) = a85dac65c40c8014b41dfbcadafe3ed1
• ocaml(Unicodetable) = 9b0791030b54609388bfa856c0d58db3
• ocaml(Unification) = c69d59750e13992563cc37bd287d70a3
• ocaml(Unionfind) = b23c4b3cf8231679fa6c9a94a6fec7e1
• ocaml(Unit_info) = 11cc0f955fa64ad827b34bfd76aa3d6e
• ocaml(Univ) = 3c2fe6798a168ef754f3af6682208113
• ocaml(UnivFlex) = f8b4b578e6d27536b25744c6babf53f0
• ocaml(UnivGen) = 7d6feeef8f86d48fd01ab29d7180c08a
• ocaml(UnivMinim) = 8bb24ec3a7429cb6ec6506547bf4f9be
• ocaml(UnivNames) = 309440d2098d9d2d3aa0d2a983800e06
• ocaml(UnivProblem) = d77df69e5dc8a5a4568e955487103237
• ocaml(UnivSubst) = 6f4bdafe0529b03a19a86d69a3e6a54e
• ocaml(Unix) = a088c1880ec9ae11d7b8ef8cdf3a21d7
• ocaml(UserWarn) = 66cacfd8009a321050bded2ce0a9fd11
• ocaml(Util) = 219a82943a407209300fd2eca83af94c
• ocaml(Values) = 45cafd9cf84d283e233b8fe611baf6fe
• ocaml(Vars) = 56a181095688f99c5303624a612df3fe
• ocaml(Vconv) = 876c4e05ec5cb143b7258c6748cf4088
• ocaml(Vcs) = 70ea92953d49948117fd7d240a855f4c
• ocaml(Vernac) = 8aa2b694892ca09e2cae98fa4cf91c9a
• ocaml(VernacControl) = 1f7655288d835224596e0a460b821ac5
• ocaml(Vernac_classifier) = 89fc29466b198c931f945f9d8ea6d108
• ocaml(Vernacentries) = 9131a1b46ac5394b8e9043fdf727fba9
• ocaml(Vernacexpr) = 67c5ddddeaee31b8c5d5b2557357607a
• ocaml(Vernacextend) = 0aba833874fd3eb6cb88101d9abbe56f
• ocaml(Vernacinterp) = 68c37129a1a4079dc67e04b5dffc5272
• ocaml(Vernacoptions) = 6c06b11338831e20f1e951cca2a19971
• ocaml(Vernacprop) = 4de3c5c8b61eb67741a908601480233b
• ocaml(Vernacstate) = ac3510912fe6bb959a7e52a79b6ba23a
• ocaml(Vernactypes) = c6cb3107f08b0a2d38bc11909eba19da
• ocaml(Vm) = 9e14d72de258c845c4939b4b9eef9541
• ocaml(Vmbytecodes) = d2a8610fa6ecb2844faea10b4e8fe16a
• ocaml(Vmbytegen) = 245fc6d67ad2e6b13d56f843ed91a807
• ocaml(Vmemitcodes) = 1ea3ce15bb933df35ea9a0fc0ab45c04
• ocaml(Vmerrors) = 69975c36a03dc6040406aebb257be755
• ocaml(Vmlambda) = 7197d58d07ba37dc0364af63d8c048ab
• ocaml(Vmlibrary) = 1abf8f71db3617eab8b38acc264c0602
• ocaml(Vmopcodes) = 7a5d219e38d56f8304834b93cf550f76
• ocaml(Vmsymtable) = 7d7685ad4957948b501082d1b1f889d5
• ocaml(Vmvalues) = c5815fac5c13273b8822d1d266db6182
• ocaml(Vnorm) = 72ccebf02b1442c57775b14d881002a6
• ocaml(Warnings) = 0cdc54c744998eb6c79312371851e8ba
• ocaml(WorkerPool) = 1c5bb8fdd244a7294e28cb8001308334
• ocaml(WriteOnceArray) = 14a1f30bda227a8fa2000e7e2ab978bb
• ocaml(Xml_datatype) = 1fc2a66ce0e39b30eb800beefd4367e7
• ocaml(Z) = 6f4dc1533ce2000c365adfd65d52b204
• ocaml(Zify_plugin) = 98e07f2e6d79a604ea4ce6a2f294b78a
• ocaml(Zify_plugin__Zify) = f53e802f24b4157ec70d26600f3c58a0
• rocq(aarch-64) = 9.2.0-2.fc45
• rpmlib(CompressedFileNames) <= 3.0.4-1
• rpmlib(FileDigests) <= 4.6.0-1
• rpmlib(PayloadFilesHavePrefix) <= 4.0-1
• rpmlib(PayloadIsZstd) <= 5.4.18-1
• rtld(GNU_HASH)

License

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

Changelog

* Thu Jul 09 2026 Jerry James <loganjerry@gmail.com> - 9.2.0-2
  - OCaml 5.5.0 rebuild
  - Add patch to adapt to dune 3.24
  - Fix rocq.xml
* Thu Apr 16 2026 Jerry James <loganjerry@gmail.com> - 9.2.0-1
  - Version 9.2.0
  - Drop upstreamed documentation patch
  - Enable the native compiler for x86_64
* Fri Mar 20 2026 Jerry James <loganjerry@gmail.com> - 9.1.1-1
  - Initial RPM

Files

/usr/bin/csdpcert
/usr/bin/ocamllibdep
/usr/bin/rocq
/usr/bin/rocq.byte
/usr/bin/rocqchk
/usr/bin/votour
/usr/lib/.build-id
/usr/lib/.build-id/0c
/usr/lib/.build-id/0c/572cde431ce5e5b92389ded5bb4bee99bde16d
/usr/lib/.build-id/12
/usr/lib/.build-id/12/e44ef22b5aff4c463dc3ad4229fcec2299518b
/usr/lib/.build-id/19
/usr/lib/.build-id/19/7c648abf5fb2eb4e5f0f067871c5aca31d43e1
/usr/lib/.build-id/19/d1822f528c71a36d8115993ac771307567fffe
/usr/lib/.build-id/1e
/usr/lib/.build-id/1e/34dc15923fcc5a2f9b305fd26d9696b17ecbd9
/usr/lib/.build-id/20
/usr/lib/.build-id/20/1d1217a8a4d47bbed013b5844aa31acbf688b8
/usr/lib/.build-id/23
/usr/lib/.build-id/23/813d6385662a103b25c5cc64a7a2994c4991a3
/usr/lib/.build-id/26
/usr/lib/.build-id/26/2cb45b1ee906220f7844cc9f0512129a322949
/usr/lib/.build-id/27
/usr/lib/.build-id/27/4da8ac7ee8a85dbe6a10214eab991314e6a785
/usr/lib/.build-id/30
/usr/lib/.build-id/30/eb2c162963ab45bfcce7a55b5d0b5b8fa33e68
/usr/lib/.build-id/33
/usr/lib/.build-id/33/ca39a70079ca56069ca3afd5933801fac716b8
/usr/lib/.build-id/35
/usr/lib/.build-id/35/99f44ff3d0444917d8fdeab52db749f22fcf26
/usr/lib/.build-id/3d
/usr/lib/.build-id/3d/b6d6a49611820f46999430b8d991e31051c061
/usr/lib/.build-id/3f
/usr/lib/.build-id/3f/7303588e1beff4ff4ae83865211aef25b1be14
/usr/lib/.build-id/45
/usr/lib/.build-id/45/c2bc4a052eb8dd6e0daf1b56b7b0ff0ca48de9
/usr/lib/.build-id/47
/usr/lib/.build-id/47/c5082eddfb59d5d90fce6702b158f13523056f
/usr/lib/.build-id/4c
/usr/lib/.build-id/4c/a4f4d9cc28fd31dcbaefbd4dbfbb8411221937
/usr/lib/.build-id/55
/usr/lib/.build-id/55/b315d105a2cba4afb1d49232380b76b72dfecd
/usr/lib/.build-id/5f
/usr/lib/.build-id/5f/69ce3521efff20c1eea522f40bcff66cbd0564
/usr/lib/.build-id/5f/8dd5b036b2f1ea860f4d818cb54f5f5da66765
/usr/lib/.build-id/65
/usr/lib/.build-id/65/a85bc110d472216931e38dd09740c3f8c89a58
/usr/lib/.build-id/71
/usr/lib/.build-id/71/f13100f2c1de94b2e11db2355f4dab8736f7af
/usr/lib/.build-id/73
/usr/lib/.build-id/73/451bab4014c6e541edf99e6553454a942929eb
/usr/lib/.build-id/74
/usr/lib/.build-id/74/4388acd00ac4da64af26b771ab0a7f1050bf0d
/usr/lib/.build-id/7a
/usr/lib/.build-id/7a/d2559f9160796320a2347c366682ce6fce155e
/usr/lib/.build-id/7b
/usr/lib/.build-id/7b/2b0248bcfef54238744ebd9f75e7d6a21bbd79
/usr/lib/.build-id/7c
/usr/lib/.build-id/7c/7e2fa1c0b68f27788ab9779b855ec725a88fa1
/usr/lib/.build-id/80
/usr/lib/.build-id/80/1227209527de06118bb62b8f1680e8d4523368
/usr/lib/.build-id/85
/usr/lib/.build-id/85/df2dcde1f1f7a90dd99ac979d043871b52559b
/usr/lib/.build-id/8a
/usr/lib/.build-id/8a/1fd796a4482f0270a4ef5501df167207e53b14
/usr/lib/.build-id/92
/usr/lib/.build-id/92/dc603badd77f8bd8ca6f0c8431d4e0af0ea8fa
/usr/lib/.build-id/9a
/usr/lib/.build-id/9a/d8bdfa0bdd43da65bb0c8a95b78a4b18cf074c
/usr/lib/.build-id/9b
/usr/lib/.build-id/9b/e93d6a19b0b7f1c01198e8a51b11316f5c61e2
/usr/lib/.build-id/9d
/usr/lib/.build-id/9d/a9caf2e5c244c59bef6b4c6713160749d7f203
/usr/lib/.build-id/a2
/usr/lib/.build-id/a2/1e5f4d1abccafa16f1bd0cb2980fafd5c07e10
/usr/lib/.build-id/a5
/usr/lib/.build-id/a5/fe55d3b6e7c2ad7e54538288b9d1598cdba499
/usr/lib/.build-id/a9
/usr/lib/.build-id/a9/e0f157be4aa8536d67f42dbd0954b1aef566fa
/usr/lib/.build-id/ac
/usr/lib/.build-id/ac/b87ddf1242146274890424354e336e862b50b7
/usr/lib/.build-id/af
/usr/lib/.build-id/af/8190e4ce29901528d27dc12ccc790673b4d38f
/usr/lib/.build-id/b5
/usr/lib/.build-id/b5/db3b77d51294254a5ca77303a74b581297c985
/usr/lib/.build-id/c0
/usr/lib/.build-id/c0/204cf38acedf772d7222038d5c0d4d6b7f1e71
/usr/lib/.build-id/c2
/usr/lib/.build-id/c2/2bdc82922778ccd713e273daebb5f3fccdd3d7
/usr/lib/.build-id/c2/7f9083efda32301cb9d763610dee1c4ce971a5
/usr/lib/.build-id/c5
/usr/lib/.build-id/c5/0e9de6959fd6a96c5e3595e1c724d4a93b40d2
/usr/lib/.build-id/c6
/usr/lib/.build-id/c6/2eedb83ede885424240fc953ff6147a65343c8
/usr/lib/.build-id/c6/87533471cf39de74d6f7abf3d9f04355de2f78
/usr/lib/.build-id/c8
/usr/lib/.build-id/c8/471076b1f075e19a2fe6ecc21b103fb4a4e897
/usr/lib/.build-id/ca
/usr/lib/.build-id/ca/45ca1e4d5b3d26baa7e30dcbde0caf8129c4b5
/usr/lib/.build-id/d0
/usr/lib/.build-id/d0/4951e27651f5dc5eaf730c40eb77ef5bbe22ad
/usr/lib/.build-id/d5
/usr/lib/.build-id/d5/4785aee7ca8b0d0059b731fe5a1149d78f5b9f
/usr/lib/.build-id/d7
/usr/lib/.build-id/d7/a34e293e81f68bee3364020369f86f7441fd96
/usr/lib/.build-id/da
/usr/lib/.build-id/da/3a81aa98c2be51056b8bf08a6286ed256b04b2
/usr/lib/.build-id/e7
/usr/lib/.build-id/e7/5b7722946844cd9392868fbb68329ed7ca4d06
/usr/lib/.build-id/e7/df56bb4f4f35651b0a42e74e556c91d95f7148
/usr/lib/.build-id/ec
/usr/lib/.build-id/ec/e4c9ca92f8120f515b78833d4bde50aac9abf5
/usr/lib/.build-id/f0
/usr/lib/.build-id/f0/c2feff6c57435c2b19f60db532ac4c7d12407f
/usr/lib/.build-id/f1
/usr/lib/.build-id/f1/b3d3436d4fc3c7d81ba4b92b4d39988492d271
/usr/lib/.build-id/f2
/usr/lib/.build-id/f2/f77d9f9780ce459145cf4808635e2d9bf34ee6
/usr/lib/.build-id/f3
/usr/lib/.build-id/f3/6f98eb609b3b93f98381476e08b1ec511d3ad2
/usr/lib/.build-id/f8
/usr/lib/.build-id/f8/039525f28dad040d2b79db7fc3b31582434ba5
/usr/lib/.build-id/f8/55defeaf3cdc85489533b34c43d361ef273a10
/usr/lib/.build-id/fc
/usr/lib/.build-id/fc/82c4133660b956c03a4739ec4c22b5bef36e54
/usr/lib/.build-id/fe
/usr/lib/.build-id/fe/4a076ea4d734b5504f86060fb42b6c84da41c4
/usr/lib64/ocaml/rocq-runtime
/usr/lib64/ocaml/rocq-runtime/META
/usr/lib64/ocaml/rocq-runtime/boot
/usr/lib64/ocaml/rocq-runtime/boot/boot.cma
/usr/lib64/ocaml/rocq-runtime/boot/boot.cmi
/usr/lib64/ocaml/rocq-runtime/boot/boot.cmxs
/usr/lib64/ocaml/rocq-runtime/boot/boot__Env.cmi
/usr/lib64/ocaml/rocq-runtime/boot/boot__Path.cmi
/usr/lib64/ocaml/rocq-runtime/boot/boot__Usage.cmi
/usr/lib64/ocaml/rocq-runtime/boot/boot__Util.cmi
/usr/lib64/ocaml/rocq-runtime/checklib
/usr/lib64/ocaml/rocq-runtime/checklib/coq_checklib.cma
/usr/lib64/ocaml/rocq-runtime/checklib/coq_checklib.cmi
/usr/lib64/ocaml/rocq-runtime/checklib/coq_checklib.cmxs
/usr/lib64/ocaml/rocq-runtime/checklib/coq_checklib__Analyze.cmi
/usr/lib64/ocaml/rocq-runtime/checklib/coq_checklib__CheckFlags.cmi
/usr/lib64/ocaml/rocq-runtime/checklib/coq_checklib__CheckInductive.cmi
/usr/lib64/ocaml/rocq-runtime/checklib/coq_checklib__CheckLibrary.cmi
/usr/lib64/ocaml/rocq-runtime/checklib/coq_checklib__Check_stat.cmi
/usr/lib64/ocaml/rocq-runtime/checklib/coq_checklib__Coqchk_main.cmi
/usr/lib64/ocaml/rocq-runtime/checklib/coq_checklib__Mod_checking.cmi
/usr/lib64/ocaml/rocq-runtime/checklib/coq_checklib__Safe_checking.cmi
/usr/lib64/ocaml/rocq-runtime/checklib/coq_checklib__Validate.cmi
/usr/lib64/ocaml/rocq-runtime/checklib/coq_checklib__Values.cmi
/usr/lib64/ocaml/rocq-runtime/clib
/usr/lib64/ocaml/rocq-runtime/clib/cArray.cmi
/usr/lib64/ocaml/rocq-runtime/clib/cEphemeron.cmi
/usr/lib64/ocaml/rocq-runtime/clib/cList.cmi
/usr/lib64/ocaml/rocq-runtime/clib/cMap.cmi
/usr/lib64/ocaml/rocq-runtime/clib/cObj.cmi
/usr/lib64/ocaml/rocq-runtime/clib/cSet.cmi
/usr/lib64/ocaml/rocq-runtime/clib/cSig.cmi
/usr/lib64/ocaml/rocq-runtime/clib/cString.cmi
/usr/lib64/ocaml/rocq-runtime/clib/cThread.cmi
/usr/lib64/ocaml/rocq-runtime/clib/cUnix.cmi
/usr/lib64/ocaml/rocq-runtime/clib/clib.cma
/usr/lib64/ocaml/rocq-runtime/clib/clib.cmxs
/usr/lib64/ocaml/rocq-runtime/clib/diff2.cmi
/usr/lib64/ocaml/rocq-runtime/clib/dyn.cmi
/usr/lib64/ocaml/rocq-runtime/clib/exninfo.cmi
/usr/lib64/ocaml/rocq-runtime/clib/hMap.cmi
/usr/lib64/ocaml/rocq-runtime/clib/hashcons.cmi
/usr/lib64/ocaml/rocq-runtime/clib/hashset.cmi
/usr/lib64/ocaml/rocq-runtime/clib/heap.cmi
/usr/lib64/ocaml/rocq-runtime/clib/iStream.cmi
/usr/lib64/ocaml/rocq-runtime/clib/int.cmi
/usr/lib64/ocaml/rocq-runtime/clib/memprof_coq.cmi
/usr/lib64/ocaml/rocq-runtime/clib/monad.cmi
/usr/lib64/ocaml/rocq-runtime/clib/mutex_aux.cmi
/usr/lib64/ocaml/rocq-runtime/clib/neList.cmi
/usr/lib64/ocaml/rocq-runtime/clib/option.cmi
/usr/lib64/ocaml/rocq-runtime/clib/orderedType.cmi
/usr/lib64/ocaml/rocq-runtime/clib/polyMap.cmi
/usr/lib64/ocaml/rocq-runtime/clib/predicate.cmi
/usr/lib64/ocaml/rocq-runtime/clib/range.cmi
/usr/lib64/ocaml/rocq-runtime/clib/sList.cmi
/usr/lib64/ocaml/rocq-runtime/clib/segmenttree.cmi
/usr/lib64/ocaml/rocq-runtime/clib/store.cmi
/usr/lib64/ocaml/rocq-runtime/clib/terminal.cmi
/usr/lib64/ocaml/rocq-runtime/clib/trie.cmi
/usr/lib64/ocaml/rocq-runtime/clib/unicode.cmi
/usr/lib64/ocaml/rocq-runtime/clib/unicodetable.cmi
/usr/lib64/ocaml/rocq-runtime/clib/unionfind.cmi
/usr/lib64/ocaml/rocq-runtime/clib/writeOnceArray.cmi
/usr/lib64/ocaml/rocq-runtime/config
/usr/lib64/ocaml/rocq-runtime/config/byte
/usr/lib64/ocaml/rocq-runtime/config/byte/byte_config.cma
/usr/lib64/ocaml/rocq-runtime/config/byte/coq_byte_config.cmi
/usr/lib64/ocaml/rocq-runtime/config/config.cma
/usr/lib64/ocaml/rocq-runtime/config/config.cmxs
/usr/lib64/ocaml/rocq-runtime/config/coq_config.cmi
/usr/lib64/ocaml/rocq-runtime/coqargs
/usr/lib64/ocaml/rocq-runtime/coqargs/coqargs.cma
/usr/lib64/ocaml/rocq-runtime/coqargs/coqargs.cmi
/usr/lib64/ocaml/rocq-runtime/coqargs/coqargs.cmxs
/usr/lib64/ocaml/rocq-runtime/coqdeplib
/usr/lib64/ocaml/rocq-runtime/coqdeplib/coqdeplib.cma
/usr/lib64/ocaml/rocq-runtime/coqdeplib/coqdeplib.cmi
/usr/lib64/ocaml/rocq-runtime/coqdeplib/coqdeplib.cmxs
/usr/lib64/ocaml/rocq-runtime/coqdeplib/coqdeplib__Args.cmi
/usr/lib64/ocaml/rocq-runtime/coqdeplib/coqdeplib__Common.cmi
/usr/lib64/ocaml/rocq-runtime/coqdeplib/coqdeplib__Dep_info.cmi
/usr/lib64/ocaml/rocq-runtime/coqdeplib/coqdeplib__Error.cmi
/usr/lib64/ocaml/rocq-runtime/coqdeplib/coqdeplib__File_util.cmi
/usr/lib64/ocaml/rocq-runtime/coqdeplib/coqdeplib__Fl.cmi
/usr/lib64/ocaml/rocq-runtime/coqdeplib/coqdeplib__Lexer.cmi
/usr/lib64/ocaml/rocq-runtime/coqdeplib/coqdeplib__Loadpath.cmi
/usr/lib64/ocaml/rocq-runtime/coqdeplib/coqdeplib__Makefile.cmi
/usr/lib64/ocaml/rocq-runtime/coqdeplib/coqdeplib__Rocqdep_main.cmi
/usr/lib64/ocaml/rocq-runtime/coqworkmgrapi
/usr/lib64/ocaml/rocq-runtime/coqworkmgrapi/coqworkmgrApi.cma
/usr/lib64/ocaml/rocq-runtime/coqworkmgrapi/coqworkmgrApi.cmi
/usr/lib64/ocaml/rocq-runtime/coqworkmgrapi/coqworkmgrApi.cmxs
/usr/lib64/ocaml/rocq-runtime/debugger_support
/usr/lib64/ocaml/rocq-runtime/debugger_support/debugger_support.cma
/usr/lib64/ocaml/rocq-runtime/debugger_support/debugger_support.cmi
/usr/lib64/ocaml/rocq-runtime/debugger_support/debugger_support.cmxs
/usr/lib64/ocaml/rocq-runtime/dev
/usr/lib64/ocaml/rocq-runtime/dev/dev.cma
/usr/lib64/ocaml/rocq-runtime/dev/dev.cmxs
/usr/lib64/ocaml/rocq-runtime/dev/ml_toplevel
/usr/lib64/ocaml/rocq-runtime/dev/ml_toplevel/include
/usr/lib64/ocaml/rocq-runtime/dev/ml_toplevel/include_directories
/usr/lib64/ocaml/rocq-runtime/dev/ml_toplevel/include_printers
/usr/lib64/ocaml/rocq-runtime/dev/ml_toplevel/include_utilities
/usr/lib64/ocaml/rocq-runtime/dev/top_printers.cmi
/usr/lib64/ocaml/rocq-runtime/dev/vm_printers.cmi
/usr/lib64/ocaml/rocq-runtime/engine
/usr/lib64/ocaml/rocq-runtime/engine/eConstr.cmi
/usr/lib64/ocaml/rocq-runtime/engine/engine.cma
/usr/lib64/ocaml/rocq-runtime/engine/engine.cmxs
/usr/lib64/ocaml/rocq-runtime/engine/evar_kinds.cmi
/usr/lib64/ocaml/rocq-runtime/engine/evarnames.cmi
/usr/lib64/ocaml/rocq-runtime/engine/evarutil.cmi
/usr/lib64/ocaml/rocq-runtime/engine/evd.cmi
/usr/lib64/ocaml/rocq-runtime/engine/ftactic.cmi
/usr/lib64/ocaml/rocq-runtime/engine/logic_monad.cmi
/usr/lib64/ocaml/rocq-runtime/engine/namegen.cmi
/usr/lib64/ocaml/rocq-runtime/engine/nameops.cmi
/usr/lib64/ocaml/rocq-runtime/engine/polyFlags.cmi
/usr/lib64/ocaml/rocq-runtime/engine/profile_tactic.cmi
/usr/lib64/ocaml/rocq-runtime/engine/proofview.cmi
/usr/lib64/ocaml/rocq-runtime/engine/proofview_monad.cmi
/usr/lib64/ocaml/rocq-runtime/engine/termops.cmi
/usr/lib64/ocaml/rocq-runtime/engine/uState.cmi
/usr/lib64/ocaml/rocq-runtime/engine/univFlex.cmi
/usr/lib64/ocaml/rocq-runtime/engine/univGen.cmi
/usr/lib64/ocaml/rocq-runtime/engine/univMinim.cmi
/usr/lib64/ocaml/rocq-runtime/engine/univNames.cmi
/usr/lib64/ocaml/rocq-runtime/engine/univProblem.cmi
/usr/lib64/ocaml/rocq-runtime/engine/univSubst.cmi
/usr/lib64/ocaml/rocq-runtime/gramlib
/usr/lib64/ocaml/rocq-runtime/gramlib/gramlib.cma
/usr/lib64/ocaml/rocq-runtime/gramlib/gramlib.cmi
/usr/lib64/ocaml/rocq-runtime/gramlib/gramlib.cmxs
/usr/lib64/ocaml/rocq-runtime/gramlib/gramlib__Gramext.cmi
/usr/lib64/ocaml/rocq-runtime/gramlib/gramlib__Grammar.cmi
/usr/lib64/ocaml/rocq-runtime/gramlib/gramlib__LStream.cmi
/usr/lib64/ocaml/rocq-runtime/gramlib/gramlib__Plexing.cmi
/usr/lib64/ocaml/rocq-runtime/gramlib/gramlib__Stream.cmi
/usr/lib64/ocaml/rocq-runtime/interp
/usr/lib64/ocaml/rocq-runtime/interp/abbreviation.cmi
/usr/lib64/ocaml/rocq-runtime/interp/constrexpr.cmi
/usr/lib64/ocaml/rocq-runtime/interp/constrexpr_ops.cmi
/usr/lib64/ocaml/rocq-runtime/interp/constrextern.cmi
/usr/lib64/ocaml/rocq-runtime/interp/constrintern.cmi
/usr/lib64/ocaml/rocq-runtime/interp/decls.cmi
/usr/lib64/ocaml/rocq-runtime/interp/dumpglob.cmi
/usr/lib64/ocaml/rocq-runtime/interp/genintern.cmi
/usr/lib64/ocaml/rocq-runtime/interp/impargs.cmi
/usr/lib64/ocaml/rocq-runtime/interp/implicit_quantifiers.cmi
/usr/lib64/ocaml/rocq-runtime/interp/interp.cma
/usr/lib64/ocaml/rocq-runtime/interp/interp.cmxs
/usr/lib64/ocaml/rocq-runtime/interp/modintern.cmi
/usr/lib64/ocaml/rocq-runtime/interp/notation.cmi
/usr/lib64/ocaml/rocq-runtime/interp/notation_ops.cmi
/usr/lib64/ocaml/rocq-runtime/interp/notation_term.cmi
/usr/lib64/ocaml/rocq-runtime/interp/notationextern.cmi
/usr/lib64/ocaml/rocq-runtime/interp/numTok.cmi
/usr/lib64/ocaml/rocq-runtime/interp/primNotations.cmi
/usr/lib64/ocaml/rocq-runtime/interp/reserve.cmi
/usr/lib64/ocaml/rocq-runtime/interp/smartlocate.cmi
/usr/lib64/ocaml/rocq-runtime/kernel
/usr/lib64/ocaml/rocq-runtime/kernel/cClosure.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/cPrimitives.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/constant_typing.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/constr.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/context.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/conv_oracle.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/conversion.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/cooking.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/declarations.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/declareops.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/discharge.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/entries.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/environ.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/esubst.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/evar.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/float64.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/float64_common.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/genlambda.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/hConstr.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/indTyping.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/indtypes.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/inductive.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/inferCumulativity.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/kernel.cma
/usr/lib64/ocaml/rocq-runtime/kernel/kernel.cmxs
/usr/lib64/ocaml/rocq-runtime/kernel/mod_declarations.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/mod_subst.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/mod_typing.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/modops.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/names.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/nativecode.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/nativeconv.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/nativelambda.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/nativelib.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/nativelibrary.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/nativevalues.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/opaqueproof.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/pConstraints.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/parray.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/partial_subst.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/primred.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/pstring.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/qGraph.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/redFlags.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/reduction.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/relevanceops.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/retroknowledge.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/rtree.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/safe_typing.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/section.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/sorts.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/subtyping.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/term.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/transparentState.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/type_errors.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/typeops.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/uGraph.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/uVars.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/uint63.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/univ.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/values.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/vars.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/vconv.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/vm.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/vmbytecodes.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/vmbytegen.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/vmemitcodes.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/vmerrors.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/vmlambda.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/vmlibrary.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/vmopcodes.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/vmsymtable.cmi
/usr/lib64/ocaml/rocq-runtime/kernel/vmvalues.cmi
/usr/lib64/ocaml/rocq-runtime/lib
/usr/lib64/ocaml/rocq-runtime/lib/acyclicGraph.cmi
/usr/lib64/ocaml/rocq-runtime/lib/aux_file.cmi
/usr/lib64/ocaml/rocq-runtime/lib/cAst.cmi
/usr/lib64/ocaml/rocq-runtime/lib/cDebug.cmi
/usr/lib64/ocaml/rocq-runtime/lib/cErrors.cmi
/usr/lib64/ocaml/rocq-runtime/lib/cWarnings.cmi
/usr/lib64/ocaml/rocq-runtime/lib/control.cmi
/usr/lib64/ocaml/rocq-runtime/lib/coqProject_file.cmi
/usr/lib64/ocaml/rocq-runtime/lib/dAst.cmi
/usr/lib64/ocaml/rocq-runtime/lib/deprecation.cmi
/usr/lib64/ocaml/rocq-runtime/lib/envars.cmi
/usr/lib64/ocaml/rocq-runtime/lib/feedback.cmi
/usr/lib64/ocaml/rocq-runtime/lib/flags.cmi
/usr/lib64/ocaml/rocq-runtime/lib/hook.cmi
/usr/lib64/ocaml/rocq-runtime/lib/instr.cmi
/usr/lib64/ocaml/rocq-runtime/lib/lib.cma
/usr/lib64/ocaml/rocq-runtime/lib/lib.cmxs
/usr/lib64/ocaml/rocq-runtime/lib/loc.cmi
/usr/lib64/ocaml/rocq-runtime/lib/newProfile.cmi
/usr/lib64/ocaml/rocq-runtime/lib/objFile.cmi
/usr/lib64/ocaml/rocq-runtime/lib/pp.cmi
/usr/lib64/ocaml/rocq-runtime/lib/pp_diff.cmi
/usr/lib64/ocaml/rocq-runtime/lib/quickfix.cmi
/usr/lib64/ocaml/rocq-runtime/lib/spawn.cmi
/usr/lib64/ocaml/rocq-runtime/lib/stateid.cmi
/usr/lib64/ocaml/rocq-runtime/lib/system.cmi
/usr/lib64/ocaml/rocq-runtime/lib/userWarn.cmi
/usr/lib64/ocaml/rocq-runtime/lib/util.cmi
/usr/lib64/ocaml/rocq-runtime/lib/xml_datatype.cmi
/usr/lib64/ocaml/rocq-runtime/library
/usr/lib64/ocaml/rocq-runtime/library/coqlib.cmi
/usr/lib64/ocaml/rocq-runtime/library/global.cmi
/usr/lib64/ocaml/rocq-runtime/library/globnames.cmi
/usr/lib64/ocaml/rocq-runtime/library/goptions.cmi
/usr/lib64/ocaml/rocq-runtime/library/lib.cmi
/usr/lib64/ocaml/rocq-runtime/library/libnames.cmi
/usr/lib64/ocaml/rocq-runtime/library/libobject.cmi
/usr/lib64/ocaml/rocq-runtime/library/library.cma
/usr/lib64/ocaml/rocq-runtime/library/library.cmxs
/usr/lib64/ocaml/rocq-runtime/library/library_info.cmi
/usr/lib64/ocaml/rocq-runtime/library/locality.cmi
/usr/lib64/ocaml/rocq-runtime/library/nametab.cmi
/usr/lib64/ocaml/rocq-runtime/library/rocqlib.cmi
/usr/lib64/ocaml/rocq-runtime/library/summary.cmi
/usr/lib64/ocaml/rocq-runtime/parsing
/usr/lib64/ocaml/rocq-runtime/parsing/cLexer.cmi
/usr/lib64/ocaml/rocq-runtime/parsing/extend.cmi
/usr/lib64/ocaml/rocq-runtime/parsing/g_constr.cmi
/usr/lib64/ocaml/rocq-runtime/parsing/g_prim.cmi
/usr/lib64/ocaml/rocq-runtime/parsing/notation_gram.cmi
/usr/lib64/ocaml/rocq-runtime/parsing/notgram_ops.cmi
/usr/lib64/ocaml/rocq-runtime/parsing/parsing.cma
/usr/lib64/ocaml/rocq-runtime/parsing/parsing.cmxs
/usr/lib64/ocaml/rocq-runtime/parsing/pcoq.cmi
/usr/lib64/ocaml/rocq-runtime/parsing/procq.cmi
/usr/lib64/ocaml/rocq-runtime/parsing/tok.cmi
/usr/lib64/ocaml/rocq-runtime/perf
/usr/lib64/ocaml/rocq-runtime/perf/coqperf.cma
/usr/lib64/ocaml/rocq-runtime/perf/coqperf.cmxs
/usr/lib64/ocaml/rocq-runtime/perf/perf.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/btauto
/usr/lib64/ocaml/rocq-runtime/plugins/btauto/btauto_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/btauto/btauto_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/btauto/btauto_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/btauto/btauto_plugin__G_btauto.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/btauto/btauto_plugin__Refl_btauto.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/cc
/usr/lib64/ocaml/rocq-runtime/plugins/cc/cc_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/cc/cc_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/cc/cc_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/cc/cc_plugin__G_congruence.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/cc_core
/usr/lib64/ocaml/rocq-runtime/plugins/cc_core/cc_core_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/cc_core/cc_core_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/cc_core/cc_core_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/cc_core/cc_core_plugin__Ccalgo.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/cc_core/cc_core_plugin__Ccprojectability.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/cc_core/cc_core_plugin__Ccproof.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/cc_core/cc_core_plugin__Cctac.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/derive
/usr/lib64/ocaml/rocq-runtime/plugins/derive/derive_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/derive/derive_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/derive/derive_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/derive/derive_plugin__Derive.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/derive/derive_plugin__G_derive.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/extraction
/usr/lib64/ocaml/rocq-runtime/plugins/extraction/extraction_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/extraction/extraction_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/extraction/extraction_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/extraction/extraction_plugin__Common.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/extraction/extraction_plugin__Extract_env.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/extraction/extraction_plugin__Extraction.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/extraction/extraction_plugin__G_extraction.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/extraction/extraction_plugin__Haskell.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/extraction/extraction_plugin__Json.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/extraction/extraction_plugin__Miniml.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/extraction/extraction_plugin__Mlutil.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/extraction/extraction_plugin__Modutil.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/extraction/extraction_plugin__Ocaml.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/extraction/extraction_plugin__Scheme.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/extraction/extraction_plugin__Table.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/firstorder
/usr/lib64/ocaml/rocq-runtime/plugins/firstorder/firstorder_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/firstorder/firstorder_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/firstorder/firstorder_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/firstorder/firstorder_plugin__G_ground.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/firstorder_core
/usr/lib64/ocaml/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin__Formula.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin__Ground.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin__Instances.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin__Rules.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin__Sequent.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/firstorder_core/firstorder_core_plugin__Unify.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/funind
/usr/lib64/ocaml/rocq-runtime/plugins/funind/funind_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/funind/funind_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/funind/funind_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/funind/funind_plugin__Functional_principles_proofs.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/funind/funind_plugin__Functional_principles_types.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/funind/funind_plugin__G_indfun.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/funind/funind_plugin__Gen_principle.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/funind/funind_plugin__Glob_term_to_relation.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/funind/funind_plugin__Glob_termops.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/funind/funind_plugin__Indfun.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/funind/funind_plugin__Indfun_common.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/funind/funind_plugin__Invfun.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/funind/funind_plugin__Recdef.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__ComRewrite.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__Coretactics.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__Extraargs.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__Extratactics.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__G_auto.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__G_class.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__G_eqdecide.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__G_ltac.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__G_rewrite.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__G_tactic.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__Internals.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__Leminv.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__Pltac.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__Pptactic.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__Profile_ltac_tactics.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__Tacarg.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__Taccoerce.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__Tacentries.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__Tacenv.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__Tacexpr.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__Tacintern.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__Tacinterp.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__Tacsubst.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__Tactic_debug.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac/ltac_plugin__Tactic_matching.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin__G_ltac2.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2bt.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2core.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2dyn.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2entries.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2env.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2expr.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2externals.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2extffi.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2extravals.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2ffi.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2intern.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2interp.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2match.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2print.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2qexpr.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2quote.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2stdlib.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2tactics.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2types.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2typing_env.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2/ltac2_plugin__Tac2val.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2_ltac1
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2_ltac1/ltac2_ltac1_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2_ltac1/ltac2_ltac1_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2_ltac1/ltac2_ltac1_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2_ltac1/ltac2_ltac1_plugin__G_ltac2_ltac1.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2_ltac1/ltac2_ltac1_plugin__Tac2core_ltac1.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2_ltac1/ltac2_ltac1_plugin__Tac2quote_ltac1.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ltac2_ltac1/ltac2_ltac1_plugin__Tac2stdlib_ltac1.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/micromega
/usr/lib64/ocaml/rocq-runtime/plugins/micromega/micromega_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/micromega/micromega_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/micromega/micromega_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/micromega/micromega_plugin__Certificate.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/micromega/micromega_plugin__Coq_micromega.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/micromega/micromega_plugin__G_micromega.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/micromega/micromega_plugin__Itv.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/micromega/micromega_plugin__Linsolve.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/micromega/micromega_plugin__Persistent_cache.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/micromega/micromega_plugin__Polynomial.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/micromega/micromega_plugin__Simplex.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/micromega/micromega_plugin__Vect.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/micromega_core
/usr/lib64/ocaml/rocq-runtime/plugins/micromega_core/micromega_core_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/micromega_core/micromega_core_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/micromega_core/micromega_core_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/micromega_core/micromega_core_plugin__Micromega.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/micromega_core/micromega_core_plugin__Mutils.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/micromega_core/micromega_core_plugin__NumCompat.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/micromega_core/micromega_core_plugin__Sos.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/micromega_core/micromega_core_plugin__Sos_lib.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/micromega_core/micromega_core_plugin__Sos_types.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/nsatz
/usr/lib64/ocaml/rocq-runtime/plugins/nsatz/nsatz_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/nsatz/nsatz_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/nsatz/nsatz_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/nsatz/nsatz_plugin__G_nsatz.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/nsatz_core
/usr/lib64/ocaml/rocq-runtime/plugins/nsatz_core/nsatz_core_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/nsatz_core/nsatz_core_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/nsatz_core/nsatz_core_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/nsatz_core/nsatz_core_plugin__Ideal.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/nsatz_core/nsatz_core_plugin__Nsatz.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/nsatz_core/nsatz_core_plugin__Polynom.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/nsatz_core/nsatz_core_plugin__Utile.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/number_string_notation
/usr/lib64/ocaml/rocq-runtime/plugins/number_string_notation/number_string_notation_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/number_string_notation/number_string_notation_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/number_string_notation/number_string_notation_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/number_string_notation/number_string_notation_plugin__G_number_string.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/number_string_notation/number_string_notation_plugin__Number_string.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ring
/usr/lib64/ocaml/rocq-runtime/plugins/ring/ring_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/ring/ring_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ring/ring_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/ring/ring_plugin__G_ring.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ring/ring_plugin__Ring.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ring/ring_plugin__Ring_ast.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/rtauto
/usr/lib64/ocaml/rocq-runtime/plugins/rtauto/rtauto_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/rtauto/rtauto_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/rtauto/rtauto_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/rtauto/rtauto_plugin__G_rtauto.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/rtauto/rtauto_plugin__Proof_search.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/rtauto/rtauto_plugin__Refl_tauto.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ssreflect
/usr/lib64/ocaml/rocq-runtime/plugins/ssreflect/ssreflect_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/ssreflect/ssreflect_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ssreflect/ssreflect_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrast.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrbwd.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrcommon.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrelim.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrequality.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrfwd.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssripats.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrparser.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrprinters.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrtacs.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrtacticals.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrvernac.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ssreflect/ssreflect_plugin__Ssrview.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ssrmatching
/usr/lib64/ocaml/rocq-runtime/plugins/ssrmatching/ssrmatching_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/ssrmatching/ssrmatching_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ssrmatching/ssrmatching_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/ssrmatching/ssrmatching_plugin__G_ssrmatching.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/ssrmatching/ssrmatching_plugin__Ssrmatching.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/tauto
/usr/lib64/ocaml/rocq-runtime/plugins/tauto/tauto_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/tauto/tauto_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/tauto/tauto_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/tauto/tauto_plugin__Tauto.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p0
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p0/tuto0_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p0/tuto0_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p0/tuto0_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p0/tuto0_plugin__G_tuto0.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p0/tuto0_plugin__Tuto0_main.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p1
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p1/tuto1_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p1/tuto1_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p1/tuto1_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p1/tuto1_plugin__G_tuto1.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p1/tuto1_plugin__Inspector.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p1/tuto1_plugin__Simple_check.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p1/tuto1_plugin__Simple_declare.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p1/tuto1_plugin__Simple_print.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p2
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p2/tuto2_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p2/tuto2_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p2/tuto2_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p2/tuto2_plugin__Counter.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p2/tuto2_plugin__Custom.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p2/tuto2_plugin__G_tuto2.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p2/tuto2_plugin__Persistent_counter.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p3
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p3/tuto3_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p3/tuto3_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p3/tuto3_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p3/tuto3_plugin__Construction_game.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p3/tuto3_plugin__G_tuto3.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p3/tuto3_plugin__Tuto_tactic.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p4
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p4/tuto4_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p4/tuto4_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p4/tuto4_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/tutorial/p4/tuto4_plugin__Myexternals.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/zify
/usr/lib64/ocaml/rocq-runtime/plugins/zify/zify_plugin.cma
/usr/lib64/ocaml/rocq-runtime/plugins/zify/zify_plugin.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/zify/zify_plugin.cmxs
/usr/lib64/ocaml/rocq-runtime/plugins/zify/zify_plugin__G_zify.cmi
/usr/lib64/ocaml/rocq-runtime/plugins/zify/zify_plugin__Zify.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping
/usr/lib64/ocaml/rocq-runtime/pretyping/arguments_renaming.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/cases.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/cbv.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/coercion.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/coercionops.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/combinators.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/constr_matching.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/detyping.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/evaluable.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/evarconv.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/evardefine.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/evarsolve.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/find_subterm.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/genarg.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/geninterp.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/gensubst.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/globEnv.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/glob_ops.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/glob_term.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/heads.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/inductiveops.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/keys.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/libBinding.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/locus.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/locusops.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/ltac_pretype.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/nativenorm.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/pattern.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/patternops.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/pretype_errors.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/pretyping.cma
/usr/lib64/ocaml/rocq-runtime/pretyping/pretyping.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/pretyping.cmxs
/usr/lib64/ocaml/rocq-runtime/pretyping/printingFlags.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/program.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/reductionops.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/retyping.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/structures.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/tacred.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/templateArity.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/typeclasses.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/typeclasses_errors.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/typing.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/unification.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/vnorm.cmi
/usr/lib64/ocaml/rocq-runtime/printing
/usr/lib64/ocaml/rocq-runtime/printing/genprint.cmi
/usr/lib64/ocaml/rocq-runtime/printing/ppconstr.cmi
/usr/lib64/ocaml/rocq-runtime/printing/ppextend.cmi
/usr/lib64/ocaml/rocq-runtime/printing/pputils.cmi
/usr/lib64/ocaml/rocq-runtime/printing/printer.cmi
/usr/lib64/ocaml/rocq-runtime/printing/printing.cma
/usr/lib64/ocaml/rocq-runtime/printing/printing.cmxs
/usr/lib64/ocaml/rocq-runtime/printing/proof_diffs.cmi
/usr/lib64/ocaml/rocq-runtime/proofs
/usr/lib64/ocaml/rocq-runtime/proofs/clenv.cmi
/usr/lib64/ocaml/rocq-runtime/proofs/goal_select.cmi
/usr/lib64/ocaml/rocq-runtime/proofs/logic.cmi
/usr/lib64/ocaml/rocq-runtime/proofs/miscprint.cmi
/usr/lib64/ocaml/rocq-runtime/proofs/proof.cmi
/usr/lib64/ocaml/rocq-runtime/proofs/proof_bullet.cmi
/usr/lib64/ocaml/rocq-runtime/proofs/proofs.cma
/usr/lib64/ocaml/rocq-runtime/proofs/proofs.cmxs
/usr/lib64/ocaml/rocq-runtime/proofs/refine.cmi
/usr/lib64/ocaml/rocq-runtime/proofs/subproof.cmi
/usr/lib64/ocaml/rocq-runtime/proofs/tacmach.cmi
/usr/lib64/ocaml/rocq-runtime/proofs/tactypes.cmi
/usr/lib64/ocaml/rocq-runtime/revision
/usr/lib64/ocaml/rocq-runtime/rocqnative
/usr/lib64/ocaml/rocq-runtime/rocqshim
/usr/lib64/ocaml/rocq-runtime/rocqshim/rocqshim.cma
/usr/lib64/ocaml/rocq-runtime/rocqshim/rocqshim.cmi
/usr/lib64/ocaml/rocq-runtime/rocqshim/rocqshim.cmxs
/usr/lib64/ocaml/rocq-runtime/rocqworker
/usr/lib64/ocaml/rocq-runtime/rocqworker.byte
/usr/lib64/ocaml/rocq-runtime/rocqworker_with_drop
/usr/lib64/ocaml/rocq-runtime/stm
/usr/lib64/ocaml/rocq-runtime/stm/asyncTaskQueue.cmi
/usr/lib64/ocaml/rocq-runtime/stm/dag.cmi
/usr/lib64/ocaml/rocq-runtime/stm/partac.cmi
/usr/lib64/ocaml/rocq-runtime/stm/proofBlockDelimiter.cmi
/usr/lib64/ocaml/rocq-runtime/stm/spawned.cmi
/usr/lib64/ocaml/rocq-runtime/stm/stm.cma
/usr/lib64/ocaml/rocq-runtime/stm/stm.cmi
/usr/lib64/ocaml/rocq-runtime/stm/stm.cmxs
/usr/lib64/ocaml/rocq-runtime/stm/stmargs.cmi
/usr/lib64/ocaml/rocq-runtime/stm/tQueue.cmi
/usr/lib64/ocaml/rocq-runtime/stm/vcs.cmi
/usr/lib64/ocaml/rocq-runtime/stm/workerPool.cmi
/usr/lib64/ocaml/rocq-runtime/sysinit
/usr/lib64/ocaml/rocq-runtime/sysinit/coqinit.cmi
/usr/lib64/ocaml/rocq-runtime/sysinit/coqloadpath.cmi
/usr/lib64/ocaml/rocq-runtime/sysinit/sysinit.cma
/usr/lib64/ocaml/rocq-runtime/sysinit/sysinit.cmxs
/usr/lib64/ocaml/rocq-runtime/tactics
/usr/lib64/ocaml/rocq-runtime/tactics/abstract.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/allScheme.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/auto.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/autorewrite.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/btermdn.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/cbn.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/class_tactics.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/contradiction.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/declareScheme.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/dn.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/eClause.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/eauto.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/elim.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/elimschemes.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/eqdecide.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/eqschemes.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/equality.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/evar_tactics.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/fixTactics.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/generalize.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/genredexpr.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/gentactic.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/hints.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/hipattern.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/ind_tables.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/indrec.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/induction.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/inv.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/ppred.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/redexpr.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/redops.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/rewrite.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/stdarg.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/tacticErrors.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/tacticals.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/tactics.cma
/usr/lib64/ocaml/rocq-runtime/tactics/tactics.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/tactics.cmxs
/usr/lib64/ocaml/rocq-runtime/tools
/usr/lib64/ocaml/rocq-runtime/tools/CoqMakefile.in
/usr/lib64/ocaml/rocq-runtime/tools/TimeFileMaker.py
/usr/lib64/ocaml/rocq-runtime/tools/coqdoc
/usr/lib64/ocaml/rocq-runtime/tools/coqdoc/coqdoc.css
/usr/lib64/ocaml/rocq-runtime/tools/coqdoc/coqdoc.sty
/usr/lib64/ocaml/rocq-runtime/tools/make-both-single-timing-files.py
/usr/lib64/ocaml/rocq-runtime/tools/make-both-time-files.py
/usr/lib64/ocaml/rocq-runtime/tools/make-one-time-file.py
/usr/lib64/ocaml/rocq-runtime/toplevel
/usr/lib64/ocaml/rocq-runtime/toplevel/ccompile.cmi
/usr/lib64/ocaml/rocq-runtime/toplevel/colors.cmi
/usr/lib64/ocaml/rocq-runtime/toplevel/common_compile.cmi
/usr/lib64/ocaml/rocq-runtime/toplevel/coqc.cmi
/usr/lib64/ocaml/rocq-runtime/toplevel/coqcargs.cmi
/usr/lib64/ocaml/rocq-runtime/toplevel/coqloop.cmi
/usr/lib64/ocaml/rocq-runtime/toplevel/coqrc.cmi
/usr/lib64/ocaml/rocq-runtime/toplevel/coqtop.cmi
/usr/lib64/ocaml/rocq-runtime/toplevel/g_toplevel.cmi
/usr/lib64/ocaml/rocq-runtime/toplevel/load.cmi
/usr/lib64/ocaml/rocq-runtime/toplevel/memtrace_init.cmi
/usr/lib64/ocaml/rocq-runtime/toplevel/toplevel.cma
/usr/lib64/ocaml/rocq-runtime/toplevel/toplevel.cmxs
/usr/lib64/ocaml/rocq-runtime/toplevel/vernac.cmi
/usr/lib64/ocaml/rocq-runtime/toplevel/workerLoop.cmi
/usr/lib64/ocaml/rocq-runtime/vernac
/usr/lib64/ocaml/rocq-runtime/vernac/assumptions.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/attributes.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/auto_ind_decl.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/canonical.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/classes.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/comArguments.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/comAssumption.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/comCoercion.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/comDefinition.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/comExtraDeps.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/comFixpoint.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/comHints.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/comInductive.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/comPrimitive.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/comRewriteRule.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/comSearch.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/comTactic.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/debugHook.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/declare.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/declareInd.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/declareUniv.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/declaremods.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/egramml.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/egramrocq.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/future.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/g_obligations.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/g_proofs.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/g_redexpr.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/g_vernac.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/himsg.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/indschemes.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/library.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/loadpath.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/metasyntax.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/mltop.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/opaques.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/ppvernac.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/prettyp.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/printmod.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/proof_using.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/pvernac.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/recLemmas.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/record.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/retrieveObl.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/search.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/synterp.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/tactic_option.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/topfmt.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/vernac.cma
/usr/lib64/ocaml/rocq-runtime/vernac/vernac.cmxs
/usr/lib64/ocaml/rocq-runtime/vernac/vernacControl.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/vernac_classifier.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/vernacentries.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/vernacexpr.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/vernacextend.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/vernacinterp.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/vernacoptions.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/vernacprop.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/vernacstate.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/vernactypes.cmi
/usr/lib64/ocaml/rocq-runtime/vm
/usr/lib64/ocaml/rocq-runtime/vm/coqrun.cma
/usr/lib64/ocaml/rocq-runtime/vm/coqrun.cmi
/usr/lib64/ocaml/rocq-runtime/vm/coqrun.cmxs
/usr/lib64/ocaml/stublibs/dllcoqperf_stubs.so
/usr/lib64/ocaml/stublibs/dllcoqrun_stubs.so
/usr/share/doc/rocq-runtime
/usr/share/doc/rocq-runtime/README.md
/usr/share/licenses/rocq-runtime
/usr/share/licenses/rocq-runtime/LICENSE
/usr/share/man/man1/rocq.1.gz
/usr/share/man/man1/rocqchk.1.gz
/usr/share/texlive/texmf-dist/tex/latex/misc
/usr/share/texlive/texmf-dist/tex/latex/misc/coqdoc.sty

Generated by rpm2html 1.8.1

Fabrice Bellet, Mon Jul 13 22:44:02 2026