rocq-runtime-9.1.1-1.fc44 RPM for ppc64le

From Fedora 44 for ppc64le / r

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

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

Provides

• rocq-runtime
• coq-core
• ocaml(Abbreviation)
• ocaml(Abstract)
• ocaml(AcyclicGraph)
• ocaml(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(Coqdeplib__Static_toplevel_libs)
• 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(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(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(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__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(Parray)
• ocaml(Partac)
• ocaml(Partial_subst)
• ocaml(Pattern)
• ocaml(Patternops)
• ocaml(Pcoq)
• ocaml(Perf)
• 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(Primred)
• ocaml(Printer)
• 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(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(Subtyping)
• ocaml(Summary)
• ocaml(Synterp)
• ocaml(System)
• ocaml(TQueue)
• ocaml(Tacmach)
• ocaml(Tacred)
• 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(Xml_datatype)
• ocaml(Zify_plugin)
• ocaml(Zify_plugin__G_zify)
• ocaml(Zify_plugin__Zify)
• rocq-runtime(ppc-64)

Requires

• /usr/bin/ocamlrun
• /usr/bin/python3
• ld64.so.2()(64bit)
• ld64.so.2(GLIBC_2.22)(64bit)
• libc.so.6()(64bit)
• libc.so.6(GLIBC_2.17)(64bit)
• libc.so.6(GLIBC_2.25)(64bit)
• libc.so.6(GLIBC_2.28)(64bit)
• libc.so.6(GLIBC_2.32)(64bit)
• libc.so.6(GLIBC_2.33)(64bit)
• libc.so.6(GLIBC_2.34)(64bit)
• libc.so.6(GLIBC_2.38)(64bit)
• libc.so.6(GLIBC_2.42)(64bit)
• libc.so.6(GLIBC_ABI_DT_RELR)(64bit)
• libgmp.so.10()(64bit)
• libm.so.6()(64bit)
• libm.so.6(GLIBC_2.17)(64bit)
• libm.so.6(GLIBC_2.29)(64bit)
• libm.so.6(GLIBC_2.35)(64bit)
• libm.so.6(GLIBC_2.38)(64bit)
• ocaml(Abbreviation) = 3d585238df32d77987bc0412da374066
• ocaml(Abstract) = dce637fb6a9b4b0cdab2f688eb2abe89
• ocaml(AcyclicGraph) = 9e0518132292ba200eec41bfa795f956
• ocaml(Arguments_renaming) = dd1fbb9e7a9e0988f74a3587bd5575be
• ocaml(Assumptions) = 1545782cbf5fbf2b4de533d34bb1242c
• ocaml(Asttypes) = e507ef6e691c55af686b09bd398e52fe
• ocaml(AsyncTaskQueue) = c2c76e34bd65fad7f95570f1f5d3810d
• ocaml(Attributes) = 9b35ec78323c573681dcdea2e0e1da4f
• ocaml(Auto) = f2a52f7ec115ce7658e8471db9873498
• ocaml(Auto_ind_decl) = 2c6fb53af45575d44e58925cf3cc3f1b
• ocaml(Autorewrite) = 8fef4021e85b9fd98f66ae9aa6b1f9d8
• ocaml(Aux_file) = 80391d3302cfd4395c115333517cd26e
• ocaml(Big_int_Z) = d6cb9e1c54060ad10e28f7ba86ae266a
• ocaml(Boot) = c10d1826ec03550bc542cef705e8a113
• ocaml(Boot__Env) = bebf7c9de90d368d0c86ae7d4ef8635a
• ocaml(Boot__Path) = db34ea431173f9ae4c5adf48124456ea
• ocaml(Boot__Usage) = 38a803d96d64d1260891320e63e0a08b
• ocaml(Boot__Util) = 7ba9a906ee0085778ce0b96e0afcfde3
• ocaml(Btauto_plugin) = 021f47edaa1c3dcd96029f3b21dd4a96
• ocaml(Btauto_plugin__Refl_btauto) = be5da81a805eef6699b550beda20b54e
• ocaml(Btermdn) = df8d0f8e8ce275732deadc35ef1971d5
• ocaml(Build_path_prefix_map) = e0f5cdd3ea76275f8c562bce411ee08b
• ocaml(CArray) = a2e455be7013ec529edc7deeb9c88dcd
• ocaml(CAst) = f6d00920bd24c55bb173a1ab0212e577
• ocaml(CClosure) = 40258bca9f5938d5244d17fd50a9e079
• ocaml(CDebug) = 7f2e1a015766edd1310ed03bf997b5bf
• ocaml(CEphemeron) = 7cae4867455538660558bdff12463859
• ocaml(CErrors) = a39311cc209c60b13d5492af985c5437
• ocaml(CLexer) = b2d2eb5ae372a7bbd8619187f63b39a4
• ocaml(CList) = 0de21becae3d402b63e131798333d505
• ocaml(CMap) = d8df1ab91a0cf1bc2bb100f53ca23222
• ocaml(CObj) = 2adb6c04a1dd1ddff801b115e6e3dfd6
• ocaml(CPrimitives) = d549748a4fc2389450389beb8ba38467
• ocaml(CSet) = c99ec5a860a1db040e3cb46a4ef41cff
• ocaml(CSig) = 8cb23fa269471e19f2cc9161ba3980d0
• ocaml(CString) = 6ccd68e56971762e4417e8eabadc5ea9
• ocaml(CThread) = c04f6295803e585cd503bd0078828dee
• ocaml(CUnix) = f6850de84f62fe0043b8f44ae8b780c8
• ocaml(CWarnings) = b26e9bfccd48436bbcd67a4036bebd44
• ocaml(CamlinternalFormat) = 70bcbb90ec668384a2248434bb2eb1ab
• ocaml(CamlinternalFormatBasics) = bb23651112c1e05c61498d902472830d
• ocaml(CamlinternalLazy) = 321f83e197d23ef3129f66a139b9829f
• ocaml(CamlinternalMod) = 091e0f55942111b1b8c378809123a052
• ocaml(Canonical) = 56ec3cc9dfa523f3950f64c4139003d8
• ocaml(Cases) = acca1833300735cfa4486aecca57ad7b
• ocaml(Cbn) = 2337c257bc0fa25eeaa3dad66620ecbe
• ocaml(Cbv) = 247b37cfff3484131668d5bc873db533
• ocaml(Cc_core_plugin) = 7221186ffe2b1d4feeb3b619e5518b5b
• ocaml(Cc_core_plugin__Ccalgo) = b96d8465e1a1d57dbae86b7c02801fb1
• ocaml(Cc_core_plugin__Ccprojectability) = 3a4b0d08997febbaeae75f68877a74e4
• ocaml(Cc_core_plugin__Ccproof) = eb615068e61de5101b9f5fae28b9ff90
• ocaml(Cc_core_plugin__Cctac) = c36d022ec7e1d7427e64131a9bb73cc2
• ocaml(Cc_plugin) = ace7197075e417f45053eabc4ecb5148
• ocaml(Ccompile) = a151d1521188f18d460e3f6a8299a464
• ocaml(Class_tactics) = dd5f9fd70ada03853d04217a2c467843
• ocaml(Classes) = 6e7604524a58ea3ace3d2aa17d4d7cf7
• ocaml(Clenv) = ea4bec1b845443b8b55e901985667c3a
• ocaml(Clflags) = 1e5696f0c01b2a0894699729b9bf930a
• ocaml(Cmi_format) = af4e87c82d2bb018b25d798368662790
• ocaml(Coercion) = 647f35f66b095be4831353a32183a586
• ocaml(Coercionops) = e6a7bad6595d5eefdbd30f0ad20eda63
• ocaml(Colors) = f64d1bac25e83f529dca98fcd2183c24
• ocaml(ComArguments) = 2b7395e3fe1243ddf665793f17126857
• ocaml(ComAssumption) = b8e07e75d20567eb906ac5f91dfc39e2
• ocaml(ComCoercion) = 6540c46941f9e02f769b97043fd94ac0
• ocaml(ComDefinition) = 28d7788d42133a406ff2275401644d59
• ocaml(ComExtraDeps) = 3851489593b0fe76cbebdeee8b0c5988
• ocaml(ComFixpoint) = d6650c007121fadf25a411befbb06bd5
• ocaml(ComHints) = 158f82962173aa039c3a6621b8f1ce8f
• ocaml(ComInductive) = 2780267462e0a06429d1c6019b6061dc
• ocaml(ComPrimitive) = 884aadc6f2222bcd70f929510630abda
• ocaml(ComRewriteRule) = 1e7e49e4c4cb14d51d47f9a85a8a201d
• ocaml(ComSearch) = 7aac536dd41cc94d548f90399a0e28a4
• ocaml(ComTactic) = fbf02ce640d1d69a38df2b948eac985e
• ocaml(Combinators) = 424e433328ac5bbd58b96135abd0629e
• ocaml(Common_compile) = 8b9f1ab2504e41a1a73402d8199ec792
• ocaml(Compenv) = c5b2a25f63b81e35600f80ebdc868b4b
• ocaml(Constant_typing) = f3dd68d745b0e8571c9fd738072b61db
• ocaml(Constr) = 227a83c618e5c078dac57963506b381a
• ocaml(Constr_matching) = 2ef9e05f0938aec3e76fc2736f08a7b8
• ocaml(Constrexpr) = 5da6217dfa3c35d751c3006938679521
• ocaml(Constrexpr_ops) = 51f64f68443c51a622a0e20273f493de
• ocaml(Constrextern) = 5db59e2af49aa53922fb292fd59422e9
• ocaml(Constrintern) = 48c0ed1c7cd610a25ca031883f56642f
• ocaml(Context) = 24fe2677ff0f1668a2af38f90c020782
• ocaml(Contradiction) = 444fec6eba33b1498f9edb4618ae8dd6
• ocaml(Control) = ea49f573046a09f58239c7c422d27682
• ocaml(Conv_oracle) = 915c6e4b6b5e53e5197d3acc8abcd818
• ocaml(Conversion) = 7fd22293e2c0c3f3685bf181053706d2
• ocaml(Cooking) = 3142e0452502e215aeed877a44fcd817
• ocaml(CoqProject_file) = 88f02f03103b88830d4ada291869936a
• ocaml(Coq_checklib) = 2baf09a1c451962aa0d821a3fdd11db5
• ocaml(Coq_checklib__Analyze) = 83361539cce55e3551b4cf869801cbcf
• ocaml(Coq_checklib__CheckFlags) = 7255e596eed027c1234c435ff66d7f8f
• ocaml(Coq_checklib__CheckInductive) = ffcd6ac675d52d212fc01554f73eabfb
• ocaml(Coq_checklib__CheckLibrary) = 923b6140fc7ca8da2e8e8b45db2245ab
• ocaml(Coq_checklib__Check_stat) = ac12b29780df77ae93c2919b05ab54f0
• ocaml(Coq_checklib__Mod_checking) = 04b55fdbf6d91cba687273fd5c20d244
• ocaml(Coq_checklib__Safe_checking) = bf887c82768c0f687831c282af777753
• ocaml(Coq_checklib__Validate) = ad1a44e6c3fd2bd40f5ee2efa483b7c8
• ocaml(Coq_checklib__Values) = 0e0d1b05633b37f4cda113582947eb1a
• ocaml(Coq_config) = d757a4ce8cef8bc8ac402d4052453e6e
• ocaml(Coqargs) = a2c5bc0139ea8298665ae4f7441f48f4
• ocaml(Coqcargs) = 5ba2daec45526727061bed4f34fc8f0a
• ocaml(Coqdeplib) = dc1d7e03b4344a4138207d34ac781ccb
• ocaml(Coqdeplib__Args) = 7978ab8f00e41b7aa42a8058890c5e15
• ocaml(Coqdeplib__Common) = 0a23636ce7ff7eb41fcc1da5b400b2d7
• ocaml(Coqdeplib__Dep_info) = 987d267a6b461770dfcddc0793048700
• ocaml(Coqdeplib__Error) = d66c3b0c7050dc0d15f6b31f01acc6e3
• ocaml(Coqdeplib__File_util) = ad07372615ddaa9aac6921a6907eb304
• ocaml(Coqdeplib__Fl) = 61c16aead40a29c9b2815ce31f486d23
• ocaml(Coqdeplib__Lexer) = 381f9c96e8cfa917ec7077aadb3c1997
• ocaml(Coqdeplib__Loadpath) = e5916035935099e2b4c813b843419b15
• ocaml(Coqdeplib__Makefile) = 8419c34e42f237d97e9c227b6e44a19d
• ocaml(Coqdeplib__Static_toplevel_libs) = 9afa8b68144879b0c836b068fcac1cd3
• ocaml(Coqinit) = 40f5b2d2bc8ce164bc84521d99c3c21c
• ocaml(Coqloadpath) = ac92e3e05a7e4f8c9d86cc5fe94db635
• ocaml(Coqloop) = 7d1ba6f0887b4f9e0f56e40eb6f94221
• ocaml(Coqrc) = 45ccec5688f862bdaed8c239b882e172
• ocaml(Coqtop) = 2906ce1694d974148389c20f27a55c57
• ocaml(CoqworkmgrApi) = bf9291ab65d50704790e0ce2f6f3b962
• ocaml(DAst) = dfe8298509e157009558d4e8012a58d7
• ocaml(Dag) = 7e85dc3bd26aa26d7f1582df587d5618
• ocaml(Data_types) = 9f178cf8e1e58dacbc1ab559802bb5d5
• ocaml(DebugHook) = 4a0b419408abdbaad3466f51bd079051
• ocaml(Declarations) = bac5e6ef131dcb14878cee2385889283
• ocaml(Declare) = cb4df514e8b92f6d9fdfb2a2c2624e3b
• ocaml(DeclareInd) = df21741c474e36f7b4459595b1110f80
• ocaml(DeclareScheme) = 7aa39294ad400bbbc532d9b452e442e4
• ocaml(DeclareUniv) = 650f1db61d27e7d9dbe1b2d2cbb205a6
• ocaml(Declaremods) = 099f21e7f55d343ada68e93b2aa84363
• ocaml(Declareops) = 541c72e928d107b40758838c298c7f50
• ocaml(Decls) = 9e24c8f267edc996ffdf9e8793972e6a
• ocaml(Deprecation) = 6255b65b96686c13284f6724268aad6a
• ocaml(Derive_plugin) = cfa1f7052a4b7c1f11cf5d3c30e00cf2
• ocaml(Derive_plugin__Derive) = 570950f79300176e513f1464531b91c6
• ocaml(Detyping) = 17692cf48cbec191ab80fbcd39378e5c
• ocaml(Diff2) = 8940429ed83ad199f81a27ff5df3fadc
• ocaml(Discharge) = bbbbcd94590ebe0ecc1630e0af74e356
• ocaml(Dn) = f8f3a88ab1ade13c85ae0378e1148817
• ocaml(Dumpglob) = 9412e1da7ea8591f47cd0b033980a532
• ocaml(Dyn) = f0cdf5756549bfb2f13af24fa17b15ff
• ocaml(Dynlink) = 08e1461841151b2dfdeeb2b217719fea
• ocaml(EClause) = b534ffef5651b046b70fea3dd4ad0908
• ocaml(EConstr) = efbe845cb1bfc10b8ae2b5ed0f08294c
• ocaml(Eauto) = a53e71e4cc1e5a3bdf29029cfec0ec42
• ocaml(Egramml) = 893e11b53767b078a62bba926b78d49f
• ocaml(Egramrocq) = dc4085dd0400c9bb332ecb60abbe0a14
• ocaml(Elim) = 7eb165d1cafa7394a588d2834b5499e4
• ocaml(Elimschemes) = a61ac5cc316103ef053a08e88782b5a0
• ocaml(Entries) = 0fc9a00c5cfef2ee486ae07057005b3b
• ocaml(Env) = 0cdf66ea216efe371c58a7976afe2075
• ocaml(Envars) = fc8d9acafb03dbdf0cf9bd347b88c21f
• ocaml(Environ) = dfcc992935128e554bc15d60187b3069
• ocaml(Eqdecide) = e3690ecf46e3de985b2a1289d29a69dd
• ocaml(Eqschemes) = f2f915e7a3a56aceca5ca91622e60f40
• ocaml(Equality) = 8c400458930077a47f719bbb7134431d
• ocaml(Esubst) = b37f3ffca63215b8141d151bb2a8b5af
• ocaml(Evaluable) = 34f828307011a98d4cfd4dd8f7fb5e26
• ocaml(Evar) = 5c12d3020e6c58f5eec50fd86ffb3278
• ocaml(Evar_kinds) = 361b786772c4686cad25fc63ab28e850
• ocaml(Evar_tactics) = 249dc13897ebee8f9ccd932fa1df9785
• ocaml(Evarconv) = 4c954b36bb98607fca9cf0848862909d
• ocaml(Evardefine) = 0d687db12fa7b1edd9ab1434b81b5c6c
• ocaml(Evarsolve) = 128dc3c2e1880f11b89a29f030936ad9
• ocaml(Evarutil) = 1b23cf6f6b45c693a77d7cdbbe764c23
• ocaml(Evd) = 1cdc7b2ace4e21a4e8d35ba112606d4a
• ocaml(Exninfo) = 95e7f938070548b5b5d750588295e6db
• ocaml(Extend) = 38d4d5ec9c49591537557ab8a87414f4
• ocaml(Extraction_plugin) = 45385a433336b20d3b91e013e59f2671
• ocaml(Extraction_plugin__Common) = b6abdd2c561b1f0a93a63f2ebac0ff2c
• ocaml(Extraction_plugin__Extract_env) = 3ba5af752983ae758cc29642c9e2038f
• ocaml(Extraction_plugin__Extraction) = 96e5b38b566f6878271ede4e11c521e8
• ocaml(Extraction_plugin__Haskell) = 0192cb45f29bf117e18ade5632618c61
• ocaml(Extraction_plugin__Json) = cedf77d385a759ce2464a4edb9782ccd
• ocaml(Extraction_plugin__Miniml) = 77249bd2bcd683f537cc07bfc0d75490
• ocaml(Extraction_plugin__Mlutil) = 4292abca2f088be44fee44053d4f29d9
• ocaml(Extraction_plugin__Modutil) = e241621bbc0f6c2d28fae598624a7919
• ocaml(Extraction_plugin__Ocaml) = f8151831c224316363f5b14577b730f9
• ocaml(Extraction_plugin__Scheme) = 649450122d90fc4833cb9e2726b2b813
• ocaml(Extraction_plugin__Table) = 5d94209c481dbe8c46de9aa83fa1fc5e
• ocaml(Feedback) = 747950a142a2a3b06505c9203be8ca69
• ocaml(Find_subterm) = 9abcb5d78b34f8ab3116b78db7097486
• ocaml(Findlib) = a5fc3db70ae71cda44eb0da93e094eb2
• ocaml(Firstorder_core_plugin) = 117b378e702191a4f2b1921366b5a21f
• ocaml(Firstorder_core_plugin__Formula) = 3d6327ebec80a76caa8dd4c49a26fe0d
• ocaml(Firstorder_core_plugin__Ground) = d7e92442c3eb83be26f4ea75e1aeb02d
• ocaml(Firstorder_core_plugin__Instances) = c27dc2ecf9419d5ea5f6d314ba843559
• ocaml(Firstorder_core_plugin__Rules) = 33f263738bfa1cc77de153ac3710a72a
• ocaml(Firstorder_core_plugin__Sequent) = 4629687112bf309f43cdb60de927d726
• ocaml(Firstorder_core_plugin__Unify) = 2f1a62d74a8ee87815ac22fc4e7436a8
• ocaml(Firstorder_plugin) = de43944fb21b3ca4a0fdc2c59c4173d1
• ocaml(Fl_metascanner) = f2833d59fc6fb9013774ad16022f6e1f
• ocaml(Fl_metatoken) = c52aa6baf9d82887fc926a04bacae69b
• ocaml(Fl_package_base) = b49943184674c704462363ed948c27f6
• ocaml(Flags) = fc81870f2e60f48ff4de6c9953744b5f
• ocaml(Float64) = e3af59c461d447770a9513d585363662
• ocaml(Float64_common) = 8bb3514a86d9aa53eca574fb5a08dba4
• ocaml(Format_doc) = e9bc76d69e0a38952eeb83c757a95d18
• ocaml(Ftactic) = 80eda42280e194706d79e167b51fceea
• ocaml(Funind_plugin) = 478d36ea9a949ae615ecf6f234e67878
• ocaml(Funind_plugin__Functional_principles_proofs) = 720e5f711700ecb79e7c84f9ed2dd0f3
• ocaml(Funind_plugin__Functional_principles_types) = fac0faa9e39db48fd598745283f5c769
• ocaml(Funind_plugin__Gen_principle) = 5f9a05121717b5839725f1efcbcfe5da
• ocaml(Funind_plugin__Glob_term_to_relation) = 5660f4d8062316d655aca7bb57009981
• ocaml(Funind_plugin__Glob_termops) = 5a66fbefbc2216149cf200c17b082535
• ocaml(Funind_plugin__Indfun) = e05d0ff43387ef32cb1bf717334a3339
• ocaml(Funind_plugin__Indfun_common) = effee1c4df3219b9c2402b6af9a19faf
• ocaml(Funind_plugin__Invfun) = ea3ed124073c88fc7761632b347ef8b8
• ocaml(Funind_plugin__Recdef) = 5e8d9fad3e0ca7cf09fe3cfe99efcc9d
• ocaml(Future) = 0834bf495a97d13fe3d43454740f6994
• ocaml(G_constr) = 29e265e344998f76822e7a7fa418c6b0
• ocaml(G_proofs) = bfc5925d4f5cca985a177b33864959c7
• ocaml(G_redexpr) = 3b45b23eb162cde9f1d7a7a86cf8b050
• ocaml(G_toplevel) = e240bc71ddcf4768a6dd2706ed66f441
• ocaml(G_vernac) = 513338d507570e6e4b0e19208e7b5ea0
• ocaml(Genarg) = 5e9fff5c5aaa70fb66fcaf19783060f3
• ocaml(Generalize) = 91c837ccd7f7e31b5fe766cb573b9385
• ocaml(Genintern) = bdfda363041a833c921c6b3faccc5b69
• ocaml(Geninterp) = 03d885001350bbbfbba611f1586db156
• ocaml(Genlambda) = 7246cc240ef97522f7aceb935ff2027c
• ocaml(Genprint) = f9c1e27d5bdc248c393db13c74b49bf6
• ocaml(Genredexpr) = 05d841fd5ee0ffb318c2ea0a1b060cfb
• ocaml(Gensubst) = d8ce3f530105e98c0927957d0db81613
• ocaml(Gentactic) = ff66716fb750480ebcc99a317dff8c09
• ocaml(GlobEnv) = 2dde3cff831542394b7f5916835157af
• ocaml(Glob_ops) = 8055f98b4dfdc80ec4eb4de80593d793
• ocaml(Glob_term) = 6461f98552d4a3e06901dea34e98e3e7
• ocaml(Global) = f8038357420bb2256764b90a7ed13295
• ocaml(Globnames) = 0775d2413d1635e5ce656fbbf3ba0dda
• ocaml(Goal_select) = dd33b16e4221bd23aa2f8bdb2f7ffe10
• ocaml(Goptions) = 4c98f796e98c87dcc9f089272c9c8374
• ocaml(Gramlib) = ae39fd0bb86764a48d691d550ddeb9d2
• ocaml(Gramlib__Gramext) = ba4c816f6cb6f42379b555865db4b4fd
• ocaml(Gramlib__Grammar) = 81ec8fbd0f822077f269017f10108f87
• ocaml(Gramlib__LStream) = 49c3277367980cc05f266369c85b998f
• ocaml(Gramlib__Plexing) = dd6a02af091586921630b85e311e25cb
• ocaml(Gramlib__Stream) = 93cd148ded6ee5ffbbc971afc9c02d42
• ocaml(HConstr) = 7859c50340ca613113e7e9e2e524a8f3
• ocaml(HMap) = 809701de4a3651c0788d2967c526cb88
• ocaml(Hashcons) = d9da5b4a5d48cabeddb2878692bf1fce
• ocaml(Hashset) = f2a941d55c9ded6be6c8f9026ec7a921
• ocaml(Heads) = 9e78d467b76bccae034b966b8685228a
• ocaml(Heap) = 4f083d427cb30e39d3d786a1cf292eaa
• ocaml(Himsg) = 517d02d86e7dd8d04f27fcf2ae89e545
• ocaml(Hints) = 5365215248373c140b11006c8448afca
• ocaml(Hipattern) = 90897a32f972c2bfc5a281d0b4bee974
• ocaml(Hook) = f86461414dc1ef72fcb0b45bed7f95ce
• ocaml(IStream) = 2da469b3f4ce192ed5a5dc8fab75ced2
• ocaml(Ident) = 61cbd919c8f6ef60ced7ecbe7fb6faf5
• ocaml(Identifiable) = 8621bc2814d3f193b9cab59619693489
• ocaml(Impargs) = d07dd45a72c797138a995d18b0406d2a
• ocaml(Implicit_quantifiers) = a7b0a13a5f9e45ba99904c84e39fbe8a
• ocaml(IndTyping) = 947d149c2b6914b5955868d7ea84f6f4
• ocaml(Ind_tables) = 3a702238b8067e338c913f7e5e6b9b11
• ocaml(Indrec) = 9b84d4783f619aadbad156f82fa9975b
• ocaml(Indschemes) = 6b7bd93d44df0bcfcc93d5d16a429a06
• ocaml(Indtypes) = ecefbf610bb2ca02c8bb664ca3099726
• ocaml(Induction) = 0ff78f4c52cf47cd430c64aec748f1db
• ocaml(Inductive) = a79fe08d7f52e4b5b71031a20c9bd835
• ocaml(Inductiveops) = 1ae70d9c63637cdfd4637d4c3e31e26a
• ocaml(InferCumulativity) = 9e8a4924786fb6da36a5719856040a7e
• ocaml(Instr) = 82b17b769bc0349c36beeb461e0ca02d
• ocaml(Int) = 88f311a03d57180dbb31c55fea3304a2
• ocaml(Inv) = f74d03d17ff1ff760f16fd60a9948580
• ocaml(Keys) = 02a516e9db3dab9d7f793f5f164061ca
• ocaml(Lib) = 9a330cf6806f6a552822f4ced2f3ae15
• ocaml(Libnames) = ecd953038363385ca8f46345f785d72d
• ocaml(Libobject) = 766b042073e3b3c07dfe91d1629615b8
• ocaml(Library) = 34084b0fec6a3dbe8b7b09411e84c9f9
• ocaml(Library_info) = 1658e19dc4eb399867fad13b7c0176c3
• ocaml(Load) = 58b0a34d7edbf60c52429b2ec0b1fd53
• ocaml(Load_path) = 311833dc50b7f0117c7580122e8b521b
• ocaml(Loadpath) = 3c1e0a55c152c87b9edf3817104e8b46
• ocaml(Loc) = ffb3e7b210af621f9edf1d0515b9fddb
• ocaml(Locality) = 612b747db62cdc9f438dfa8ee04ac8d7
• ocaml(Location) = 1f3b4a14027aa1c3d06755358fe40ab9
• ocaml(Locus) = 8807da5f5c042e96584470973aff404f
• ocaml(Locusops) = 77710774f1e0fe449a8ca1dd78be0d71
• ocaml(Logic) = 8707501bb98f1fe5008b250b7234fbf9
• ocaml(Logic_monad) = db3b617ffc94115bbc34a20f466d27ba
• ocaml(Longident) = 4fec6bb94016657f43f91bd096f27b38
• ocaml(Ltac2_ltac1_plugin) = f36ee64104bf7571ca1347ac2369081a
• ocaml(Ltac2_ltac1_plugin__Tac2quote_ltac1) = 1df175c745820fffaa00a914f7fd3be8
• ocaml(Ltac2_plugin) = ecbccae8d1b0e61d26457d4797e36c66
• ocaml(Ltac2_plugin__G_ltac2) = c4e54cfd19af71e224d0eeca186e9e76
• ocaml(Ltac2_plugin__Tac2bt) = 738260e4509cf0ebbbb55e0b5995cce8
• ocaml(Ltac2_plugin__Tac2core) = 408e4f9c781efac24f09f62c2ff28962
• ocaml(Ltac2_plugin__Tac2dyn) = d24f3728f40d60794f81ccbd13ec36ca
• ocaml(Ltac2_plugin__Tac2entries) = 102b3be0c5804433b911cbc9344dde53
• ocaml(Ltac2_plugin__Tac2env) = 27cf58279cf6e2d51dbeb73fc64ebb14
• ocaml(Ltac2_plugin__Tac2expr) = 3f9a69c15965eb427b6117734ec1e0da
• ocaml(Ltac2_plugin__Tac2externals) = 1fd3bcfb1c9fa1ed008baf22413d4d9e
• ocaml(Ltac2_plugin__Tac2extffi) = 24a4b5a29408faec71f9dccad962ff41
• ocaml(Ltac2_plugin__Tac2ffi) = baab19746958b4e5ad826f23bba76c88
• ocaml(Ltac2_plugin__Tac2intern) = 4be4d9ad610b8c7739431095fa206c21
• ocaml(Ltac2_plugin__Tac2interp) = 80759e2d0e979ccc5796f3712261adbf
• ocaml(Ltac2_plugin__Tac2match) = a135e486c4a9b7a198cd2e19929c267f
• ocaml(Ltac2_plugin__Tac2print) = acbdf3633a06bef5e9fed18fc9c65455
• ocaml(Ltac2_plugin__Tac2qexpr) = f6ea0912df8c9a802044f7fdbe8557f6
• ocaml(Ltac2_plugin__Tac2quote) = 3dd0395cd4d6116d58b190104a1588cb
• ocaml(Ltac2_plugin__Tac2stdlib) = b0a68119ebfec792dc76a3032abbc328
• ocaml(Ltac2_plugin__Tac2tactics) = 67bc83f0b8c8463eebafebe8136a164c
• ocaml(Ltac2_plugin__Tac2types) = 8671af3051e13a4ffd7dd5f95a037640
• ocaml(Ltac2_plugin__Tac2typing_env) = b9074f73e180395ee5fe55376c4147cc
• ocaml(Ltac2_plugin__Tac2val) = a0e813cce7c904718b0648904ae2a8de
• ocaml(Ltac_plugin) = 5409ef6e2f1819f62566d425aa6b978f
• ocaml(Ltac_plugin__ComRewrite) = 779aad2ae89c1c0eabd398e36121f8dc
• ocaml(Ltac_plugin__Extraargs) = e87eb5cbc73aa8a46e6285ca83782b15
• ocaml(Ltac_plugin__G_ltac) = 0d928e49d08ee2c7790e4b219c734976
• ocaml(Ltac_plugin__Internals) = ff6f7579ea2eeea85548aef5bee52d73
• ocaml(Ltac_plugin__Leminv) = 762a257966941ae7f97637971c0885d6
• ocaml(Ltac_plugin__Pltac) = 5b6d3500442a65e2f8a8c1b39d8f6031
• ocaml(Ltac_plugin__Pptactic) = 322cb859586a3dc2e6a83c7d9f009057
• ocaml(Ltac_plugin__Tacarg) = bc921bab893b23cb1dafe23bbc69f1f3
• ocaml(Ltac_plugin__Taccoerce) = 32ce142c956cf0b677aa556a6c73224a
• ocaml(Ltac_plugin__Tacentries) = 7cf92b5ef58c10b7bd817defb823a92d
• ocaml(Ltac_plugin__Tacenv) = 3b79b2e6b02e471a4f93a6744796362f
• ocaml(Ltac_plugin__Tacexpr) = 15f5cf3eabc9819053aab31bdfff269b
• ocaml(Ltac_plugin__Tacintern) = bb4425849e171f8d27a7a012f37b2ca9
• ocaml(Ltac_plugin__Tacinterp) = fef9dfd449787a92a7e75819a43a64aa
• ocaml(Ltac_plugin__Tacsubst) = fd7954fd08b8b7c1071c81a810604940
• ocaml(Ltac_plugin__Tactic_debug) = 75125fa6461c4d0fa3e958344a071c79
• ocaml(Ltac_plugin__Tactic_matching) = 95560b3786cc4602caa4af23061f3745
• ocaml(Ltac_pretype) = 51e6c168750a923536e6f663c30d4636
• ocaml(Memprof_coq) = 52002a7377d174641891b3bb807cfac4
• ocaml(Memtrace_init) = 767bc231aec961de2ef9b3b9c923a001
• ocaml(Metasyntax) = dea6cf071d488ef4326026cdce478528
• ocaml(Micromega_core_plugin) = 7431add2f7d94df09a1d16829af126c7
• ocaml(Micromega_core_plugin__Micromega) = 71eec3b72c1bc19482934ced988a0111
• ocaml(Micromega_core_plugin__Mutils) = 1a771d55f1eb75dcb6bf1c6298f25a43
• ocaml(Micromega_core_plugin__NumCompat) = b4521a7b0c76da1f719112cab513ab9f
• ocaml(Micromega_core_plugin__Sos_lib) = 7984dbed222b5707b22935261e97a1bf
• ocaml(Micromega_core_plugin__Sos_types) = d35f96b164748f21c9464fc982deec04
• ocaml(Micromega_plugin) = a2028cada0a4dc8d4a36ba485208ccd7
• ocaml(Micromega_plugin__Certificate) = 0ff6bce9e4c0b3e61be7ba859ff9935b
• ocaml(Micromega_plugin__Coq_micromega) = 039ec84e81a8f39b214c4732e3556610
• ocaml(Micromega_plugin__Linsolve) = c6bf4a1fed428bc78c04d0870bc55dfd
• ocaml(Micromega_plugin__Persistent_cache) = 8cdec97154e15e90f3ad9f9fd6819e56
• ocaml(Micromega_plugin__Polynomial) = 45d7375512df29400a8b8721e0f09e7e
• ocaml(Micromega_plugin__Simplex) = 27248d453e731e71110165b31132dbe1
• ocaml(Micromega_plugin__Vect) = ef45c5589b09036d2b04e4e340656cc8
• ocaml(Misc) = ea5241d01e1dabb94abc602b35e56ade
• ocaml(Miscprint) = 062bb3184a5513bfbb80d378beba1025
• ocaml(Mltop) = 96aba89183d0a87539f9788ee60adb61
• ocaml(Mod_declarations) = 92ab37a5802d9e27f92b3be032813f84
• ocaml(Mod_subst) = e8350b0343765b06377130a1625ea784
• ocaml(Mod_typing) = 8749ba866c799ce5bdae09a4abf69938
• ocaml(Modintern) = a9992eb7706ce476a512d5eae7e9ec4e
• ocaml(Modops) = 9194a2d710974103d09e9efe2ab269a6
• ocaml(Monad) = 2bde140cae2e992b633c464725202d31
• ocaml(Mutex_aux) = 84cdbad35da10d625c4ac3e57b8d5bf7
• ocaml(Namegen) = ce54ca0aef2c37e55b54fc2c21ce88ff
• ocaml(Nameops) = 739dddf56b3be826277bf8eed9d42dee
• ocaml(Names) = 6f6d675211dfa6226880a648f7e38180
• ocaml(Nametab) = ec18ed04312c50f1065693b6dbf15aaa
• ocaml(Nativecode) = 57942f08a2a3841387627c1ea47ded2e
• ocaml(Nativeconv) = ecee5123840845f2c608a7fa392d56c2
• ocaml(Nativelambda) = 43228bddc0ce9c86bf3d7d0cb504f187
• ocaml(Nativelib) = 30dd026a436c42d563279b442b1c86ec
• ocaml(Nativelibrary) = c2e283d886225ba731e561ce5ebf5eec
• ocaml(Nativenorm) = 60f3743bb0e1bff94dbb407a47ea2141
• ocaml(Nativevalues) = a759234dfa29da16a4fafc7575ff9bec
• ocaml(NeList) = 7fd80b98ad74757a38fb8feefb62c9a7
• ocaml(NewProfile) = 8624ed40210cb2479d322dd52eb526bc
• ocaml(Notation) = 54587b3bce9055f2b9a653f64f596162
• ocaml(Notation_gram) = f586f63e931c4f8d430fe6305a5f157c
• ocaml(Notation_ops) = 0aa41ef6b59e5f240096ec2d06aa5cd8
• ocaml(Notation_term) = 82aaefba44fcabd04e11675fa19549a7
• ocaml(Notationextern) = 599ab8e684d5924ddffd5d87ae074b9c
• ocaml(Notgram_ops) = 1b982eaa88a8bdf7881dcb195bd10559
• ocaml(Nsatz_core_plugin) = 76d693b67dd1f6dbcb3a3cbabed1fe1b
• ocaml(Nsatz_core_plugin__Ideal) = a765a74ecb2f99dd029774554da4232f
• ocaml(Nsatz_core_plugin__Nsatz) = 693ccaa47f26965aaeed1d4d9c4bfa0f
• ocaml(Nsatz_core_plugin__Polynom) = 5ab4d812d86ac931b0eb8972d82a6634
• ocaml(Nsatz_core_plugin__Utile) = 7eeebf3221ebec1b72b4d8fca48d6cb4
• ocaml(Nsatz_plugin) = 0197dfd0d488dc3a12f6db250b8ad92a
• ocaml(NumTok) = b0a48bb88f6d3e5f986113f2cd7218c2
• ocaml(Number_string_notation_plugin) = 5eb1faf58a1d0e41dfb791001450f53d
• ocaml(Number_string_notation_plugin__Number_string) = 26be4862e3a3de92a1e47c389ee5988d
• ocaml(ObjFile) = 25dd0e5647c5865eaa71e7db809a9e5f
• ocaml(Opaqueproof) = 9eac3139a620ac299e91106e75f428dd
• ocaml(Opaques) = 3799ed2c2cfdedde36fb7ba28ecd433f
• ocaml(Oprint) = a9904171b8bf1832d4d8d6c06ba280db
• ocaml(Option) = e6b230b1582aa5d429e5fc3ca4c80044
• ocaml(OrderedType) = 028516fb8b4953517cfa25d8cafb99fd
• ocaml(Outcometree) = 793c2f1dc6a3183ed387453b3e75c9df
• ocaml(Parray) = ada8d69c7b1080d775636133f4554360
• ocaml(Parsetree) = a8e773e1784913e8af2f5f83ed53a93b
• ocaml(Partac) = b5aa49e8447f56224772f0a28da09664
• ocaml(Partial_subst) = d0a694f2626cecd5d818f389ea1954a2
• ocaml(Path) = d652fc6085398c2f07e51fed32d448b8
• ocaml(Pattern) = 17f5dedf7d52a6b3a3d6754fa6df3244
• ocaml(Patternops) = 9b8ec1062e786df63808d20f610bc276
• ocaml(Perf) = f9658dac7d62890a1935a30afa3f96c9
• ocaml(PolyMap) = 66080bdfef65eeb15369226d1dc7a75f
• ocaml(Pp) = a3240b9aca1401ce479dc8d56de4079e
• ocaml(Pp_diff) = ad557b5b20afce42083bda5bb86c722a
• ocaml(Ppconstr) = 36f2bb8a77cdf3061c21d89329ac6191
• ocaml(Ppextend) = d68d63356febeb551ee4d9a25be98b8c
• ocaml(Ppred) = 031a1fc29fddbca9886b7918cd68ce05
• ocaml(Pputils) = 8d5c98f34794cd15a802ca9bb9ecbf1d
• ocaml(Ppvernac) = e89db62b06bb16b79a8e0b25b728a46b
• ocaml(Predicate) = 8dab2e64145accdd2f7a4ca1384b7899
• ocaml(Prettyp) = bf303ec3b4870a19c27b1926f54a7850
• ocaml(Pretype_errors) = 7c24062a8617f3c087af3cf6901bd424
• ocaml(Pretyping) = 95cc1064a6fd17755cc84ccb340200da
• ocaml(Primitive) = 691172872c2967e1d5ca29687c0c6b3f
• ocaml(Primred) = 12cbe4229000295c2b33fb9f98c005d0
• ocaml(Printer) = 5ba7e5451e34df6d970610bbba61cfc2
• ocaml(Printmod) = 0396f533deae30abcc5f0fffb6c524eb
• ocaml(Procq) = 4cfef49457233ab02fe3ee90fdd1a2a0
• ocaml(Profile) = c057f723b65cb54f6058b2938cfc50a4
• ocaml(Profile_tactic) = e827379cb67095a42b18afa0ec63c35c
• ocaml(Program) = 269af67f1457ac69ee585085d60f9d81
• ocaml(Proof) = bbfe8c43d4ead02a0e5a6710cc224761
• ocaml(Proof_bullet) = ec74a74b6ccb18651583e503bc9ac83c
• ocaml(Proof_diffs) = 260ad7e40f2dbf20f4f8fbad0a971a21
• ocaml(Proof_using) = 908c52339ceb3695eadccf4073f12986
• ocaml(Proofview) = dfbd66a884d59d052ab8a7f7ee8b7310
• ocaml(Proofview_monad) = 43661bbc1ec61eca5aa81e78fb20e7c9
• ocaml(Pstring) = 713359389f44624c284e5e4d20a80627
• ocaml(Pvernac) = f81f59ebddeeed12a1cb0f790558d46d
• ocaml(Q) = 8b54816595b0494f1630c558d7f2fdec
• ocaml(Quickfix) = a8f347b27dc5e58c308b6569477dbfb0
• ocaml(Range) = 8ac81b8659e15fffbbfa2497f5d41683
• ocaml(RecLemmas) = bc1a338445afe6afd711c25170d51eb7
• ocaml(Record) = e5b7b9f2a6d831b3a370e75b769202fb
• ocaml(RedFlags) = 464621ff3f873f830cca7624bb5e7348
• ocaml(Redexpr) = 35fc42292d0dd7f02a93bd04ca06650b
• ocaml(Redops) = e437f2d630bc6a5939d44a744ab4ba23
• ocaml(Reduction) = dda8c0a1442dde9fb25512ec2119a0b8
• ocaml(Reductionops) = 52ee09855547f2199210d10f05fcab7e
• ocaml(Refine) = 509779c6e75e7e783def8f1d0d6a84e7
• ocaml(Relevanceops) = 85a09e51fa96dc6b901d9b5753fea604
• ocaml(Reserve) = 0ebcbdd5d368730804451ec566a53ecb
• ocaml(RetrieveObl) = 7f001735c1600e7232a20494dcc76a75
• ocaml(Retroknowledge) = d244dbe59621256d3052fb89838c4a68
• ocaml(Retyping) = 46225e269157307199fa084e3158c33d
• ocaml(Rewrite) = 85e030505211df3b10dd5bcc6400aecb
• ocaml(Ring_plugin) = cc06a0dbb7faaa0affdb43d6e81922f0
• ocaml(Ring_plugin__Ring) = b1ee853c6eefdde0118a3e0a7ac4480b
• ocaml(Ring_plugin__Ring_ast) = b060186b08010016db2f69729dfaeac7
• ocaml(Rocqlib) = 73f23452a4338ee227059cc009d49aab
• ocaml(Rtauto_plugin) = bef1b1a95c817e3bc0983d58fab82ec3
• ocaml(Rtauto_plugin__Proof_search) = 2395ba64feb37e1b1843d6a0063fe396
• ocaml(Rtauto_plugin__Refl_tauto) = f00052ac4915f818c5df93729da855b1
• ocaml(Rtree) = 76c9c7866446e0e30fb1f7e89ba8fe56
• ocaml(SList) = 8f839b11093748431b165456534a4cde
• ocaml(Safe_typing) = dc062f013adc9a2492a47514c9775f09
• ocaml(Search) = ef1270c48e3b263601c2c358a3a25842
• ocaml(Section) = 1d4c495bdd794cda45006d17db0ffe67
• ocaml(Segmenttree) = 3542ef972686acbb94ada459284e6bb0
• ocaml(Shape) = 639524fde7fd305260a62f1e1cefbd0a
• ocaml(Smartlocate) = 65b69bfea564a56c1e81c9c20a502133
• ocaml(Sorts) = d83a2186bf232469c3ad5bdbbe5e1cad
• ocaml(Spawn) = e58a5144e73bf5ba67b7439648199d64
• ocaml(Spawned) = 890a65f8a9a58a413fdf47cf3bea91cb
• ocaml(Ssreflect_plugin) = df2edbd9591521138483880f58a1bde5
• ocaml(Ssreflect_plugin__Ssrast) = 41e8e2dd8d085639dd8ca307f83ce003
• ocaml(Ssreflect_plugin__Ssrbwd) = c807f9af56c055d26e8efbfd049eea35
• ocaml(Ssreflect_plugin__Ssrcommon) = 7b6f19f9c0926207f9277ee88bfa658e
• ocaml(Ssreflect_plugin__Ssrelim) = 5eb5827cb46b2fec0a3bc785d2c48c89
• ocaml(Ssreflect_plugin__Ssrequality) = 0535875005bb3531543d3a037d304fbf
• ocaml(Ssreflect_plugin__Ssrfwd) = 9c530c229fe09243fa1530f64b18b07c
• ocaml(Ssreflect_plugin__Ssripats) = a3e7a8013904e351d674a0fc9400698d
• ocaml(Ssreflect_plugin__Ssrparser) = 999acf790bc4a39637f03f00c827e981
• ocaml(Ssreflect_plugin__Ssrprinters) = d71e94606fa5466877eebdae50f403e4
• ocaml(Ssreflect_plugin__Ssrtacticals) = 9eb9ec5ac58d8786d04b82049b16ad8f
• ocaml(Ssreflect_plugin__Ssrview) = 473893e371fb956821721f1ab4277e14
• ocaml(Ssrmatching_plugin) = 47740f9f41d7bde9b34c128f3187aea8
• ocaml(Ssrmatching_plugin__G_ssrmatching) = 3e06d0dbcca616b25b55cd817698b4d0
• ocaml(Ssrmatching_plugin__Ssrmatching) = f81b77d3d8f1cddb57d4d6af44aa870a
• ocaml(Stateid) = 7a2fd3563391a6fa0d41e519f878e667
• ocaml(Stdarg) = 9043edaa3b9e0dda19d3baf58be81b69
• ocaml(Stdlib) = 7ff659a4a6b8ca32adc85623b24921e4
• ocaml(Stdlib__Arg) = c45f9dbce830bdf7c07d08fc27cae4b2
• ocaml(Stdlib__Array) = c1e9990cfc96f4a80be219086df84a1a
• ocaml(Stdlib__Bigarray) = 53e1fb135dc2b52a9be495706f0fe941
• ocaml(Stdlib__Bool) = 7d26c397d64c30c6bfc9fcc31bfd9e64
• ocaml(Stdlib__Buffer) = 199531813c148c733aa4841901f61885
• ocaml(Stdlib__Bytes) = 673437615face5d16342decc909aee70
• ocaml(Stdlib__Callback) = f81228af62f8d1689727fb188b982c9c
• ocaml(Stdlib__Char) = aab5b2646a35544343b9729f2a340b60
• ocaml(Stdlib__Complex) = 10107702cfc5d64ad493797d02699351
• ocaml(Stdlib__Condition) = 1c01c895aec3b63b8ab8cbe2aa66d19e
• ocaml(Stdlib__Digest) = 34f0d73da12b160ad2ec9f14ef6ccb12
• ocaml(Stdlib__Domain) = f4f911af3a887deb4246da1952f3bbde
• ocaml(Stdlib__Either) = d0d544d8ad6cd8d3916ef604e87e8b79
• ocaml(Stdlib__Ephemeron) = 0e97e578bba2a1892394a875582409b1
• ocaml(Stdlib__Filename) = dca44599068c4f1117dfeb6a2637f3f9
• ocaml(Stdlib__Float) = 982b5c7843be6c7a654d37077ab2df6f
• ocaml(Stdlib__Format) = 59fa71efaaaea19dea6b27602dcaaaa2
• ocaml(Stdlib__Fun) = 69dd52f26a432581d74d2acf8cbfdd4f
• ocaml(Stdlib__Gc) = 7001b1bdc5fa669e74321ebe814f5c3c
• ocaml(Stdlib__Hashtbl) = 962e9d183e8a207a666ca7506cf46032
• ocaml(Stdlib__Int32) = eb4f33ed29b560525b336e79955fa30a
• ocaml(Stdlib__Int64) = 29e84e0d87545e4220cc5617eb2d20d5
• ocaml(Stdlib__Lazy) = d0b8d3be22a8b5bdfc9dda1877ae006f
• ocaml(Stdlib__Lexing) = 070822eb5537492e7ac0d885f1627b82
• ocaml(Stdlib__List) = 1f65c7c74ac3633417a8002cc6dd0e53
• ocaml(Stdlib__Map) = 2d8ea4e0be35a4403643e7043fc81316
• ocaml(Stdlib__Marshal) = b6dd359978d92b445715f8b6e7291756
• ocaml(Stdlib__Mutex) = be9647a85be946b28ceaaad8440df78c
• ocaml(Stdlib__Nativeint) = 3274bc361f120620f5df0ee8b898262b
• ocaml(Stdlib__Obj) = 70f3df7415d40eb721c8413fa408b7b6
• ocaml(Stdlib__Printexc) = e58645338ce0e91a971f2806d56d691b
• ocaml(Stdlib__Printf) = 689694603948509ee3d0b39b9ac66005
• ocaml(Stdlib__Queue) = 3b321c1bad5b935cfbf4767b238e4180
• ocaml(Stdlib__Random) = 56f5b48db4d9ef67c6b0228d4fe599b4
• ocaml(Stdlib__Result) = 57c890b1fb51649494b6cefd7d3ddc9b
• ocaml(Stdlib__Scanf) = 2e9739978caab34087dc83418ace9de6
• ocaml(Stdlib__Seq) = 1d1c31e02b77070ff0e51eaaab2af0cc
• ocaml(Stdlib__Set) = f1c0353417503cf69279f65dd7b31d22
• ocaml(Stdlib__Stack) = 8beb90704d5de14f0323d6421c8095d6
• ocaml(Stdlib__String) = 64f1c33cae78f3dd80ca58dbba3deaf9
• ocaml(Stdlib__Sys) = 06196acdacded24c46c02b8acd00223a
• ocaml(Stdlib__Uchar) = f6a44dd0c2e2c80b44deed7eb3c121ef
• ocaml(Stdlib__Weak) = d315fd61fbd009f4439cd0d03c62af48
• ocaml(Stm) = b559e67f416916a13e78612fd59dc9b7
• ocaml(Stmargs) = 1b963824eb7d6638699545d167312798
• ocaml(Store) = b9136c58a2dd4791fc1d21a39fb36017
• ocaml(Str) = 82bb8230a6bbf7cb2d8be245938b615a
• ocaml(Structures) = 619787330bebec865bbcd18230d9f884
• ocaml(Subst) = b930cee1e6bdd0d12aaa3723dec0cbf8
• ocaml(Subtyping) = bbefae9437fff437e5cd4e0ccabdeeee
• ocaml(Summary) = bd0c2d9ffcb014e2b8fbbf5b090c75ce
• ocaml(Synterp) = 3d29d78895c2201e140bba1c439ac68f
• ocaml(System) = 083edf2fdc428062aa8e2efba7461e0f
• ocaml(TQueue) = 06f2f0c295a422dab7042027e9408739
• ocaml(Tacmach) = 8ba599478df4392c8f9447543521ab26
• ocaml(Tacred) = 088e3de9cff32e754fff390f75c167e9
• ocaml(Tactic_option) = 1e9f499ebf44288b90803651c701e52d
• ocaml(Tacticals) = 474064050f3fcb808da57eed62086f40
• ocaml(Tactics) = 5e0b4f5912b90e4bfa0b7869235ab51b
• ocaml(Tactypes) = 0ec10db77c88d30db9e99011e93c210c
• ocaml(Tauto_plugin) = 9ccf8b9a8e9b5f349fb354a6268da0e1
• ocaml(TemplateArity) = 9e48adb1eea260e9886a715cba91421b
• ocaml(Term) = 4b094fc1c1d368f9edf37c987ae768e5
• ocaml(Terminal) = e6ddc9c8ac2d341ec485865bea78afaa
• ocaml(Termops) = 085444b10f769ca8424ab1a5d22d7708
• ocaml(Thread) = 99d33b3840c6d249522009e7ea8cf472
• ocaml(Tok) = fb64a029c4f14c556c54f93a3a0319a2
• ocaml(Top_printers) = 5e431dacb6a11d38987fa89a48d9fd44
• ocaml(Topfmt) = 2383104adedec2bb688b790988a59e65
• ocaml(Toploop) = c80e2fca60fda9d8dfe6e9bfde4f1118
• ocaml(TransparentState) = de77add7184ba43492228ac29aae0802
• ocaml(Trie) = 49f3b048c4ef037dc20113ac2ad9654a
• ocaml(Tuto0_plugin) = 55bac9a5a042df8029066af4a5ecc9ab
• ocaml(Tuto0_plugin__Tuto0_main) = 501355a8e6223a4f8b30bcc5108f2dc0
• ocaml(Tuto1_plugin) = 00435ebd7722771ac79d9c776a1817c3
• ocaml(Tuto1_plugin__Inspector) = cec56edb003bd7f80868692373c20d80
• ocaml(Tuto1_plugin__Simple_check) = 52273e00f7f8badf1f55a52110ec6a04
• ocaml(Tuto1_plugin__Simple_declare) = 32050c7ec0a5baaa943d975c14d7c042
• ocaml(Tuto1_plugin__Simple_print) = f35006ed73ae34a60e6cb357edcab1c4
• ocaml(Tuto2_plugin) = 184262ed8436fe96abc9a352ae926716
• ocaml(Tuto2_plugin__Counter) = adaec3cc229db9f72843af6871311eeb
• ocaml(Tuto2_plugin__Custom) = 35e76c5ea338b2ed2dd6799a746bbf6c
• ocaml(Tuto2_plugin__Persistent_counter) = 4d4990a44c8c04bbd27cc573d45d6caf
• ocaml(Tuto3_plugin) = 8d95e40d324b36be29469244aa44d456
• ocaml(Tuto3_plugin__Construction_game) = eeed0588d3886031db967f1f4642c068
• ocaml(Tuto3_plugin__Tuto_tactic) = aab070abfea82dad600c28e0cbeedf53
• ocaml(Tuto4_plugin) = 6a376dcf2741cdebdb070a1441263c46
• ocaml(Type_errors) = 663269bc602719b3d712a2469a7023f2
• ocaml(Type_immediacy) = e9c7b29e4682b2c8d33db46d874c4407
• ocaml(Typeclasses) = f019cb18e5ccb14439fcf06d78862358
• ocaml(Typeclasses_errors) = 454aa91aa502796f475e272539a019d6
• ocaml(Typeops) = a2cc2f8f20c1c6ee31f06d8409eaf7e3
• ocaml(Types) = 9cd5e0c0403b733edee4d9c7b8a72d97
• ocaml(Typing) = 52e40b155080aa68dbf65c9261e3c2b6
• ocaml(UGraph) = 3b772c0bef4ea1c9e9fa4f54c35e3928
• ocaml(UState) = 9632204cce05d2b03051e8bef06a8700
• ocaml(UVars) = 613fbece796bede9a02847a1377a3613
• ocaml(Uint63) = 7dea127224220e1e5822638ceac8a7d9
• ocaml(Unicode) = 1dcf32c58474279195a1088f1570993e
• ocaml(Unicodetable) = 7978a3214251c9eae8c81d10e7e883a3
• ocaml(Unification) = 1288d34bb5571997cdf4748141f0636d
• ocaml(Unionfind) = da600e6dc756b192efcd4d76cbc94ec4
• ocaml(Unit_info) = 3c074c0f4cbfe70413b3f89c1a0fbf56
• ocaml(Univ) = 3230b34bf11fa26a0034d1ae083ff446
• ocaml(UnivFlex) = c0884ea4e18fecf999514e41ae1db303
• ocaml(UnivGen) = 8ee037a363052f3135c135ecfa974b38
• ocaml(UnivMinim) = 958f03758c750624d7dae7544d04a176
• ocaml(UnivNames) = ff856e13a956e8b237b56e9f2fdb623a
• ocaml(UnivProblem) = b09318f5c743f36394ef0d15472eb2f0
• ocaml(UnivSubst) = f5f7b2ee6107e7ee1e6bf2c9067ff557
• ocaml(Unix) = c1dc7711fef7c883b67ab33c46fd7030
• ocaml(UserWarn) = dcba2d44e488412dfb4707f7d5257625
• ocaml(Util) = 6d6405eea6173eefd26ae1bf0cad4c54
• ocaml(Values) = 696451dda458a5396ea1e78d5be48ab2
• ocaml(Vars) = a3656158cf57a67dae5a8ec4d34d01a7
• ocaml(Vconv) = 56406c5f26b59f7bee3bafce458c6d0d
• ocaml(Vcs) = c21c4b1f7e473fefa3470cfd323e4ec5
• ocaml(Vernac) = 2dcbef2fea9d42503c31d4f0ba296375
• ocaml(VernacControl) = 9b6eca717284fbf9976bbbd2e876287f
• ocaml(Vernac_classifier) = 2d652bdbd78b2519e1245f4f93ddf0b3
• ocaml(Vernacentries) = ed09e84daeee415ed462353edc39b1ba
• ocaml(Vernacexpr) = 93fc5b1ea155512f1988493cf9c99014
• ocaml(Vernacextend) = 15e8a4b3cdc70c5b8f93b59b2f9ede9d
• ocaml(Vernacinterp) = 555bded854ab800afc2ff15450fb1334
• ocaml(Vernacoptions) = 4fc732664da533011aabb56280017f5e
• ocaml(Vernacprop) = 2d13fae95e86b5cd9aa8972510610ee7
• ocaml(Vernacstate) = 22bde5d6b762d88c88b2746db92e4858
• ocaml(Vernactypes) = 4f5e2c2c66498d0ad4e8ff9c43e06e7e
• ocaml(Vm) = e1125464aa3af1d986db25fca47b1d9c
• ocaml(Vmbytecodes) = 288e4e062c05fb610d4ae06421348db4
• ocaml(Vmbytegen) = 8c3b8ae842de3b91552f996a962e960e
• ocaml(Vmemitcodes) = fc8c05cc70b370817fcf3f47c444b9b5
• ocaml(Vmerrors) = c44396199eab6e9d3168232d768363d9
• ocaml(Vmlambda) = 5813c2b7b1e8b7454dfd407235a2d8f6
• ocaml(Vmlibrary) = 14d41b715a4d5dc081385c7139c26390
• ocaml(Vmopcodes) = 08d9af700e76e6c5b9dc8272952a751d
• ocaml(Vmsymtable) = b0fa9264636cc7f9bcd6745d15646eaf
• ocaml(Vmvalues) = 91aa6129d467a6b99ac09255e29d9438
• ocaml(Vnorm) = 8d65e1648d3650eadd3453dbee59f18b
• ocaml(Warnings) = fb0409a10304c2fa86fc9e127c31ff52
• ocaml(WorkerPool) = e4a4344e47882d81661ed9eb7ec855f3
• ocaml(Xml_datatype) = 467b68b73cffd645333815d6b355f3c7
• ocaml(Z) = b8f36df41ec3ad4dd65a34f697424998
• ocaml(Zify_plugin) = 3726fda4ee09d032689f52a677c41d45
• ocaml(Zify_plugin__Zify) = 7af0ef005ffcfc804454c7cd8f9205c0
• rocq(ppc-64) = 9.1.1-1.fc44
• rpmlib(CompressedFileNames) <= 3.0.4-1
• rpmlib(FileDigests) <= 4.6.0-1
• rpmlib(PayloadFilesHavePrefix) <= 4.0-1
• rpmlib(PayloadIsZstd) <= 5.4.18-1
• rtld(GNU_HASH)

License

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

Changelog

* 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/01
/usr/lib/.build-id/01/207260bdafbe20c91b8288cc4eee75b625553e
/usr/lib/.build-id/08
/usr/lib/.build-id/08/a2708bdec59bc5781b74daf4bb2b3f8eda4fda
/usr/lib/.build-id/10
/usr/lib/.build-id/10/13a74e06c1c50ffd4948ded3f7734725c29830
/usr/lib/.build-id/14
/usr/lib/.build-id/14/6e8c599fde52657c667ef6a1e419950cb1e9ce
/usr/lib/.build-id/1a
/usr/lib/.build-id/1a/7b6f8d380b6f04cd624699e5917d77a07a4ca3
/usr/lib/.build-id/1c
/usr/lib/.build-id/1c/a1e7e1485c4f869c0ebcebd6d55c948a02ad6e
/usr/lib/.build-id/24
/usr/lib/.build-id/24/672fa88c5c70a46fd636767e524fd0042e71a7
/usr/lib/.build-id/27
/usr/lib/.build-id/27/915a0e30a7289f88b2f66707adb138c838a832
/usr/lib/.build-id/29
/usr/lib/.build-id/29/27a52be3108667121713f049cb36d4af46176c
/usr/lib/.build-id/2a
/usr/lib/.build-id/2a/8913034a058905c64ec9b3552ca7eb46051baa
/usr/lib/.build-id/2e
/usr/lib/.build-id/2e/25a2b7bd479f54c46db692a3f56c7545bc324d
/usr/lib/.build-id/3c
/usr/lib/.build-id/3c/11b799e0c85c3588f4576a07bada9d2b1ff723
/usr/lib/.build-id/49
/usr/lib/.build-id/49/5f63c64006af84735d2fdc7112c035da26aee8
/usr/lib/.build-id/4c
/usr/lib/.build-id/4c/e316c04a52bbf2f9a13c24405c5020f0a94364
/usr/lib/.build-id/52
/usr/lib/.build-id/52/556aad7966b07ae0646074abd4e18ab4a5d1f7
/usr/lib/.build-id/5b
/usr/lib/.build-id/5b/fe0b8de0eeb2851d52d706174b4edf79503fdd
/usr/lib/.build-id/5e
/usr/lib/.build-id/5e/66ba472f421ee1e7235b5ccbd14b168a9d1b7d
/usr/lib/.build-id/61
/usr/lib/.build-id/61/b0bf762518ce48f87e4f4de7ab2794f4b4ccb7
/usr/lib/.build-id/62
/usr/lib/.build-id/62/fb8a0affee3a464804ba721eb3237b6520fbd8
/usr/lib/.build-id/63
/usr/lib/.build-id/63/d7a6e56aa5b43a07986964694a25a0f4f2e64d
/usr/lib/.build-id/64
/usr/lib/.build-id/64/e561831b1e029111c954f9d81587c80092b327
/usr/lib/.build-id/69
/usr/lib/.build-id/69/c3d6b96e30753413af82be832597abed151314
/usr/lib/.build-id/74
/usr/lib/.build-id/74/5b3ebdbd53fc446f62ae5f73cfbb26a1a3f023
/usr/lib/.build-id/7d
/usr/lib/.build-id/7d/3b169c95d871f11a700c9caa68c9a56eeef1d7
/usr/lib/.build-id/84
/usr/lib/.build-id/84/6807669f4f1914cc071caae045caac1474f0e2
/usr/lib/.build-id/85
/usr/lib/.build-id/85/05370b4f33c3babb00581434c0d000a8c97e47
/usr/lib/.build-id/86
/usr/lib/.build-id/86/0a63d34783128af46ba0163bdce6b6b2544320
/usr/lib/.build-id/87
/usr/lib/.build-id/87/883b5476acaf67e42e3030eee1d3acaa80649a
/usr/lib/.build-id/94
/usr/lib/.build-id/94/c8a12cceb44b32ae07cf20ff8c90a760157686
/usr/lib/.build-id/9a
/usr/lib/.build-id/9a/af31c7712c12deb4388de22233315f22c9ef01
/usr/lib/.build-id/9d
/usr/lib/.build-id/9d/789d149a7ff826c97845c2dd98d01e65f6fadb
/usr/lib/.build-id/9f
/usr/lib/.build-id/9f/e461f0f746313e39c3f57966ee5099fd78b771
/usr/lib/.build-id/a0
/usr/lib/.build-id/a0/5a0628c73aaa575fb3f3fced960182894ed084
/usr/lib/.build-id/a6
/usr/lib/.build-id/a6/1febd427a771e360fbf581edea4e5e357e73f8
/usr/lib/.build-id/aa
/usr/lib/.build-id/aa/cdf0b7ce1a821363e7ee3eae4aead927174c74
/usr/lib/.build-id/af
/usr/lib/.build-id/af/9263289b2f13e5e8ee17d25ec21f5176df098b
/usr/lib/.build-id/af/971f73ea8d76c9cb0a1aa37efb27499ed7ebc6
/usr/lib/.build-id/b0
/usr/lib/.build-id/b0/9c8d09ed44d82e0e9ec6d12470d4f7baf74ce9
/usr/lib/.build-id/b1
/usr/lib/.build-id/b1/f05255539254c13dadedf93ca419fc0b6c2eeb
/usr/lib/.build-id/b2
/usr/lib/.build-id/b2/54afeaaddcc380f434cac184c567f575ecec11
/usr/lib/.build-id/b4
/usr/lib/.build-id/b4/1bae501382e19c4822d191171a5bc876ca7d49
/usr/lib/.build-id/b8
/usr/lib/.build-id/b8/044cb3dbc8537223d66319abdb7b66e10f5cbf
/usr/lib/.build-id/ba
/usr/lib/.build-id/ba/67efd2735170d4e2f21ea9b92b31bf7aeef23d
/usr/lib/.build-id/ba/77a25b5c4bdf6cbaaaeb03a93e00b7fe1003bc
/usr/lib/.build-id/c3
/usr/lib/.build-id/c3/a01d3daf4e66c0e14a6f02b2e7043c010c6655
/usr/lib/.build-id/c8
/usr/lib/.build-id/c8/300dad2c11f64d699e04e617c62e72ef004852
/usr/lib/.build-id/cd
/usr/lib/.build-id/cd/ff2aa241d25b158a0002ef42b6dc0226b3bfec
/usr/lib/.build-id/cf
/usr/lib/.build-id/cf/db795713d8a8aaa9e46b6c05a3fb9c0bd675df
/usr/lib/.build-id/d2
/usr/lib/.build-id/d2/4fdcabb93ca37eff41607ee5d4415a798d88ee
/usr/lib/.build-id/d2/cf763776d9a1941c86a6ee6d080c0478bd1945
/usr/lib/.build-id/d3
/usr/lib/.build-id/d3/11a94b9d80313e3297c657316605eb974f623f
/usr/lib/.build-id/d3/2c0abdd24104da232fa41813a168d934fd1acd
/usr/lib/.build-id/d3/545e8d64fb6ec39d34cca46b438cb9bae25680
/usr/lib/.build-id/d3/7c432b8f90b76430e649fb58e2a5506a1e4f55
/usr/lib/.build-id/d9
/usr/lib/.build-id/d9/dff449fa2cdc8304785da8bdf2bb76aaa591d4
/usr/lib/.build-id/dd
/usr/lib/.build-id/dd/98e41e223113d9169a819c2ba9e3260d0d0a4b
/usr/lib/.build-id/e2
/usr/lib/.build-id/e2/0c467845106581d118d1798b0495371ee75a36
/usr/lib/.build-id/e7
/usr/lib/.build-id/e7/66b034db1507011639a58fd365e3bb119f0574
/usr/lib/.build-id/e8
/usr/lib/.build-id/e8/1a75b131c2f408442256d11277c3dab6c26f20
/usr/lib/.build-id/e9
/usr/lib/.build-id/e9/a770d38949ead7e2d0289570a59b8fb2394c3e
/usr/lib/.build-id/eb
/usr/lib/.build-id/eb/a0773fcbda0910a0ba3ff81711a4ef131b99cc
/usr/lib/.build-id/f7
/usr/lib/.build-id/f7/581f00c8c20d023d064484196443e784613940
/usr/lib/.build-id/fd
/usr/lib/.build-id/fd/c93c1f79b187addb5a144aeff41a18f1a30635
/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/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/coqdeplib/coqdeplib__Static_toplevel_libs.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/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/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/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/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/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__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/indrec.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/inductiveops.cmi
/usr/lib64/ocaml/rocq-runtime/pretyping/keys.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/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/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/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/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/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/tacticals.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/tactics.cma
/usr/lib64/ocaml/rocq-runtime/tactics/tactics.cmi
/usr/lib64/ocaml/rocq-runtime/tactics/tactics.cmxs
/usr/lib64/ocaml/rocq-runtime/tools
/usr/lib64/ocaml/rocq-runtime/tools/CoqMakefile.in
/usr/lib64/ocaml/rocq-runtime/tools/TimeFileMaker.py
/usr/lib64/ocaml/rocq-runtime/tools/coqdoc
/usr/lib64/ocaml/rocq-runtime/tools/coqdoc/coqdoc.css
/usr/lib64/ocaml/rocq-runtime/tools/coqdoc/coqdoc.sty
/usr/lib64/ocaml/rocq-runtime/tools/make-both-single-timing-files.py
/usr/lib64/ocaml/rocq-runtime/tools/make-both-time-files.py
/usr/lib64/ocaml/rocq-runtime/tools/make-one-time-file.py
/usr/lib64/ocaml/rocq-runtime/toplevel
/usr/lib64/ocaml/rocq-runtime/toplevel/ccompile.cmi
/usr/lib64/ocaml/rocq-runtime/toplevel/colors.cmi
/usr/lib64/ocaml/rocq-runtime/toplevel/common_compile.cmi
/usr/lib64/ocaml/rocq-runtime/toplevel/coqc.cmi
/usr/lib64/ocaml/rocq-runtime/toplevel/coqcargs.cmi
/usr/lib64/ocaml/rocq-runtime/toplevel/coqloop.cmi
/usr/lib64/ocaml/rocq-runtime/toplevel/coqrc.cmi
/usr/lib64/ocaml/rocq-runtime/toplevel/coqtop.cmi
/usr/lib64/ocaml/rocq-runtime/toplevel/g_toplevel.cmi
/usr/lib64/ocaml/rocq-runtime/toplevel/load.cmi
/usr/lib64/ocaml/rocq-runtime/toplevel/memtrace_init.cmi
/usr/lib64/ocaml/rocq-runtime/toplevel/toplevel.cma
/usr/lib64/ocaml/rocq-runtime/toplevel/toplevel.cmxs
/usr/lib64/ocaml/rocq-runtime/toplevel/vernac.cmi
/usr/lib64/ocaml/rocq-runtime/toplevel/workerLoop.cmi
/usr/lib64/ocaml/rocq-runtime/vernac
/usr/lib64/ocaml/rocq-runtime/vernac/assumptions.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/attributes.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/auto_ind_decl.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/canonical.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/classes.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/comArguments.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/comAssumption.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/comCoercion.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/comDefinition.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/comExtraDeps.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/comFixpoint.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/comHints.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/comInductive.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/comPrimitive.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/comRewriteRule.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/comSearch.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/comTactic.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/debugHook.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/declare.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/declareInd.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/declareUniv.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/declaremods.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/egramml.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/egramrocq.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/future.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/g_obligations.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/g_proofs.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/g_redexpr.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/g_vernac.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/himsg.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/indschemes.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/library.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/loadpath.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/metasyntax.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/mltop.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/opaques.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/ppvernac.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/prettyp.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/printmod.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/proof_using.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/pvernac.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/recLemmas.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/record.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/retrieveObl.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/search.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/synterp.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/tactic_option.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/topfmt.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/vernac.cma
/usr/lib64/ocaml/rocq-runtime/vernac/vernac.cmxs
/usr/lib64/ocaml/rocq-runtime/vernac/vernacControl.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/vernac_classifier.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/vernacentries.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/vernacexpr.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/vernacextend.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/vernacinterp.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/vernacoptions.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/vernacprop.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/vernacstate.cmi
/usr/lib64/ocaml/rocq-runtime/vernac/vernactypes.cmi
/usr/lib64/ocaml/rocq-runtime/vm
/usr/lib64/ocaml/rocq-runtime/vm/coqrun.cma
/usr/lib64/ocaml/rocq-runtime/vm/coqrun.cmi
/usr/lib64/ocaml/rocq-runtime/vm/coqrun.cmxs
/usr/lib64/ocaml/stublibs/dllcoqperf_stubs.so
/usr/lib64/ocaml/stublibs/dllcoqrun_stubs.so
/usr/share/doc/rocq-runtime
/usr/share/doc/rocq-runtime/README.md
/usr/share/licenses/rocq-runtime
/usr/share/licenses/rocq-runtime/LICENSE
/usr/share/man/man1/rocq.1.gz
/usr/share/man/man1/rocqchk.1.gz
/usr/share/texlive/texmf-dist/tex/latex/misc
/usr/share/texlive/texmf-dist/tex/latex/misc/coqdoc.sty

Generated by rpm2html 1.8.1

Fabrice Bellet, Sun Apr 26 02:37:53 2026