coq-core-8.14.1-2.fc36 in Fedora Rawhide

↵ Return to the main page of coq-core
View build
Search for updates

Package Info (Data from x86_64 build)
🠗 Changelog
🠗 Dependencies
🠗 Provides
🠗 Files

Changelog

Date	Author	Change
2021-12-27	Jerry James <loganjerry at gmail dot com> - 8.14.1-2	- Rebuild for ocaml-lablgtk3 3.1.2
2021-11-30	Jerry James <loganjerry at gmail dot com> - 8.14.1-1	- Version 8.14.1
2021-10-21	Jerry James <loganjerry at gmail dot com> - 8.14.0-1	- Version 8.14.0 - Add -core subpackage
2021-10-05	Richard W.M. Jones <rjones at redhat dot com> - 8.13.2-5	- OCaml 4.13.1 build
2021-10-04	Richard W.M. Jones <rjones at redhat dot com> - 8.13.2-4	- Try to build on s390x with OCaml 4.13
2021-07-29	Jerry James <loganjerry at gmail dot com> - 8.13.2-3	- Rebuild for changed ocamlx(Dynlink)
2021-07-21	Fedora Release Engineering <releng at fedoraproject dot org> - 8.13.2-2	- Rebuilt for https://fedoraproject.org/wiki/Fedora_35_Mass_Rebuild
2021-06-04	Jerry James <loganjerry at gmail dot com> - 8.13.2-1	- Version 8.13.2
2021-03-03	Jerry James <loganjerry at gmail dot com> - 8.13.1-1	- Version 8.13.1
2021-03-02	Richard W.M. Jones <rjones at redhat dot com> - 8.13.0-2	- OCaml 4.12.0 build

Dependencies

coq = 8.14.1-2.fc36
glibc >= 2.34.9000-34.fc36
gmp
ocaml = c4b583a727ec28f5bc9ba36adc64cfc7
ocaml-runtime = c4b583a727ec28f5bc9ba36adc64cfc7
ocaml-zarith = 28893fe4e203824f596139a85cea8961
ocaml-zarith-devel = 28893fe4e203824f596139a85cea8961

Provides

coq-core
coq-core(x86-64)
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(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(CPath)
ocaml(CPrimitives)
ocaml(CProfile)
ocaml(CSet)
ocaml(CSig)
ocaml(CString)
ocaml(CThread)
ocaml(CUnix)
ocaml(CWarnings)
ocaml(Canonical)
ocaml(Cases)
ocaml(Cbn)
ocaml(Cbv)
ocaml(Cc_plugin)
ocaml(Cc_plugin__Ccalgo)
ocaml(Cc_plugin__Ccproof)
ocaml(Cc_plugin__Cctac)
ocaml(Cc_plugin__G_congruence)
ocaml(Ccompile)
ocaml(Class_tactics)
ocaml(Classes)
ocaml(Clenv)
ocaml(Coercion)
ocaml(Coercionops)
ocaml(ComArguments)
ocaml(ComAssumption)
ocaml(ComCoercion)
ocaml(ComDefinition)
ocaml(ComFixpoint)
ocaml(ComHints)
ocaml(ComInductive)
ocaml(ComPrimitive)
ocaml(ComProgramFixpoint)
ocaml(ComSearch)
ocaml(ComTactic)
ocaml(Constr)
ocaml(Constr_matching)
ocaml(Constrexpr)
ocaml(Constrexpr_ops)
ocaml(Constrextern)
ocaml(Constrintern)
ocaml(Context)
ocaml(Contradiction)
ocaml(Control)
ocaml(Conv_oracle)
ocaml(Cooking)
ocaml(CoqProject_file)
ocaml(Coq_config)
ocaml(Coqargs)
ocaml(Coqc)
ocaml(Coqcargs)
ocaml(Coqinit)
ocaml(Coqlib)
ocaml(Coqloadpath)
ocaml(Coqloop)
ocaml(Coqrc)
ocaml(Coqrun)
ocaml(Coqtop)
ocaml(CoqworkmgrApi)
ocaml(DAst)
ocaml(Dag)
ocaml(DebugHook)
ocaml(Declarations)
ocaml(Declare)
ocaml(DeclareInd)
ocaml(DeclareScheme)
ocaml(DeclareUctx)
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(Dn)
ocaml(Dnet)
ocaml(Dumpglob)
ocaml(Dyn)
ocaml(EConstr)
ocaml(Eauto)
ocaml(Egramcoq)
ocaml(Egramml)
ocaml(Elim)
ocaml(Elimschemes)
ocaml(Entries)
ocaml(Envars)
ocaml(Environ)
ocaml(Eqdecide)
ocaml(Eqschemes)
ocaml(Equality)
ocaml(Esubst)
ocaml(Evar)
ocaml(Evar_kinds)
ocaml(Evar_refiner)
ocaml(Evarconv)
ocaml(Evardefine)
ocaml(Evarsolve)
ocaml(Evarutil)
ocaml(Evd)
ocaml(Exninfo)
ocaml(Explore)
ocaml(Extend)
ocaml(Extraction_plugin)
ocaml(Extraction_plugin__Big)
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_plugin)
ocaml(Firstorder_plugin__Formula)
ocaml(Firstorder_plugin__G_ground)
ocaml(Firstorder_plugin__Ground)
ocaml(Firstorder_plugin__Instances)
ocaml(Firstorder_plugin__Rules)
ocaml(Firstorder_plugin__Sequent)
ocaml(Firstorder_plugin__Unify)
ocaml(Flags)
ocaml(Float64)
ocaml(Float64_common)
ocaml(Float_syntax_plugin)
ocaml(Float_syntax_plugin__Float_syntax)
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_prim)
ocaml(G_proofs)
ocaml(G_toplevel)
ocaml(G_vernac)
ocaml(Genarg)
ocaml(Genintern)
ocaml(Geninterp)
ocaml(Genprint)
ocaml(Genredexpr)
ocaml(GlobEnv)
ocaml(Glob_ops)
ocaml(Glob_term)
ocaml(Global)
ocaml(Globnames)
ocaml(Goal)
ocaml(Goal_select)
ocaml(Goptions)
ocaml(Gramlib)
ocaml(Gramlib__Gramext)
ocaml(Gramlib__Grammar)
ocaml(Gramlib__Plexing)
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(Inductive)
ocaml(Inductiveops)
ocaml(InferCumulativity)
ocaml(Int)
ocaml(Inv)
ocaml(Keys)
ocaml(LStream)
ocaml(Lib)
ocaml(Libnames)
ocaml(Libobject)
ocaml(Library)
ocaml(Loadpath)
ocaml(Loc)
ocaml(Locality)
ocaml(Locus)
ocaml(Locusops)
ocaml(Logic)
ocaml(Logic_monad)
ocaml(Ltac2_plugin)
ocaml(Ltac2_plugin__G_ltac2)
ocaml(Ltac2_plugin__Tac2core)
ocaml(Ltac2_plugin__Tac2dyn)
ocaml(Ltac2_plugin__Tac2entries)
ocaml(Ltac2_plugin__Tac2env)
ocaml(Ltac2_plugin__Tac2expr)
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(Ltac_plugin)
ocaml(Ltac_plugin__Coretactics)
ocaml(Ltac_plugin__Evar_tactics)
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_obligations)
ocaml(Ltac_plugin__G_rewrite)
ocaml(Ltac_plugin__G_tactic)
ocaml(Ltac_plugin__Leminv)
ocaml(Ltac_plugin__Pltac)
ocaml(Ltac_plugin__Pptactic)
ocaml(Ltac_plugin__Profile_ltac)
ocaml(Ltac_plugin__Profile_ltac_tactics)
ocaml(Ltac_plugin__Rewrite)
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_plugin__Tactic_option)
ocaml(Ltac_pretype)
ocaml(Metasyntax)
ocaml(Micromega_plugin)
ocaml(Micromega_plugin__Certificate)
ocaml(Micromega_plugin__Coq_micromega)
ocaml(Micromega_plugin__G_micromega)
ocaml(Micromega_plugin__Itv)
ocaml(Micromega_plugin__Mfourier)
ocaml(Micromega_plugin__Micromega)
ocaml(Micromega_plugin__Mutils)
ocaml(Micromega_plugin__NumCompat)
ocaml(Micromega_plugin__Persistent_cache)
ocaml(Micromega_plugin__Polynomial)
ocaml(Micromega_plugin__Simplex)
ocaml(Micromega_plugin__Sos)
ocaml(Micromega_plugin__Sos_lib)
ocaml(Micromega_plugin__Sos_types)
ocaml(Micromega_plugin__Vect)
ocaml(Minisys)
ocaml(Miscprint)
ocaml(Mltop)
ocaml(Mod_subst)
ocaml(Mod_typing)
ocaml(Modintern)
ocaml(Modops)
ocaml(Monad)
ocaml(Namegen)
ocaml(Nameops)
ocaml(Names)
ocaml(Nametab)
ocaml(Nativecode)
ocaml(Nativeconv)
ocaml(Nativelambda)
ocaml(Nativelib)
ocaml(Nativelibrary)
ocaml(Nativenorm)
ocaml(Nativevalues)
ocaml(Notation)
ocaml(Notation_gram)
ocaml(Notation_ops)
ocaml(Notation_term)
ocaml(Notgram_ops)
ocaml(Nsatz_plugin)
ocaml(Nsatz_plugin__G_nsatz)
ocaml(Nsatz_plugin__Ideal)
ocaml(Nsatz_plugin__Nsatz)
ocaml(Nsatz_plugin__Polynom)
ocaml(Nsatz_plugin__Utile)
ocaml(NumTok)
ocaml(Number_string_notation_plugin)
ocaml(Number_string_notation_plugin__G_number_string)
ocaml(Number_string_notation_plugin__Number)
ocaml(Number_string_notation_plugin__String_notation)
ocaml(ObjFile)
ocaml(Opaqueproof)
ocaml(Option)
ocaml(OrderedType)
ocaml(Parray)
ocaml(Partac)
ocaml(Pattern)
ocaml(Patternops)
ocaml(Pcoq)
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(Program)
ocaml(Proof)
ocaml(ProofBlockDelimiter)
ocaml(Proof_bullet)
ocaml(Proof_diffs)
ocaml(Proof_using)
ocaml(Proofview)
ocaml(Proofview_monad)
ocaml(Pvernac)
ocaml(Range)
ocaml(RecLemmas)
ocaml(Record)
ocaml(Redexpr)
ocaml(Redops)
ocaml(Reduction)
ocaml(Reductionops)
ocaml(Refine)
ocaml(Relevanceops)
ocaml(Reserve)
ocaml(RetrieveObl)
ocaml(Retroknowledge)
ocaml(Retyping)
ocaml(Ring_plugin)
ocaml(Ring_plugin__G_ring)
ocaml(Ring_plugin__Ring)
ocaml(Ring_plugin__Ring_ast)
ocaml(Rtauto_plugin)
ocaml(Rtauto_plugin__G_rtauto)
ocaml(Rtauto_plugin__Proof_search)
ocaml(Rtauto_plugin__Refl_tauto)
ocaml(Rtree)
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__Ssrtacticals)
ocaml(Ssreflect_plugin__Ssrvernac)
ocaml(Ssreflect_plugin__Ssrview)
ocaml(Ssrmatching_plugin)
ocaml(Ssrmatching_plugin__G_ssrmatching)
ocaml(Ssrmatching_plugin__Ssrmatching)
ocaml(Ssrsearch_plugin)
ocaml(Ssrsearch_plugin__G_search)
ocaml(Stateid)
ocaml(Stdarg)
ocaml(Stm)
ocaml(Stmargs)
ocaml(Store)
ocaml(Structures)
ocaml(Subtyping)
ocaml(Summary)
ocaml(Syntax_def)
ocaml(System)
ocaml(TQueue)
ocaml(Tacmach)
ocaml(Tacred)
ocaml(Tacticals)
ocaml(Tactics)
ocaml(Tactypes)
ocaml(Tauto_plugin)
ocaml(Tauto_plugin__Tauto)
ocaml(Term)
ocaml(Term_dnet)
ocaml(Term_typing)
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(Type_errors)
ocaml(Typeclasses)
ocaml(Typeclasses_errors)
ocaml(Typeops)
ocaml(Typing)
ocaml(UGraph)
ocaml(UState)
ocaml(Uint63)
ocaml(Unicode)
ocaml(Unicodetable)
ocaml(Unification)
ocaml(Unionfind)
ocaml(Univ)
ocaml(UnivGen)
ocaml(UnivMinim)
ocaml(UnivNames)
ocaml(UnivProblem)
ocaml(UnivSubst)
ocaml(Usage)
ocaml(Util)
ocaml(Vars)
ocaml(Vconv)
ocaml(Vcs)
ocaml(Vernac)
ocaml(Vernac_classifier)
ocaml(Vernacentries)
ocaml(Vernacexpr)
ocaml(Vernacextend)
ocaml(Vernacinterp)
ocaml(Vernacprop)
ocaml(Vernacstate)
ocaml(Vio_checking)
ocaml(Vm)
ocaml(Vmbytecodes)
ocaml(Vmbytegen)
ocaml(Vmemitcodes)
ocaml(Vmlambda)
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)
ocamlx(Abstract)
ocamlx(AcyclicGraph)
ocamlx(Arguments_renaming)
ocamlx(Assumptions)
ocamlx(AsyncTaskQueue)
ocamlx(Attributes)
ocamlx(Auto)
ocamlx(Auto_ind_decl)
ocamlx(Autorewrite)
ocamlx(Aux_file)
ocamlx(Btauto_plugin)
ocamlx(Btauto_plugin__G_btauto)
ocamlx(Btauto_plugin__Refl_btauto)
ocamlx(Btermdn)
ocamlx(CArray)
ocamlx(CAst)
ocamlx(CClosure)
ocamlx(CDebug)
ocamlx(CEphemeron)
ocamlx(CErrors)
ocamlx(CLexer)
ocamlx(CList)
ocamlx(CMap)
ocamlx(CObj)
ocamlx(CPath)
ocamlx(CPrimitives)
ocamlx(CProfile)
ocamlx(CSet)
ocamlx(CString)
ocamlx(CThread)
ocamlx(CUnix)
ocamlx(CWarnings)
ocamlx(Canonical)
ocamlx(Cases)
ocamlx(Cbn)
ocamlx(Cbv)
ocamlx(Cc_plugin)
ocamlx(Cc_plugin__Ccalgo)
ocamlx(Cc_plugin__Ccproof)
ocamlx(Cc_plugin__Cctac)
ocamlx(Cc_plugin__G_congruence)
ocamlx(Ccompile)
ocamlx(Class_tactics)
ocamlx(Classes)
ocamlx(Clenv)
ocamlx(Coercion)
ocamlx(Coercionops)
ocamlx(ComArguments)
ocamlx(ComAssumption)
ocamlx(ComCoercion)
ocamlx(ComDefinition)
ocamlx(ComFixpoint)
ocamlx(ComHints)
ocamlx(ComInductive)
ocamlx(ComPrimitive)
ocamlx(ComProgramFixpoint)
ocamlx(ComSearch)
ocamlx(ComTactic)
ocamlx(Constr)
ocamlx(Constr_matching)
ocamlx(Constrexpr)
ocamlx(Constrexpr_ops)
ocamlx(Constrextern)
ocamlx(Constrintern)
ocamlx(Context)
ocamlx(Contradiction)
ocamlx(Control)
ocamlx(Conv_oracle)
ocamlx(Cooking)
ocamlx(CoqProject_file)
ocamlx(Coq_config)
ocamlx(Coqargs)
ocamlx(Coqc)
ocamlx(Coqcargs)
ocamlx(Coqinit)
ocamlx(Coqlib)
ocamlx(Coqloadpath)
ocamlx(Coqloop)
ocamlx(Coqrc)
ocamlx(Coqrun)
ocamlx(Coqtop)
ocamlx(CoqworkmgrApi)
ocamlx(DAst)
ocamlx(Dag)
ocamlx(DebugHook)
ocamlx(Declarations)
ocamlx(Declare)
ocamlx(DeclareInd)
ocamlx(DeclareScheme)
ocamlx(DeclareUctx)
ocamlx(DeclareUniv)
ocamlx(Declaremods)
ocamlx(Declareops)
ocamlx(Decls)
ocamlx(Deprecation)
ocamlx(Derive_plugin)
ocamlx(Derive_plugin__Derive)
ocamlx(Derive_plugin__G_derive)
ocamlx(Detyping)
ocamlx(Diff2)
ocamlx(Dn)
ocamlx(Dnet)
ocamlx(Dumpglob)
ocamlx(Dyn)
ocamlx(EConstr)
ocamlx(Eauto)
ocamlx(Egramcoq)
ocamlx(Egramml)
ocamlx(Elim)
ocamlx(Elimschemes)
ocamlx(Entries)
ocamlx(Envars)
ocamlx(Environ)
ocamlx(Eqdecide)
ocamlx(Eqschemes)
ocamlx(Equality)
ocamlx(Esubst)
ocamlx(Evar)
ocamlx(Evar_kinds)
ocamlx(Evar_refiner)
ocamlx(Evarconv)
ocamlx(Evardefine)
ocamlx(Evarsolve)
ocamlx(Evarutil)
ocamlx(Evd)
ocamlx(Exninfo)
ocamlx(Explore)
ocamlx(Extend)
ocamlx(Extraction_plugin)
ocamlx(Extraction_plugin__Big)
ocamlx(Extraction_plugin__Common)
ocamlx(Extraction_plugin__Extract_env)
ocamlx(Extraction_plugin__Extraction)
ocamlx(Extraction_plugin__G_extraction)
ocamlx(Extraction_plugin__Haskell)
ocamlx(Extraction_plugin__Json)
ocamlx(Extraction_plugin__Miniml)
ocamlx(Extraction_plugin__Mlutil)
ocamlx(Extraction_plugin__Modutil)
ocamlx(Extraction_plugin__Ocaml)
ocamlx(Extraction_plugin__Scheme)
ocamlx(Extraction_plugin__Table)
ocamlx(Feedback)
ocamlx(Find_subterm)
ocamlx(Firstorder_plugin)
ocamlx(Firstorder_plugin__Formula)
ocamlx(Firstorder_plugin__G_ground)
ocamlx(Firstorder_plugin__Ground)
ocamlx(Firstorder_plugin__Instances)
ocamlx(Firstorder_plugin__Rules)
ocamlx(Firstorder_plugin__Sequent)
ocamlx(Firstorder_plugin__Unify)
ocamlx(Flags)
ocamlx(Float64)
ocamlx(Float64_common)
ocamlx(Float_syntax_plugin)
ocamlx(Float_syntax_plugin__Float_syntax)
ocamlx(Ftactic)
ocamlx(Funind_plugin)
ocamlx(Funind_plugin__Functional_principles_proofs)
ocamlx(Funind_plugin__Functional_principles_types)
ocamlx(Funind_plugin__G_indfun)
ocamlx(Funind_plugin__Gen_principle)
ocamlx(Funind_plugin__Glob_term_to_relation)
ocamlx(Funind_plugin__Glob_termops)
ocamlx(Funind_plugin__Indfun)
ocamlx(Funind_plugin__Indfun_common)
ocamlx(Funind_plugin__Invfun)
ocamlx(Funind_plugin__Recdef)
ocamlx(Future)
ocamlx(G_constr)
ocamlx(G_prim)
ocamlx(G_proofs)
ocamlx(G_toplevel)
ocamlx(G_vernac)
ocamlx(Genarg)
ocamlx(Genintern)
ocamlx(Geninterp)
ocamlx(Genprint)
ocamlx(Genredexpr)
ocamlx(GlobEnv)
ocamlx(Glob_ops)
ocamlx(Glob_term)
ocamlx(Global)
ocamlx(Globnames)
ocamlx(Goal)
ocamlx(Goal_select)
ocamlx(Goptions)
ocamlx(Gramlib)
ocamlx(Gramlib__Gramext)
ocamlx(Gramlib__Grammar)
ocamlx(Gramlib__Plexing)
ocamlx(HMap)
ocamlx(Hashcons)
ocamlx(Hashset)
ocamlx(Heads)
ocamlx(Heap)
ocamlx(Himsg)
ocamlx(Hints)
ocamlx(Hipattern)
ocamlx(Hook)
ocamlx(IStream)
ocamlx(Impargs)
ocamlx(Implicit_quantifiers)
ocamlx(IndTyping)
ocamlx(Ind_tables)
ocamlx(Indrec)
ocamlx(Indschemes)
ocamlx(Indtypes)
ocamlx(Inductive)
ocamlx(Inductiveops)
ocamlx(InferCumulativity)
ocamlx(Int)
ocamlx(Inv)
ocamlx(Keys)
ocamlx(LStream)
ocamlx(Lib)
ocamlx(Libnames)
ocamlx(Libobject)
ocamlx(Library)
ocamlx(Loadpath)
ocamlx(Loc)
ocamlx(Locality)
ocamlx(Locus)
ocamlx(Locusops)
ocamlx(Logic)
ocamlx(Logic_monad)
ocamlx(Ltac2_plugin)
ocamlx(Ltac2_plugin__G_ltac2)
ocamlx(Ltac2_plugin__Tac2core)
ocamlx(Ltac2_plugin__Tac2dyn)
ocamlx(Ltac2_plugin__Tac2entries)
ocamlx(Ltac2_plugin__Tac2env)
ocamlx(Ltac2_plugin__Tac2extffi)
ocamlx(Ltac2_plugin__Tac2ffi)
ocamlx(Ltac2_plugin__Tac2intern)
ocamlx(Ltac2_plugin__Tac2interp)
ocamlx(Ltac2_plugin__Tac2match)
ocamlx(Ltac2_plugin__Tac2print)
ocamlx(Ltac2_plugin__Tac2quote)
ocamlx(Ltac2_plugin__Tac2stdlib)
ocamlx(Ltac2_plugin__Tac2tactics)
ocamlx(Ltac_plugin)
ocamlx(Ltac_plugin__Coretactics)
ocamlx(Ltac_plugin__Evar_tactics)
ocamlx(Ltac_plugin__Extraargs)
ocamlx(Ltac_plugin__Extratactics)
ocamlx(Ltac_plugin__G_auto)
ocamlx(Ltac_plugin__G_class)
ocamlx(Ltac_plugin__G_eqdecide)
ocamlx(Ltac_plugin__G_ltac)
ocamlx(Ltac_plugin__G_obligations)
ocamlx(Ltac_plugin__G_rewrite)
ocamlx(Ltac_plugin__G_tactic)
ocamlx(Ltac_plugin__Leminv)
ocamlx(Ltac_plugin__Pltac)
ocamlx(Ltac_plugin__Pptactic)
ocamlx(Ltac_plugin__Profile_ltac)
ocamlx(Ltac_plugin__Profile_ltac_tactics)
ocamlx(Ltac_plugin__Rewrite)
ocamlx(Ltac_plugin__Tacarg)
ocamlx(Ltac_plugin__Taccoerce)
ocamlx(Ltac_plugin__Tacentries)
ocamlx(Ltac_plugin__Tacenv)
ocamlx(Ltac_plugin__Tacexpr)
ocamlx(Ltac_plugin__Tacintern)
ocamlx(Ltac_plugin__Tacinterp)
ocamlx(Ltac_plugin__Tacsubst)
ocamlx(Ltac_plugin__Tactic_debug)
ocamlx(Ltac_plugin__Tactic_matching)
ocamlx(Ltac_plugin__Tactic_option)
ocamlx(Ltac_pretype)
ocamlx(Metasyntax)
ocamlx(Micromega_plugin)
ocamlx(Micromega_plugin__Certificate)
ocamlx(Micromega_plugin__Coq_micromega)
ocamlx(Micromega_plugin__G_micromega)
ocamlx(Micromega_plugin__Itv)
ocamlx(Micromega_plugin__Mfourier)
ocamlx(Micromega_plugin__Micromega)
ocamlx(Micromega_plugin__Mutils)
ocamlx(Micromega_plugin__NumCompat)
ocamlx(Micromega_plugin__Persistent_cache)
ocamlx(Micromega_plugin__Polynomial)
ocamlx(Micromega_plugin__Simplex)
ocamlx(Micromega_plugin__Sos)
ocamlx(Micromega_plugin__Sos_lib)
ocamlx(Micromega_plugin__Sos_types)
ocamlx(Micromega_plugin__Vect)
ocamlx(Minisys)
ocamlx(Miscprint)
ocamlx(Mltop)
ocamlx(Mod_subst)
ocamlx(Mod_typing)
ocamlx(Modintern)
ocamlx(Modops)
ocamlx(Monad)
ocamlx(Namegen)
ocamlx(Nameops)
ocamlx(Names)
ocamlx(Nametab)
ocamlx(Nativecode)
ocamlx(Nativeconv)
ocamlx(Nativelambda)
ocamlx(Nativelib)
ocamlx(Nativelibrary)
ocamlx(Nativenorm)
ocamlx(Nativevalues)
ocamlx(Notation)
ocamlx(Notation_gram)
ocamlx(Notation_ops)
ocamlx(Notation_term)
ocamlx(Notgram_ops)
ocamlx(Nsatz_plugin)
ocamlx(Nsatz_plugin__G_nsatz)
ocamlx(Nsatz_plugin__Ideal)
ocamlx(Nsatz_plugin__Nsatz)
ocamlx(Nsatz_plugin__Polynom)
ocamlx(Nsatz_plugin__Utile)
ocamlx(NumTok)
ocamlx(Number_string_notation_plugin)
ocamlx(Number_string_notation_plugin__G_number_string)
ocamlx(Number_string_notation_plugin__Number)
ocamlx(Number_string_notation_plugin__String_notation)
ocamlx(ObjFile)
ocamlx(Opaqueproof)
ocamlx(Option)
ocamlx(OrderedType)
ocamlx(Parray)
ocamlx(Partac)
ocamlx(Pattern)
ocamlx(Patternops)
ocamlx(Pcoq)
ocamlx(Pp)
ocamlx(Pp_diff)
ocamlx(Ppconstr)
ocamlx(Ppextend)
ocamlx(Ppred)
ocamlx(Pputils)
ocamlx(Ppvernac)
ocamlx(Predicate)
ocamlx(Prettyp)
ocamlx(Pretype_errors)
ocamlx(Pretyping)
ocamlx(Primred)
ocamlx(Printer)
ocamlx(Printmod)
ocamlx(Program)
ocamlx(Proof)
ocamlx(ProofBlockDelimiter)
ocamlx(Proof_bullet)
ocamlx(Proof_diffs)
ocamlx(Proof_using)
ocamlx(Proofview)
ocamlx(Proofview_monad)
ocamlx(Pvernac)
ocamlx(Range)
ocamlx(RecLemmas)
ocamlx(Record)
ocamlx(Redexpr)
ocamlx(Redops)
ocamlx(Reduction)
ocamlx(Reductionops)
ocamlx(Refine)
ocamlx(Relevanceops)
ocamlx(Reserve)
ocamlx(RetrieveObl)
ocamlx(Retroknowledge)
ocamlx(Retyping)
ocamlx(Ring_plugin)
ocamlx(Ring_plugin__G_ring)
ocamlx(Ring_plugin__Ring)
ocamlx(Ring_plugin__Ring_ast)
ocamlx(Rtauto_plugin)
ocamlx(Rtauto_plugin__G_rtauto)
ocamlx(Rtauto_plugin__Proof_search)
ocamlx(Rtauto_plugin__Refl_tauto)
ocamlx(Rtree)
ocamlx(Safe_typing)
ocamlx(Search)
ocamlx(Section)
ocamlx(Segmenttree)
ocamlx(Smartlocate)
ocamlx(Sorts)
ocamlx(Spawn)
ocamlx(Spawned)
ocamlx(Ssreflect_plugin)
ocamlx(Ssreflect_plugin__Ssrbwd)
ocamlx(Ssreflect_plugin__Ssrcommon)
ocamlx(Ssreflect_plugin__Ssrelim)
ocamlx(Ssreflect_plugin__Ssrequality)
ocamlx(Ssreflect_plugin__Ssrfwd)
ocamlx(Ssreflect_plugin__Ssripats)
ocamlx(Ssreflect_plugin__Ssrparser)
ocamlx(Ssreflect_plugin__Ssrprinters)
ocamlx(Ssreflect_plugin__Ssrtacticals)
ocamlx(Ssreflect_plugin__Ssrvernac)
ocamlx(Ssreflect_plugin__Ssrview)
ocamlx(Ssrmatching_plugin)
ocamlx(Ssrmatching_plugin__G_ssrmatching)
ocamlx(Ssrmatching_plugin__Ssrmatching)
ocamlx(Ssrsearch_plugin)
ocamlx(Ssrsearch_plugin__G_search)
ocamlx(Stateid)
ocamlx(Stdarg)
ocamlx(Stm)
ocamlx(Stmargs)
ocamlx(Store)
ocamlx(Structures)
ocamlx(Subtyping)
ocamlx(Summary)
ocamlx(Syntax_def)
ocamlx(System)
ocamlx(TQueue)
ocamlx(Tacmach)
ocamlx(Tacred)
ocamlx(Tacticals)
ocamlx(Tactics)
ocamlx(Tactypes)
ocamlx(Tauto_plugin)
ocamlx(Tauto_plugin__Tauto)
ocamlx(Term)
ocamlx(Term_dnet)
ocamlx(Term_typing)
ocamlx(Terminal)
ocamlx(Termops)
ocamlx(Tok)
ocamlx(Top_printers)
ocamlx(Topfmt)
ocamlx(TransparentState)
ocamlx(Trie)
ocamlx(Tuto0_plugin)
ocamlx(Tuto0_plugin__G_tuto0)
ocamlx(Tuto0_plugin__Tuto0_main)
ocamlx(Tuto1_plugin)
ocamlx(Tuto1_plugin__G_tuto1)
ocamlx(Tuto1_plugin__Inspector)
ocamlx(Tuto1_plugin__Simple_check)
ocamlx(Tuto1_plugin__Simple_declare)
ocamlx(Tuto1_plugin__Simple_print)
ocamlx(Tuto2_plugin)
ocamlx(Tuto2_plugin__Counter)
ocamlx(Tuto2_plugin__Custom)
ocamlx(Tuto2_plugin__G_tuto2)
ocamlx(Tuto2_plugin__Persistent_counter)
ocamlx(Tuto3_plugin)
ocamlx(Tuto3_plugin__Construction_game)
ocamlx(Tuto3_plugin__G_tuto3)
ocamlx(Tuto3_plugin__Tuto_tactic)
ocamlx(Type_errors)
ocamlx(Typeclasses)
ocamlx(Typeclasses_errors)
ocamlx(Typeops)
ocamlx(Typing)
ocamlx(UGraph)
ocamlx(UState)
ocamlx(Uint63)
ocamlx(Unicode)
ocamlx(Unicodetable)
ocamlx(Unification)
ocamlx(Unionfind)
ocamlx(Univ)
ocamlx(UnivGen)
ocamlx(UnivMinim)
ocamlx(UnivNames)
ocamlx(UnivProblem)
ocamlx(UnivSubst)
ocamlx(Usage)
ocamlx(Util)
ocamlx(Vars)
ocamlx(Vconv)
ocamlx(Vcs)
ocamlx(Vernac)
ocamlx(Vernac_classifier)
ocamlx(Vernacentries)
ocamlx(Vernacexpr)
ocamlx(Vernacextend)
ocamlx(Vernacinterp)
ocamlx(Vernacprop)
ocamlx(Vernacstate)
ocamlx(Vio_checking)
ocamlx(Vm)
ocamlx(Vmbytecodes)
ocamlx(Vmbytegen)
ocamlx(Vmemitcodes)
ocamlx(Vmlambda)
ocamlx(Vmopcodes)
ocamlx(Vmsymtable)
ocamlx(Vmvalues)
ocamlx(Vnorm)
ocamlx(WorkerLoop)
ocamlx(WorkerPool)
ocamlx(Zify_plugin)
ocamlx(Zify_plugin__G_zify)
ocamlx(Zify_plugin__Zify)

Files

usr/
- bin/
  - coq-tex
  - coq_makefile
  - coqc
  - coqc.byte
  - coqchk
  - coqdep
  - coqdoc
  - coqnative
  - coqpp
  - coqproofworker.opt
  - coqqueryworker.opt
  - coqtacticworker.opt
  - coqtop
  - coqtop.byte
  - coqtop.opt
  - coqwc
  - coqworkmgr
  - csdpcert
  - ocamllibdep
  - votour
- lib/
  - .build-id/
    - 00/
      - 6bb5454b2a3d4a920018a4bfa28ce5f109c20e
    - 02/
      - bd6d3344f68958e743a68a25453a2b3fe1ebd2
    - 0c/
      - 417eed79ccb6493f4d631c68387bf99c0a3a25
    - 0f/
      - 9fa3ec5b51a92226874595487871185239b0f3
    - 23/
      - a7305353f0b0678eeaa9492b46cb6b827fa1ae
    - 2b/
      - dbf96569829cdd6c4303971325ba3145e655a6
    - 35/
      - a21b79ce0b1a75e1a8c35de7f87aadccdeb15c
    - 3a/
      - 4673ae04224aababd759b82a8bbc4feed2070b
      - ce455df9c18398b2d8cb27a76fce335a53c172
    - 45/
      - d13c6fa939576e24c7580a2c625c3bafc98510
    - 47/
      - 298762e01cfaeef880ce1701a51cab470db746
      - 4aa949ec28317c2e43fa81964aa3aa21d1fb4c
    - 48/
      - 31abc33568c3f38509aa694da9e3792fe1b8ed
    - 4c/
      - ef223591c2369760a74ec21dba5c156500f6cf
    - 52/
      - ec0cdc700b8dc8fcda36a676ea43b2139ddcd5
    - 56/
      - a3f777471518698709a8508ad9de6a58ad6d8a
    - 57/
      - 51a48c77d9977996057760f92ce97bf2746cac
    - 62/
      - e25d367f87872c8dbc2c11d3c085e5df416e7f
    - 68/
      - 4bc60a40b0097bf0b308ac144b2d8fa97c8d65
    - 6d/
      - 3862c9bb801b23b985639630b1a07abccac8b3
    - 6f/
      - 94641c7813a5a4c6a6cf411be5f377444e60e5
    - 70/
      - d8bac81514e4286b1500c09e44f2c4157160bc
    - 74/
      - 709d2a26f051a2f085bd065f61ed32ac0c07bf
    - 79/
      - 613e76dff6728bcc20added9c55f571d05b4a5
    - 7a/
      - 14e2512d04607ae32538e626802041d1e50f64
    - 7c/
      - 66d1e76bbae04852d50a72723a07e2fc575de5
    - 81/
      - bf906231c4c419816819d8f91aba8df4fb208a
    - 83/
      - f7b8aa3b896a74444c1881c5d9f9b26dcd68f7
    - 85/
      - c63dc70769191c847020e5eeb3aee7e3063d42
    - 86/
      - a92adfeb820fe2fa87b3e30c07aa6c9a5730c0
    - 88/
      - 3138493f2f98019d9daaca85cf47784fd57a0d
    - 8a/
      - 9e186822765147a2c4bc0313a640155ff62447
    - 8d/
      - 73208b6f787ad5734eda0f7201da09e81508a1
    - 92/
      - 6046f947a4e46e1d69ea010de1aea8f387571b
    - 9a/
      - 3e7f3bc6ad3a49f8e9ec04b5640ee3900afb12
    - a1/
      - 7d38331bed591c713c969d4d27d65dd2df80ad
    - a5/
      - 13864d0afb540b72015648a6d330981fffd00b
    - a7/
      - ac5bae2fe8f9876bdad4a6bca5c7aea9f7e456
    - a9/
      - 65b8a82cfd3f72a3d01d051a94fa0f6c5fc6ee
    - af/
      - 56d309c4bee1fb9289843d371b99eeb5e4eb70
    - b5/
      - a60a2c6387215323cd26c9824038593e1142b3
    - b6/
      - 0541ac627e232e9cdd18d7b63c7910b7c9f03f
    - b7/
      - 745fdab5a909c602bea409d8fd9f52faf7e5fb
    - ba/
      - 81e419d39cd6435ca1f8669439416ede1db509
    - c2/
      - 742154a99b72a0c0ee6f0fe9c4dd757ae07228
    - c4/
      - 86ba077b3accda44d9a4888fff38b674a7fe5c
    - c6/
      - c8061e60dd3b5fe5cfada5073e70bbce474b16
    - c7/
      - 653595a5c605b22df1d6650ce1ae6ccab0bf18
      - ee2daae9b8b128b757b0e975a4dc4ae217a51a
    - c8/
      - 6cdd6b64834b218d12b80361d8fc82e8825a5e
    - d7/
      - cff1e45a5074841298fb1fce0a3a21def71010
    - de/
      - 349b54b32b3705884d935e370e33cda9cd0bdb
    - e5/
      - 59b4a3c0d1ecc1b701df9d93af53fbfa5408b7
    - e9/
      - 33914f1688f531985425dc5b604cce72d96c87
      - 4e577c55f398c40ca110c02f250980675b7b6c
    - ed/
      - 707bae4694a33334b30ece08f5de326f764923
    - ee/
      - 8dccf5a44b428719a480249cd848d9fbd7a45f
      - b464b985556eed25a2ff5a5528d73bfc7e479b
    - f3/
      - 3cc5b49467206249f1f3a85e901d50b3e22be1
    - fb/
      - 8d3d61348d3b48ad8632a3e5a4442517d96ee0
      - 8d3d61348d3b48ad8632a3e5a4442517d96ee0.1
- lib64/
  - ocaml/
    - coq-core/
      - META
      - clib/
        
        cArray.cmi
        
        cArray.cmt
        
        cArray.cmti
        
        cArray.cmx
        
        cArray.ml
        
        cArray.mli
        
        cEphemeron.cmi
        
        cEphemeron.cmt
        
        cEphemeron.cmti
        
        cEphemeron.cmx
        
        cEphemeron.ml
        
        cEphemeron.mli
        
        cList.cmi
        
        cList.cmt
        
        cList.cmti
        
        cList.cmx
        
        cList.ml
        
        cList.mli
        
        cMap.cmi
        
        cMap.cmt
        
        cMap.cmti
        
        cMap.cmx
        
        cMap.ml
        
        cMap.mli
        
        cObj.cmi
        
        cObj.cmt
        
        cObj.cmti
        
        cObj.cmx
        
        cObj.ml
        
        cObj.mli
        
        cPath.cmi
        
        cPath.cmt
        
        cPath.cmti
        
        cPath.cmx
        
        cPath.ml
        
        cPath.mli
        
        cSet.cmi
        
        cSet.cmt
        
        cSet.cmti
        
        cSet.cmx
        
        cSet.ml
        
        cSet.mli
        
        cSig.cmi
        
        cSig.cmti
        
        cSig.mli
        
        cString.cmi
        
        cString.cmt
        
        cString.cmti
        
        cString.cmx
        
        cString.ml
        
        cString.mli
        
        cThread.cmi
        
        cThread.cmt
        
        cThread.cmti
        
        cThread.cmx
        
        cThread.ml
        
        cThread.mli
        
        cUnix.cmi
        
        cUnix.cmt
        
        cUnix.cmti
        
        cUnix.cmx
        
        cUnix.ml
        
        cUnix.mli
        
        clib.a
        
        clib.cma
        
        clib.cmxa
        
        clib.cmxs
        
        diff2.cmi
        
        diff2.cmt
        
        diff2.cmti
        
        diff2.cmx
        
        diff2.ml
        
        diff2.mli
        
        dyn.cmi
        
        dyn.cmt
        
        dyn.cmti
        
        dyn.cmx
        
        dyn.ml
        
        dyn.mli
        
        exninfo.cmi
        
        exninfo.cmt
        
        exninfo.cmti
        
        exninfo.cmx
        
        exninfo.ml
        
        exninfo.mli
        
        hMap.cmi
        
        hMap.cmt
        
        hMap.cmti
        
        hMap.cmx
        
        hMap.ml
        
        hMap.mli
        
        hashcons.cmi
        
        hashcons.cmt
        
        hashcons.cmti
        
        hashcons.cmx
        
        hashcons.ml
        
        hashcons.mli
        
        hashset.cmi
        
        hashset.cmt
        
        hashset.cmti
        
        hashset.cmx
        
        hashset.ml
        
        hashset.mli
        
        heap.cmi
        
        heap.cmt
        
        heap.cmti
        
        heap.cmx
        
        heap.ml
        
        heap.mli
        
        iStream.cmi
        
        iStream.cmt
        
        iStream.cmti
        
        iStream.cmx
        
        iStream.ml
        
        iStream.mli
        
        int.cmi
        
        int.cmt
        
        int.cmti
        
        int.cmx
        
        int.ml
        
        int.mli
        
        minisys.cmi
        
        minisys.cmt
        
        minisys.cmx
        
        minisys.ml
        
        monad.cmi
        
        monad.cmt
        
        monad.cmti
        
        monad.cmx
        
        monad.ml
        
        monad.mli
        
        option.cmi
        
        option.cmt
        
        option.cmti
        
        option.cmx
        
        option.ml
        
        option.mli
        
        orderedType.cmi
        
        orderedType.cmt
        
        orderedType.cmti
        
        orderedType.cmx
        
        orderedType.ml
        
        orderedType.mli
        
        predicate.cmi
        
        predicate.cmt
        
        predicate.cmti
        
        predicate.cmx
        
        predicate.ml
        
        predicate.mli
        
        range.cmi
        
        range.cmt
        
        range.cmti
        
        range.cmx
        
        range.ml
        
        range.mli
        
        segmenttree.cmi
        
        segmenttree.cmt
        
        segmenttree.cmti
        
        segmenttree.cmx
        
        segmenttree.ml
        
        segmenttree.mli
        
        store.cmi
        
        store.cmt
        
        store.cmti
        
        store.cmx
        
        store.ml
        
        store.mli
        
        terminal.cmi
        
        terminal.cmt
        
        terminal.cmti
        
        terminal.cmx
        
        terminal.ml
        
        terminal.mli
        
        trie.cmi
        
        trie.cmt
        
        trie.cmti
        
        trie.cmx
        
        trie.ml
        
        trie.mli
        
        unicode.cmi
        
        unicode.cmt
        
        unicode.cmti
        
        unicode.cmx
        
        unicode.ml
        
        unicode.mli
        
        unicodetable.cmi
        
        unicodetable.cmt
        
        unicodetable.cmx
        
        unicodetable.ml
        
        unionfind.cmi
        
        unionfind.cmt
        
        unionfind.cmti
        
        unionfind.cmx
        
        unionfind.ml
        
        unionfind.mli
      - config/
        
        config.a
        
        config.cma
        
        config.cmxa
        
        config.cmxs
        
        coq_config.cmi
        
        coq_config.cmt
        
        coq_config.cmti
        
        coq_config.cmx
        
        coq_config.ml
        
        coq_config.mli
      - dune-package
      - engine/
        
        eConstr.cmi
        
        eConstr.cmt
        
        eConstr.cmti
        
        eConstr.cmx
        
        eConstr.ml
        
        eConstr.mli
        
        engine.a
        
        engine.cma
        
        engine.cmxa
        
        engine.cmxs
        
        evar_kinds.cmi
        
        evar_kinds.cmt
        
        evar_kinds.cmti
        
        evar_kinds.cmx
        
        evar_kinds.ml
        
        evar_kinds.mli
        
        evarutil.cmi
        
        evarutil.cmt
        
        evarutil.cmti
        
        evarutil.cmx
        
        evarutil.ml
        
        evarutil.mli
        
        evd.cmi
        
        evd.cmt
        
        evd.cmti
        
        evd.cmx
        
        evd.ml
        
        evd.mli
        
        ftactic.cmi
        
        ftactic.cmt
        
        ftactic.cmti
        
        ftactic.cmx
        
        ftactic.ml
        
        ftactic.mli
        
        logic_monad.cmi
        
        logic_monad.cmt
        
        logic_monad.cmti
        
        logic_monad.cmx
        
        logic_monad.ml
        
        logic_monad.mli
        
        namegen.cmi
        
        namegen.cmt
        
        namegen.cmti
        
        namegen.cmx
        
        namegen.ml
        
        namegen.mli
        
        nameops.cmi
        
        nameops.cmt
        
        nameops.cmti
        
        nameops.cmx
        
        nameops.ml
        
        nameops.mli
        
        proofview.cmi
        
        proofview.cmt
        
        proofview.cmti
        
        proofview.cmx
        
        proofview.ml
        
        proofview.mli
        
        proofview_monad.cmi
        
        proofview_monad.cmt
        
        proofview_monad.cmti
        
        proofview_monad.cmx
        
        proofview_monad.ml
        
        proofview_monad.mli
        
        termops.cmi
        
        termops.cmt
        
        termops.cmti
        
        termops.cmx
        
        termops.ml
        
        termops.mli
        
        uState.cmi
        
        uState.cmt
        
        uState.cmti
        
        uState.cmx
        
        uState.ml
        
        uState.mli
        
        univGen.cmi
        
        univGen.cmt
        
        univGen.cmti
        
        univGen.cmx
        
        univGen.ml
        
        univGen.mli
        
        univMinim.cmi
        
        univMinim.cmt
        
        univMinim.cmti
        
        univMinim.cmx
        
        univMinim.ml
        
        univMinim.mli
        
        univNames.cmi
        
        univNames.cmt
        
        univNames.cmti
        
        univNames.cmx
        
        univNames.ml
        
        univNames.mli
        
        univProblem.cmi
        
        univProblem.cmt
        
        univProblem.cmti
        
        univProblem.cmx
        
        univProblem.ml
        
        univProblem.mli
        
        univSubst.cmi
        
        univSubst.cmt
        
        univSubst.cmti
        
        univSubst.cmx
        
        univSubst.ml
        
        univSubst.mli
      - gramlib/
        
        gramext.ml
        
        gramext.mli
        
        gramlib.a
        
        gramlib.cma
        
        gramlib.cmi
        
        gramlib.cmt
        
        gramlib.cmx
        
        gramlib.cmxa
        
        gramlib.cmxs
        
        gramlib.ml
        
        gramlib__Gramext.cmi
        
        gramlib__Gramext.cmt
        
        gramlib__Gramext.cmti
        
        gramlib__Gramext.cmx
        
        gramlib__Grammar.cmi
        
        gramlib__Grammar.cmt
        
        gramlib__Grammar.cmti
        
        gramlib__Grammar.cmx
        
        gramlib__Plexing.cmi
        
        gramlib__Plexing.cmt
        
        gramlib__Plexing.cmti
        
        gramlib__Plexing.cmx
        
        grammar.ml
        
        grammar.mli
        
        plexing.ml
        
        plexing.mli
      - interp/
        
        constrexpr.cmi
        
        constrexpr.cmt
        
        constrexpr.cmx
        
        constrexpr.ml
        
        constrexpr_ops.cmi
        
        constrexpr_ops.cmt
        
        constrexpr_ops.cmti
        
        constrexpr_ops.cmx
        
        constrexpr_ops.ml
        
        constrexpr_ops.mli
        
        constrextern.cmi
        
        constrextern.cmt
        
        constrextern.cmti
        
        constrextern.cmx
        
        constrextern.ml
        
        constrextern.mli
        
        constrintern.cmi
        
        constrintern.cmt
        
        constrintern.cmti
        
        constrintern.cmx
        
        constrintern.ml
        
        constrintern.mli
        
        decls.cmi
        
        decls.cmt
        
        decls.cmti
        
        decls.cmx
        
        decls.ml
        
        decls.mli
        
        deprecation.cmi
        
        deprecation.cmt
        
        deprecation.cmti
        
        deprecation.cmx
        
        deprecation.ml
        
        deprecation.mli
        
        dumpglob.cmi
        
        dumpglob.cmt
        
        dumpglob.cmti
        
        dumpglob.cmx
        
        dumpglob.ml
        
        dumpglob.mli
        
        genintern.cmi
        
        genintern.cmt
        
        genintern.cmti
        
        genintern.cmx
        
        genintern.ml
        
        genintern.mli
        
        impargs.cmi
        
        impargs.cmt
        
        impargs.cmti
        
        impargs.cmx
        
        impargs.ml
        
        impargs.mli
        
        implicit_quantifiers.cmi
        
        implicit_quantifiers.cmt
        
        implicit_quantifiers.cmti
        
        implicit_quantifiers.cmx
        
        implicit_quantifiers.ml
        
        implicit_quantifiers.mli
        
        interp.a
        
        interp.cma
        
        interp.cmxa
        
        interp.cmxs
        
        modintern.cmi
        
        modintern.cmt
        
        modintern.cmti
        
        modintern.cmx
        
        modintern.ml
        
        modintern.mli
        
        notation.cmi
        
        notation.cmt
        
        notation.cmti
        
        notation.cmx
        
        notation.ml
        
        notation.mli
        
        notation_ops.cmi
        
        notation_ops.cmt
        
        notation_ops.cmti
        
        notation_ops.cmx
        
        notation_ops.ml
        
        notation_ops.mli
        
        notation_term.cmi
        
        notation_term.cmt
        
        notation_term.cmx
        
        notation_term.ml
        
        numTok.cmi
        
        numTok.cmt
        
        numTok.cmti
        
        numTok.cmx
        
        numTok.ml
        
        numTok.mli
        
        reserve.cmi
        
        reserve.cmt
        
        reserve.cmti
        
        reserve.cmx
        
        reserve.ml
        
        reserve.mli
        
        smartlocate.cmi
        
        smartlocate.cmt
        
        smartlocate.cmti
        
        smartlocate.cmx
        
        smartlocate.ml
        
        smartlocate.mli
        
        stdarg.cmi
        
        stdarg.cmt
        
        stdarg.cmti
        
        stdarg.cmx
        
        stdarg.ml
        
        stdarg.mli
        
        syntax_def.cmi
        
        syntax_def.cmt
        
        syntax_def.cmti
        
        syntax_def.cmx
        
        syntax_def.ml
        
        syntax_def.mli
      - kernel/
        
        cClosure.cmi
        
        cClosure.cmt
        
        cClosure.cmti
        
        cClosure.cmx
        
        cClosure.ml
        
        cClosure.mli
        
        cPrimitives.cmi
        
        cPrimitives.cmt
        
        cPrimitives.cmti
        
        cPrimitives.cmx
        
        cPrimitives.ml
        
        cPrimitives.mli
        
        constr.cmi
        
        constr.cmt
        
        constr.cmti
        
        constr.cmx
        
        constr.ml
        
        constr.mli
        
        context.cmi
        
        context.cmt
        
        context.cmti
        
        context.cmx
        
        context.ml
        
        context.mli
        
        conv_oracle.cmi
        
        conv_oracle.cmt
        
        conv_oracle.cmti
        
        conv_oracle.cmx
        
        conv_oracle.ml
        
        conv_oracle.mli
        
        cooking.cmi
        
        cooking.cmt
        
        cooking.cmti
        
        cooking.cmx
        
        cooking.ml
        
        cooking.mli
        
        declarations.cmi
        
        declarations.cmt
        
        declarations.cmx
        
        declarations.ml
        
        declareops.cmi
        
        declareops.cmt
        
        declareops.cmti
        
        declareops.cmx
        
        declareops.ml
        
        declareops.mli
        
        entries.cmi
        
        entries.cmt
        
        entries.cmx
        
        entries.ml
        
        environ.cmi
        
        environ.cmt
        
        environ.cmti
        
        environ.cmx
        
        environ.ml
        
        environ.mli
        
        esubst.cmi
        
        esubst.cmt
        
        esubst.cmti
        
        esubst.cmx
        
        esubst.ml
        
        esubst.mli
        
        evar.cmi
        
        evar.cmt
        
        evar.cmti
        
        evar.cmx
        
        evar.ml
        
        evar.mli
        
        float64.cmi
        
        float64.cmt
        
        float64.cmti
        
        float64.cmx
        
        float64.ml
        
        float64.mli
        
        float64_common.cmi
        
        float64_common.cmt
        
        float64_common.cmti
        
        float64_common.cmx
        
        float64_common.ml
        
        float64_common.mli
        
        indTyping.cmi
        
        indTyping.cmt
        
        indTyping.cmti
        
        indTyping.cmx
        
        indTyping.ml
        
        indTyping.mli
        
        indtypes.cmi
        
        indtypes.cmt
        
        indtypes.cmti
        
        indtypes.cmx
        
        indtypes.ml
        
        indtypes.mli
        
        inductive.cmi
        
        inductive.cmt
        
        inductive.cmti
        
        inductive.cmx
        
        inductive.ml
        
        inductive.mli
        
        inferCumulativity.cmi
        
        inferCumulativity.cmt
        
        inferCumulativity.cmti
        
        inferCumulativity.cmx
        
        inferCumulativity.ml
        
        inferCumulativity.mli
        
        kernel.a
        
        kernel.cma
        
        kernel.cmxa
        
        kernel.cmxs
        
        mod_subst.cmi
        
        mod_subst.cmt
        
        mod_subst.cmti
        
        mod_subst.cmx
        
        mod_subst.ml
        
        mod_subst.mli
        
        mod_typing.cmi
        
        mod_typing.cmt
        
        mod_typing.cmti
        
        mod_typing.cmx
        
        mod_typing.ml
        
        mod_typing.mli
        
        modops.cmi
        
        modops.cmt
        
        modops.cmti
        
        modops.cmx
        
        modops.ml
        
        modops.mli
        
        names.cmi
        
        names.cmt
        
        names.cmti
        
        names.cmx
        
        names.ml
        
        names.mli
        
        nativecode.cmi
        
        nativecode.cmt
        
        nativecode.cmti
        
        nativecode.cmx
        
        nativecode.ml
        
        nativecode.mli
        
        nativeconv.cmi
        
        nativeconv.cmt
        
        nativeconv.cmti
        
        nativeconv.cmx
        
        nativeconv.ml
        
        nativeconv.mli
        
        nativelambda.cmi
        
        nativelambda.cmt
        
        nativelambda.cmti
        
        nativelambda.cmx
        
        nativelambda.ml
        
        nativelambda.mli
        
        nativelib.cmi
        
        nativelib.cmt
        
        nativelib.cmti
        
        nativelib.cmx
        
        nativelib.ml
        
        nativelib.mli
        
        nativelibrary.cmi
        
        nativelibrary.cmt
        
        nativelibrary.cmti
        
        nativelibrary.cmx
        
        nativelibrary.ml
        
        nativelibrary.mli
        
        nativevalues.cmi
        
        nativevalues.cmt
        
        nativevalues.cmti
        
        nativevalues.cmx
        
        nativevalues.ml
        
        nativevalues.mli
        
        opaqueproof.cmi
        
        opaqueproof.cmt
        
        opaqueproof.cmti
        
        opaqueproof.cmx
        
        opaqueproof.ml
        
        opaqueproof.mli
        
        parray.cmi
        
        parray.cmt
        
        parray.cmti
        
        parray.cmx
        
        parray.ml
        
        parray.mli
        
        primred.cmi
        
        primred.cmt
        
        primred.cmti
        
        primred.cmx
        
        primred.ml
        
        primred.mli
        
        reduction.cmi
        
        reduction.cmt
        
        reduction.cmti
        
        reduction.cmx
        
        reduction.ml
        
        reduction.mli
        
        relevanceops.cmi
        
        relevanceops.cmt
        
        relevanceops.cmti
        
        relevanceops.cmx
        
        relevanceops.ml
        
        relevanceops.mli
        
        retroknowledge.cmi
        
        retroknowledge.cmt
        
        retroknowledge.cmti
        
        retroknowledge.cmx
        
        retroknowledge.ml
        
        retroknowledge.mli
        
        safe_typing.cmi
        
        safe_typing.cmt
        
        safe_typing.cmti
        
        safe_typing.cmx
        
        safe_typing.ml
        
        safe_typing.mli
        
        section.cmi
        
        section.cmt
        
        section.cmti
        
        section.cmx
        
        section.ml
        
        section.mli
        
        sorts.cmi
        
        sorts.cmt
        
        sorts.cmti
        
        sorts.cmx
        
        sorts.ml
        
        sorts.mli
        
        subtyping.cmi
        
        subtyping.cmt
        
        subtyping.cmti
        
        subtyping.cmx
        
        subtyping.ml
        
        subtyping.mli
        
        term.cmi
        
        term.cmt
        
        term.cmti
        
        term.cmx
        
        term.ml
        
        term.mli
        
        term_typing.cmi
        
        term_typing.cmt
        
        term_typing.cmti
        
        term_typing.cmx
        
        term_typing.ml
        
        term_typing.mli
        
        transparentState.cmi
        
        transparentState.cmt
        
        transparentState.cmti
        
        transparentState.cmx
        
        transparentState.ml
        
        transparentState.mli
        
        type_errors.cmi
        
        type_errors.cmt
        
        type_errors.cmti
        
        type_errors.cmx
        
        type_errors.ml
        
        type_errors.mli
        
        typeops.cmi
        
        typeops.cmt
        
        typeops.cmti
        
        typeops.cmx
        
        typeops.ml
        
        typeops.mli
        
        uGraph.cmi
        
        uGraph.cmt
        
        uGraph.cmti
        
        uGraph.cmx
        
        uGraph.ml
        
        uGraph.mli
        
        uint63.cmi
        
        uint63.cmt
        
        uint63.cmti
        
        uint63.cmx
        
        uint63.ml
        
        uint63.mli
        
        univ.cmi
        
        univ.cmt
        
        univ.cmti
        
        univ.cmx
        
        univ.ml
        
        univ.mli
        
        vars.cmi
        
        vars.cmt
        
        vars.cmti
        
        vars.cmx
        
        vars.ml
        
        vars.mli
        
        vconv.cmi
        
        vconv.cmt
        
        vconv.cmti
        
        vconv.cmx
        
        vconv.ml
        
        vconv.mli
        
        vm.cmi
        
        vm.cmt
        
        vm.cmti
        
        vm.cmx
        
        vm.ml
        
        vm.mli
        
        vmbytecodes.cmi
        
        vmbytecodes.cmt
        
        vmbytecodes.cmti
        
        vmbytecodes.cmx
        
        vmbytecodes.ml
        
        vmbytecodes.mli
        
        vmbytegen.cmi
        
        vmbytegen.cmt
        
        vmbytegen.cmti
        
        vmbytegen.cmx
        
        vmbytegen.ml
        
        vmbytegen.mli
        
        vmemitcodes.cmi
        
        vmemitcodes.cmt
        
        vmemitcodes.cmti
        
        vmemitcodes.cmx
        
        vmemitcodes.ml
        
        vmemitcodes.mli
        
        vmlambda.cmi
        
        vmlambda.cmt
        
        vmlambda.cmti
        
        vmlambda.cmx
        
        vmlambda.ml
        
        vmlambda.mli
        
        vmopcodes.cmi
        
        vmopcodes.cmt
        
        vmopcodes.cmx
        
        vmopcodes.ml
        
        vmsymtable.cmi
        
        vmsymtable.cmt
        
        vmsymtable.cmti
        
        vmsymtable.cmx
        
        vmsymtable.ml
        
        vmsymtable.mli
        
        vmvalues.cmi
        
        vmvalues.cmt
        
        vmvalues.cmti
        
        vmvalues.cmx
        
        vmvalues.ml
        
        vmvalues.mli
      - lib/
        
        acyclicGraph.cmi
        
        acyclicGraph.cmt
        
        acyclicGraph.cmti
        
        acyclicGraph.cmx
        
        acyclicGraph.ml
        
        acyclicGraph.mli
        
        aux_file.cmi
        
        aux_file.cmt
        
        aux_file.cmti
        
        aux_file.cmx
        
        aux_file.ml
        
        aux_file.mli
        
        cAst.cmi
        
        cAst.cmt
        
        cAst.cmti
        
        cAst.cmx
        
        cAst.ml
        
        cAst.mli
        
        cDebug.cmi
        
        cDebug.cmt
        
        cDebug.cmti
        
        cDebug.cmx
        
        cDebug.ml
        
        cDebug.mli
        
        cErrors.cmi
        
        cErrors.cmt
        
        cErrors.cmti
        
        cErrors.cmx
        
        cErrors.ml
        
        cErrors.mli
        
        cProfile.cmi
        
        cProfile.cmt
        
        cProfile.cmti
        
        cProfile.cmx
        
        cProfile.ml
        
        cProfile.mli
        
        cWarnings.cmi
        
        cWarnings.cmt
        
        cWarnings.cmti
        
        cWarnings.cmx
        
        cWarnings.ml
        
        cWarnings.mli
        
        control.cmi
        
        control.cmt
        
        control.cmti
        
        control.cmx
        
        control.ml
        
        control.mli
        
        coqProject_file.cmi
        
        coqProject_file.cmt
        
        coqProject_file.cmti
        
        coqProject_file.cmx
        
        coqProject_file.ml
        
        coqProject_file.mli
        
        dAst.cmi
        
        dAst.cmt
        
        dAst.cmti
        
        dAst.cmx
        
        dAst.ml
        
        dAst.mli
        
        envars.cmi
        
        envars.cmt
        
        envars.cmti
        
        envars.cmx
        
        envars.ml
        
        envars.mli
        
        explore.cmi
        
        explore.cmt
        
        explore.cmti
        
        explore.cmx
        
        explore.ml
        
        explore.mli
        
        feedback.cmi
        
        feedback.cmt
        
        feedback.cmti
        
        feedback.cmx
        
        feedback.ml
        
        feedback.mli
        
        flags.cmi
        
        flags.cmt
        
        flags.cmti
        
        flags.cmx
        
        flags.ml
        
        flags.mli
        
        future.cmi
        
        future.cmt
        
        future.cmti
        
        future.cmx
        
        future.ml
        
        future.mli
        
        genarg.cmi
        
        genarg.cmt
        
        genarg.cmti
        
        genarg.cmx
        
        genarg.ml
        
        genarg.mli
        
        hook.cmi
        
        hook.cmt
        
        hook.cmti
        
        hook.cmx
        
        hook.ml
        
        hook.mli
        
        lStream.cmi
        
        lStream.cmt
        
        lStream.cmti
        
        lStream.cmx
        
        lStream.ml
        
        lStream.mli
        
        lib.a
        
        lib.cma
        
        lib.cmxa
        
        lib.cmxs
        
        loc.cmi
        
        loc.cmt
        
        loc.cmti
        
        loc.cmx
        
        loc.ml
        
        loc.mli
        
        objFile.cmi
        
        objFile.cmt
        
        objFile.cmti
        
        objFile.cmx
        
        objFile.ml
        
        objFile.mli
        
        pp.cmi
        
        pp.cmt
        
        pp.cmti
        
        pp.cmx
        
        pp.ml
        
        pp.mli
        
        pp_diff.cmi
        
        pp_diff.cmt
        
        pp_diff.cmti
        
        pp_diff.cmx
        
        pp_diff.ml
        
        pp_diff.mli
        
        rtree.cmi
        
        rtree.cmt
        
        rtree.cmti
        
        rtree.cmx
        
        rtree.ml
        
        rtree.mli
        
        spawn.cmi
        
        spawn.cmt
        
        spawn.cmti
        
        spawn.cmx
        
        spawn.ml
        
        spawn.mli
        
        stateid.cmi
        
        stateid.cmt
        
        stateid.cmti
        
        stateid.cmx
        
        stateid.ml
        
        stateid.mli
        
        system.cmi
        
        system.cmt
        
        system.cmti
        
        system.cmx
        
        system.ml
        
        system.mli
        
        util.cmi
        
        util.cmt
        
        util.cmti
        
        util.cmx
        
        util.ml
        
        util.mli
        
        xml_datatype.cmi
        
        xml_datatype.cmti
        
        xml_datatype.mli
      - library/
        
        coqlib.cmi
        
        coqlib.cmt
        
        coqlib.cmti
        
        coqlib.cmx
        
        coqlib.ml
        
        coqlib.mli
        
        global.cmi
        
        global.cmt
        
        global.cmti
        
        global.cmx
        
        global.ml
        
        global.mli
        
        globnames.cmi
        
        globnames.cmt
        
        globnames.cmti
        
        globnames.cmx
        
        globnames.ml
        
        globnames.mli
        
        goptions.cmi
        
        goptions.cmt
        
        goptions.cmti
        
        goptions.cmx
        
        goptions.ml
        
        goptions.mli
        
        lib.cmi
        
        lib.cmt
        
        lib.cmti
        
        lib.cmx
        
        lib.ml
        
        lib.mli
        
        libnames.cmi
        
        libnames.cmt
        
        libnames.cmti
        
        libnames.cmx
        
        libnames.ml
        
        libnames.mli
        
        libobject.cmi
        
        libobject.cmt
        
        libobject.cmti
        
        libobject.cmx
        
        libobject.ml
        
        libobject.mli
        
        library.a
        
        library.cma
        
        library.cmxa
        
        library.cmxs
        
        nametab.cmi
        
        nametab.cmt
        
        nametab.cmti
        
        nametab.cmx
        
        nametab.ml
        
        nametab.mli
        
        summary.cmi
        
        summary.cmt
        
        summary.cmti
        
        summary.cmx
        
        summary.ml
        
        summary.mli
      - opam
      - parsing/
        
        cLexer.cmi
        
        cLexer.cmt
        
        cLexer.cmti
        
        cLexer.cmx
        
        cLexer.ml
        
        cLexer.mli
        
        extend.cmi
        
        extend.cmt
        
        extend.cmti
        
        extend.cmx
        
        extend.ml
        
        extend.mli
        
        g_constr.cmi
        
        g_constr.cmt
        
        g_constr.cmx
        
        g_constr.ml
        
        g_prim.cmi
        
        g_prim.cmt
        
        g_prim.cmx
        
        g_prim.ml
        
        notation_gram.cmi
        
        notation_gram.cmt
        
        notation_gram.cmx
        
        notation_gram.ml
        
        notgram_ops.cmi
        
        notgram_ops.cmt
        
        notgram_ops.cmti
        
        notgram_ops.cmx
        
        notgram_ops.ml
        
        notgram_ops.mli
        
        parsing.a
        
        parsing.cma
        
        parsing.cmxa
        
        parsing.cmxs
        
        pcoq.cmi
        
        pcoq.cmt
        
        pcoq.cmti
        
        pcoq.cmx
        
        pcoq.ml
        
        pcoq.mli
        
        ppextend.cmi
        
        ppextend.cmt
        
        ppextend.cmti
        
        ppextend.cmx
        
        ppextend.ml
        
        ppextend.mli
        
        tok.cmi
        
        tok.cmt
        
        tok.cmti
        
        tok.cmx
        
        tok.ml
        
        tok.mli
      - plugins/
        
        btauto/
        
        btauto_plugin.a
        
        btauto_plugin.cma
        
        btauto_plugin.cmi
        
        btauto_plugin.cmt
        
        btauto_plugin.cmx
        
        btauto_plugin.cmxa
        
        btauto_plugin.cmxs
        
        btauto_plugin.ml
        
        btauto_plugin__G_btauto.cmi
        
        btauto_plugin__G_btauto.cmt
        
        btauto_plugin__G_btauto.cmx
        
        btauto_plugin__Refl_btauto.cmi
        
        btauto_plugin__Refl_btauto.cmt
        
        btauto_plugin__Refl_btauto.cmti
        
        btauto_plugin__Refl_btauto.cmx
        
        g_btauto.ml
        
        refl_btauto.ml
        
        refl_btauto.mli
        
        cc/
        
        cc_plugin.a
        
        cc_plugin.cma
        
        cc_plugin.cmi
        
        cc_plugin.cmt
        
        cc_plugin.cmx
        
        cc_plugin.cmxa
        
        cc_plugin.cmxs
        
        cc_plugin.ml
        
        cc_plugin__Ccalgo.cmi
        
        cc_plugin__Ccalgo.cmt
        
        cc_plugin__Ccalgo.cmti
        
        cc_plugin__Ccalgo.cmx
        
        cc_plugin__Ccproof.cmi
        
        cc_plugin__Ccproof.cmt
        
        cc_plugin__Ccproof.cmti
        
        cc_plugin__Ccproof.cmx
        
        cc_plugin__Cctac.cmi
        
        cc_plugin__Cctac.cmt
        
        cc_plugin__Cctac.cmti
        
        cc_plugin__Cctac.cmx
        
        cc_plugin__G_congruence.cmi
        
        cc_plugin__G_congruence.cmt
        
        cc_plugin__G_congruence.cmx
        
        ccalgo.ml
        
        ccalgo.mli
        
        ccproof.ml
        
        ccproof.mli
        
        cctac.ml
        
        cctac.mli
        
        g_congruence.ml
        
        derive/
        
        derive.ml
        
        derive.mli
        
        derive_plugin.a
        
        derive_plugin.cma
        
        derive_plugin.cmi
        
        derive_plugin.cmt
        
        derive_plugin.cmx
        
        derive_plugin.cmxa
        
        derive_plugin.cmxs
        
        derive_plugin.ml
        
        derive_plugin__Derive.cmi
        
        derive_plugin__Derive.cmt
        
        derive_plugin__Derive.cmti
        
        derive_plugin__Derive.cmx
        
        derive_plugin__G_derive.cmi
        
        derive_plugin__G_derive.cmt
        
        derive_plugin__G_derive.cmx
        
        g_derive.ml
        
        extraction/
        
        big.ml
        
        common.ml
        
        common.mli
        
        extract_env.ml
        
        extract_env.mli
        
        extraction.ml
        
        extraction.mli
        
        extraction_plugin.a
        
        extraction_plugin.cma
        
        extraction_plugin.cmi
        
        extraction_plugin.cmt
        
        extraction_plugin.cmx
        
        extraction_plugin.cmxa
        
        extraction_plugin.cmxs
        
        extraction_plugin.ml
        
        extraction_plugin__Big.cmi
        
        extraction_plugin__Big.cmt
        
        extraction_plugin__Big.cmx
        
        extraction_plugin__Common.cmi
        
        extraction_plugin__Common.cmt
        
        extraction_plugin__Common.cmti
        
        extraction_plugin__Common.cmx
        
        extraction_plugin__Extract_env.cmi
        
        extraction_plugin__Extract_env.cmt
        
        extraction_plugin__Extract_env.cmti
        
        extraction_plugin__Extract_env.cmx
        
        extraction_plugin__Extraction.cmi
        
        extraction_plugin__Extraction.cmt
        
        extraction_plugin__Extraction.cmti
        
        extraction_plugin__Extraction.cmx
        
        extraction_plugin__G_extraction.cmi
        
        extraction_plugin__G_extraction.cmt
        
        extraction_plugin__G_extraction.cmx
        
        extraction_plugin__Haskell.cmi
        
        extraction_plugin__Haskell.cmt
        
        extraction_plugin__Haskell.cmti
        
        extraction_plugin__Haskell.cmx
        
        extraction_plugin__Json.cmi
        
        extraction_plugin__Json.cmt
        
        extraction_plugin__Json.cmti
        
        extraction_plugin__Json.cmx
        
        extraction_plugin__Miniml.cmi
        
        extraction_plugin__Miniml.cmt
        
        extraction_plugin__Miniml.cmti
        
        extraction_plugin__Miniml.cmx
        
        extraction_plugin__Mlutil.cmi
        
        extraction_plugin__Mlutil.cmt
        
        extraction_plugin__Mlutil.cmti
        
        extraction_plugin__Mlutil.cmx
        
        extraction_plugin__Modutil.cmi
        
        extraction_plugin__Modutil.cmt
        
        extraction_plugin__Modutil.cmti
        
        extraction_plugin__Modutil.cmx
        
        extraction_plugin__Ocaml.cmi
        
        extraction_plugin__Ocaml.cmt
        
        extraction_plugin__Ocaml.cmti
        
        extraction_plugin__Ocaml.cmx
        
        extraction_plugin__Scheme.cmi
        
        extraction_plugin__Scheme.cmt
        
        extraction_plugin__Scheme.cmti
        
        extraction_plugin__Scheme.cmx
        
        extraction_plugin__Table.cmi
        
        extraction_plugin__Table.cmt
        
        extraction_plugin__Table.cmti
        
        extraction_plugin__Table.cmx
        
        g_extraction.ml
        
        haskell.ml
        
        haskell.mli
        
        json.ml
        
        json.mli
        
        miniml.ml
        
        miniml.mli
        
        mlutil.ml
        
        mlutil.mli
        
        modutil.ml
        
        modutil.mli
        
        ocaml.ml
        
        ocaml.mli
        
        scheme.ml
        
        scheme.mli
        
        table.ml
        
        table.mli
        
        firstorder/
        
        firstorder_plugin.a
        
        firstorder_plugin.cma
        
        firstorder_plugin.cmi
        
        firstorder_plugin.cmt
        
        firstorder_plugin.cmx
        
        firstorder_plugin.cmxa
        
        firstorder_plugin.cmxs
        
        firstorder_plugin.ml
        
        firstorder_plugin__Formula.cmi
        
        firstorder_plugin__Formula.cmt
        
        firstorder_plugin__Formula.cmti
        
        firstorder_plugin__Formula.cmx
        
        firstorder_plugin__G_ground.cmi
        
        firstorder_plugin__G_ground.cmt
        
        firstorder_plugin__G_ground.cmx
        
        firstorder_plugin__Ground.cmi
        
        firstorder_plugin__Ground.cmt
        
        firstorder_plugin__Ground.cmti
        
        firstorder_plugin__Ground.cmx
        
        firstorder_plugin__Instances.cmi
        
        firstorder_plugin__Instances.cmt
        
        firstorder_plugin__Instances.cmti
        
        firstorder_plugin__Instances.cmx
        
        firstorder_plugin__Rules.cmi
        
        firstorder_plugin__Rules.cmt
        
        firstorder_plugin__Rules.cmti
        
        firstorder_plugin__Rules.cmx
        
        firstorder_plugin__Sequent.cmi
        
        firstorder_plugin__Sequent.cmt
        
        firstorder_plugin__Sequent.cmti
        
        firstorder_plugin__Sequent.cmx
        
        firstorder_plugin__Unify.cmi
        
        firstorder_plugin__Unify.cmt
        
        firstorder_plugin__Unify.cmti
        
        firstorder_plugin__Unify.cmx
        
        formula.ml
        
        formula.mli
        
        g_ground.ml
        
        ground.ml
        
        ground.mli
        
        instances.ml
        
        instances.mli
        
        rules.ml
        
        rules.mli
        
        sequent.ml
        
        sequent.mli
        
        unify.ml
        
        unify.mli
        
        float_syntax/
        
        float_syntax.ml
        
        float_syntax_plugin.a
        
        float_syntax_plugin.cma
        
        float_syntax_plugin.cmi
        
        float_syntax_plugin.cmt
        
        float_syntax_plugin.cmx
        
        float_syntax_plugin.cmxa
        
        float_syntax_plugin.cmxs
        
        float_syntax_plugin.ml
        
        float_syntax_plugin__Float_syntax.cmi
        
        float_syntax_plugin__Float_syntax.cmt
        
        float_syntax_plugin__Float_syntax.cmx
        
        funind/
        
        functional_principles_proofs.ml
        
        functional_principles_proofs.mli
        
        functional_principles_types.ml
        
        functional_principles_types.mli
        
        funind_plugin.a
        
        funind_plugin.cma
        
        funind_plugin.cmi
        
        funind_plugin.cmt
        
        funind_plugin.cmx
        
        funind_plugin.cmxa
        
        funind_plugin.cmxs
        
        funind_plugin.ml
        
        funind_plugin__Functional_principles_proofs.cmi
        
        funind_plugin__Functional_principles_proofs.cmt
        
        funind_plugin__Functional_principles_proofs.cmti
        
        funind_plugin__Functional_principles_proofs.cmx
        
        funind_plugin__Functional_principles_types.cmi
        
        funind_plugin__Functional_principles_types.cmt
        
        funind_plugin__Functional_principles_types.cmti
        
        funind_plugin__Functional_principles_types.cmx
        
        funind_plugin__G_indfun.cmi
        
        funind_plugin__G_indfun.cmt
        
        funind_plugin__G_indfun.cmx
        
        funind_plugin__Gen_principle.cmi
        
        funind_plugin__Gen_principle.cmt
        
        funind_plugin__Gen_principle.cmti
        
        funind_plugin__Gen_principle.cmx
        
        funind_plugin__Glob_term_to_relation.cmi
        
        funind_plugin__Glob_term_to_relation.cmt
        
        funind_plugin__Glob_term_to_relation.cmti
        
        funind_plugin__Glob_term_to_relation.cmx
        
        funind_plugin__Glob_termops.cmi
        
        funind_plugin__Glob_termops.cmt
        
        funind_plugin__Glob_termops.cmti
        
        funind_plugin__Glob_termops.cmx
        
        funind_plugin__Indfun.cmi
        
        funind_plugin__Indfun.cmt
        
        funind_plugin__Indfun.cmti
        
        funind_plugin__Indfun.cmx
        
        funind_plugin__Indfun_common.cmi
        
        funind_plugin__Indfun_common.cmt
        
        funind_plugin__Indfun_common.cmti
        
        funind_plugin__Indfun_common.cmx
        
        funind_plugin__Invfun.cmi
        
        funind_plugin__Invfun.cmt
        
        funind_plugin__Invfun.cmti
        
        funind_plugin__Invfun.cmx
        
        funind_plugin__Recdef.cmi
        
        funind_plugin__Recdef.cmt
        
        funind_plugin__Recdef.cmti
        
        funind_plugin__Recdef.cmx
        
        g_indfun.ml
        
        gen_principle.ml
        
        gen_principle.mli
        
        glob_term_to_relation.ml
        
        glob_term_to_relation.mli
        
        glob_termops.ml
        
        glob_termops.mli
        
        indfun.ml
        
        indfun.mli
        
        indfun_common.ml
        
        indfun_common.mli
        
        invfun.ml
        
        invfun.mli
        
        recdef.ml
        
        recdef.mli
        
        ltac/
        
        coretactics.ml
        
        evar_tactics.ml
        
        evar_tactics.mli
        
        extraargs.ml
        
        extraargs.mli
        
        extratactics.ml
        
        extratactics.mli
        
        g_auto.ml
        
        g_class.ml
        
        g_eqdecide.ml
        
        g_ltac.ml
        
        g_obligations.ml
        
        g_rewrite.ml
        
        g_tactic.ml
        
        leminv.ml
        
        leminv.mli
        
        ltac_plugin.a
        
        ltac_plugin.cma
        
        ltac_plugin.cmi
        
        ltac_plugin.cmt
        
        ltac_plugin.cmx
        
        ltac_plugin.cmxa
        
        ltac_plugin.cmxs
        
        ltac_plugin.ml
        
        ltac_plugin__Coretactics.cmi
        
        ltac_plugin__Coretactics.cmt
        
        ltac_plugin__Coretactics.cmx
        
        ltac_plugin__Evar_tactics.cmi
        
        ltac_plugin__Evar_tactics.cmt
        
        ltac_plugin__Evar_tactics.cmti
        
        ltac_plugin__Evar_tactics.cmx
        
        ltac_plugin__Extraargs.cmi
        
        ltac_plugin__Extraargs.cmt
        
        ltac_plugin__Extraargs.cmti
        
        ltac_plugin__Extraargs.cmx
        
        ltac_plugin__Extratactics.cmi
        
        ltac_plugin__Extratactics.cmt
        
        ltac_plugin__Extratactics.cmti
        
        ltac_plugin__Extratactics.cmx
        
        ltac_plugin__G_auto.cmi
        
        ltac_plugin__G_auto.cmt
        
        ltac_plugin__G_auto.cmx
        
        ltac_plugin__G_class.cmi
        
        ltac_plugin__G_class.cmt
        
        ltac_plugin__G_class.cmx
        
        ltac_plugin__G_eqdecide.cmi
        
        ltac_plugin__G_eqdecide.cmt
        
        ltac_plugin__G_eqdecide.cmx
        
        ltac_plugin__G_ltac.cmi
        
        ltac_plugin__G_ltac.cmt
        
        ltac_plugin__G_ltac.cmx
        
        ltac_plugin__G_obligations.cmi
        
        ltac_plugin__G_obligations.cmt
        
        ltac_plugin__G_obligations.cmx
        
        ltac_plugin__G_rewrite.cmi
        
        ltac_plugin__G_rewrite.cmt
        
        ltac_plugin__G_rewrite.cmx
        
        ltac_plugin__G_tactic.cmi
        
        ltac_plugin__G_tactic.cmt
        
        ltac_plugin__G_tactic.cmx
        
        ltac_plugin__Leminv.cmi
        
        ltac_plugin__Leminv.cmt
        
        ltac_plugin__Leminv.cmti
        
        ltac_plugin__Leminv.cmx
        
        ltac_plugin__Pltac.cmi
        
        ltac_plugin__Pltac.cmt
        
        ltac_plugin__Pltac.cmti
        
        ltac_plugin__Pltac.cmx
        
        ltac_plugin__Pptactic.cmi
        
        ltac_plugin__Pptactic.cmt
        
        ltac_plugin__Pptactic.cmti
        
        ltac_plugin__Pptactic.cmx
        
        ltac_plugin__Profile_ltac.cmi
        
        ltac_plugin__Profile_ltac.cmt
        
        ltac_plugin__Profile_ltac.cmti
        
        ltac_plugin__Profile_ltac.cmx
        
        ltac_plugin__Profile_ltac_tactics.cmi
        
        ltac_plugin__Profile_ltac_tactics.cmt
        
        ltac_plugin__Profile_ltac_tactics.cmx
        
        ltac_plugin__Rewrite.cmi
        
        ltac_plugin__Rewrite.cmt
        
        ltac_plugin__Rewrite.cmti
        
        ltac_plugin__Rewrite.cmx
        
        ltac_plugin__Tacarg.cmi
        
        ltac_plugin__Tacarg.cmt
        
        ltac_plugin__Tacarg.cmti
        
        ltac_plugin__Tacarg.cmx
        
        ltac_plugin__Taccoerce.cmi
        
        ltac_plugin__Taccoerce.cmt
        
        ltac_plugin__Taccoerce.cmti
        
        ltac_plugin__Taccoerce.cmx
        
        ltac_plugin__Tacentries.cmi
        
        ltac_plugin__Tacentries.cmt
        
        ltac_plugin__Tacentries.cmti
        
        ltac_plugin__Tacentries.cmx
        
        ltac_plugin__Tacenv.cmi
        
        ltac_plugin__Tacenv.cmt
        
        ltac_plugin__Tacenv.cmti
        
        ltac_plugin__Tacenv.cmx
        
        ltac_plugin__Tacexpr.cmi
        
        ltac_plugin__Tacexpr.cmt
        
        ltac_plugin__Tacexpr.cmti
        
        ltac_plugin__Tacexpr.cmx
        
        ltac_plugin__Tacintern.cmi
        
        ltac_plugin__Tacintern.cmt
        
        ltac_plugin__Tacintern.cmti
        
        ltac_plugin__Tacintern.cmx
        
        ltac_plugin__Tacinterp.cmi
        
        ltac_plugin__Tacinterp.cmt
        
        ltac_plugin__Tacinterp.cmti
        
        ltac_plugin__Tacinterp.cmx
        
        ltac_plugin__Tacsubst.cmi
        
        ltac_plugin__Tacsubst.cmt
        
        ltac_plugin__Tacsubst.cmti
        
        ltac_plugin__Tacsubst.cmx
        
        ltac_plugin__Tactic_debug.cmi
        
        ltac_plugin__Tactic_debug.cmt
        
        ltac_plugin__Tactic_debug.cmti
        
        ltac_plugin__Tactic_debug.cmx
        
        ltac_plugin__Tactic_matching.cmi
        
        ltac_plugin__Tactic_matching.cmt
        
        ltac_plugin__Tactic_matching.cmti
        
        ltac_plugin__Tactic_matching.cmx
        
        ltac_plugin__Tactic_option.cmi
        
        ltac_plugin__Tactic_option.cmt
        
        ltac_plugin__Tactic_option.cmti
        
        ltac_plugin__Tactic_option.cmx
        
        pltac.ml
        
        pltac.mli
        
        pptactic.ml
        
        pptactic.mli
        
        profile_ltac.ml
        
        profile_ltac.mli
        
        profile_ltac_tactics.ml
        
        rewrite.ml
        
        rewrite.mli
        
        tacarg.ml
        
        tacarg.mli
        
        taccoerce.ml
        
        taccoerce.mli
        
        tacentries.ml
        
        tacentries.mli
        
        tacenv.ml
        
        tacenv.mli
        
        tacexpr.ml
        
        tacexpr.mli
        
        tacintern.ml
        
        tacintern.mli
        
        tacinterp.ml
        
        tacinterp.mli
        
        tacsubst.ml
        
        tacsubst.mli
        
        tactic_debug.ml
        
        tactic_debug.mli
        
        tactic_matching.ml
        
        tactic_matching.mli
        
        tactic_option.ml
        
        tactic_option.mli
        
        ltac2/
        
        g_ltac2.ml
        
        ltac2_plugin.a
        
        ltac2_plugin.cma
        
        ltac2_plugin.cmi
        
        ltac2_plugin.cmt
        
        ltac2_plugin.cmx
        
        ltac2_plugin.cmxa
        
        ltac2_plugin.cmxs
        
        ltac2_plugin.ml
        
        ltac2_plugin__G_ltac2.cmi
        
        ltac2_plugin__G_ltac2.cmt
        
        ltac2_plugin__G_ltac2.cmx
        
        ltac2_plugin__Tac2core.cmi
        
        ltac2_plugin__Tac2core.cmt
        
        ltac2_plugin__Tac2core.cmti
        
        ltac2_plugin__Tac2core.cmx
        
        ltac2_plugin__Tac2dyn.cmi
        
        ltac2_plugin__Tac2dyn.cmt
        
        ltac2_plugin__Tac2dyn.cmti
        
        ltac2_plugin__Tac2dyn.cmx
        
        ltac2_plugin__Tac2entries.cmi
        
        ltac2_plugin__Tac2entries.cmt
        
        ltac2_plugin__Tac2entries.cmti
        
        ltac2_plugin__Tac2entries.cmx
        
        ltac2_plugin__Tac2env.cmi
        
        ltac2_plugin__Tac2env.cmt
        
        ltac2_plugin__Tac2env.cmti
        
        ltac2_plugin__Tac2env.cmx
        
        ltac2_plugin__Tac2expr.cmi
        
        ltac2_plugin__Tac2expr.cmti
        
        ltac2_plugin__Tac2extffi.cmi
        
        ltac2_plugin__Tac2extffi.cmt
        
        ltac2_plugin__Tac2extffi.cmti
        
        ltac2_plugin__Tac2extffi.cmx
        
        ltac2_plugin__Tac2ffi.cmi
        
        ltac2_plugin__Tac2ffi.cmt
        
        ltac2_plugin__Tac2ffi.cmti
        
        ltac2_plugin__Tac2ffi.cmx
        
        ltac2_plugin__Tac2intern.cmi
        
        ltac2_plugin__Tac2intern.cmt
        
        ltac2_plugin__Tac2intern.cmti
        
        ltac2_plugin__Tac2intern.cmx
        
        ltac2_plugin__Tac2interp.cmi
        
        ltac2_plugin__Tac2interp.cmt
        
        ltac2_plugin__Tac2interp.cmti
        
        ltac2_plugin__Tac2interp.cmx
        
        ltac2_plugin__Tac2match.cmi
        
        ltac2_plugin__Tac2match.cmt
        
        ltac2_plugin__Tac2match.cmti
        
        ltac2_plugin__Tac2match.cmx
        
        ltac2_plugin__Tac2print.cmi
        
        ltac2_plugin__Tac2print.cmt
        
        ltac2_plugin__Tac2print.cmti
        
        ltac2_plugin__Tac2print.cmx
        
        ltac2_plugin__Tac2qexpr.cmi
        
        ltac2_plugin__Tac2qexpr.cmti
        
        ltac2_plugin__Tac2quote.cmi
        
        ltac2_plugin__Tac2quote.cmt
        
        ltac2_plugin__Tac2quote.cmti
        
        ltac2_plugin__Tac2quote.cmx
        
        ltac2_plugin__Tac2stdlib.cmi
        
        ltac2_plugin__Tac2stdlib.cmt
        
        ltac2_plugin__Tac2stdlib.cmti
        
        ltac2_plugin__Tac2stdlib.cmx
        
        ltac2_plugin__Tac2tactics.cmi
        
        ltac2_plugin__Tac2tactics.cmt
        
        ltac2_plugin__Tac2tactics.cmti
        
        ltac2_plugin__Tac2tactics.cmx
        
        ltac2_plugin__Tac2types.cmi
        
        ltac2_plugin__Tac2types.cmti
        
        tac2core.ml
        
        tac2core.mli
        
        tac2dyn.ml
        
        tac2dyn.mli
        
        tac2entries.ml
        
        tac2entries.mli
        
        tac2env.ml
        
        tac2env.mli
        
        tac2expr.mli
        
        tac2extffi.ml
        
        tac2extffi.mli
        
        tac2ffi.ml
        
        tac2ffi.mli
        
        tac2intern.ml
        
        tac2intern.mli
        
        tac2interp.ml
        
        tac2interp.mli
        
        tac2match.ml
        
        tac2match.mli
        
        tac2print.ml
        
        tac2print.mli
        
        tac2qexpr.mli
        
        tac2quote.ml
        
        tac2quote.mli
        
        tac2stdlib.ml
        
        tac2stdlib.mli
        
        tac2tactics.ml
        
        tac2tactics.mli
        
        tac2types.mli
        
        micromega/
        
        certificate.ml
        
        certificate.mli
        
        coq_micromega.ml
        
        coq_micromega.mli
        
        g_micromega.ml
        
        g_micromega.mli
        
        itv.ml
        
        itv.mli
        
        mfourier.ml
        
        mfourier.mli
        
        micromega.ml
        
        micromega.mli
        
        micromega_plugin.a
        
        micromega_plugin.cma
        
        micromega_plugin.cmi
        
        micromega_plugin.cmt
        
        micromega_plugin.cmx
        
        micromega_plugin.cmxa
        
        micromega_plugin.cmxs
        
        micromega_plugin.ml
        
        micromega_plugin__Certificate.cmi
        
        micromega_plugin__Certificate.cmt
        
        micromega_plugin__Certificate.cmti
        
        micromega_plugin__Certificate.cmx
        
        micromega_plugin__Coq_micromega.cmi
        
        micromega_plugin__Coq_micromega.cmt
        
        micromega_plugin__Coq_micromega.cmti
        
        micromega_plugin__Coq_micromega.cmx
        
        micromega_plugin__G_micromega.cmi
        
        micromega_plugin__G_micromega.cmt
        
        micromega_plugin__G_micromega.cmti
        
        micromega_plugin__G_micromega.cmx
        
        micromega_plugin__Itv.cmi
        
        micromega_plugin__Itv.cmt
        
        micromega_plugin__Itv.cmti
        
        micromega_plugin__Itv.cmx
        
        micromega_plugin__Mfourier.cmi
        
        micromega_plugin__Mfourier.cmt
        
        micromega_plugin__Mfourier.cmti
        
        micromega_plugin__Mfourier.cmx
        
        micromega_plugin__Micromega.cmi
        
        micromega_plugin__Micromega.cmt
        
        micromega_plugin__Micromega.cmti
        
        micromega_plugin__Micromega.cmx
        
        micromega_plugin__Mutils.cmi
        
        micromega_plugin__Mutils.cmt
        
        micromega_plugin__Mutils.cmti
        
        micromega_plugin__Mutils.cmx
        
        micromega_plugin__NumCompat.cmi
        
        micromega_plugin__NumCompat.cmt
        
        micromega_plugin__NumCompat.cmti
        
        micromega_plugin__NumCompat.cmx
        
        micromega_plugin__Persistent_cache.cmi
        
        micromega_plugin__Persistent_cache.cmt
        
        micromega_plugin__Persistent_cache.cmti
        
        micromega_plugin__Persistent_cache.cmx
        
        micromega_plugin__Polynomial.cmi
        
        micromega_plugin__Polynomial.cmt
        
        micromega_plugin__Polynomial.cmti
        
        micromega_plugin__Polynomial.cmx
        
        micromega_plugin__Simplex.cmi
        
        micromega_plugin__Simplex.cmt
        
        micromega_plugin__Simplex.cmti
        
        micromega_plugin__Simplex.cmx
        
        micromega_plugin__Sos.cmi
        
        micromega_plugin__Sos.cmt
        
        micromega_plugin__Sos.cmti
        
        micromega_plugin__Sos.cmx
        
        micromega_plugin__Sos_lib.cmi
        
        micromega_plugin__Sos_lib.cmt
        
        micromega_plugin__Sos_lib.cmti
        
        micromega_plugin__Sos_lib.cmx
        
        micromega_plugin__Sos_types.cmi
        
        micromega_plugin__Sos_types.cmt
        
        micromega_plugin__Sos_types.cmti
        
        micromega_plugin__Sos_types.cmx
        
        micromega_plugin__Vect.cmi
        
        micromega_plugin__Vect.cmt
        
        micromega_plugin__Vect.cmti
        
        micromega_plugin__Vect.cmx
        
        mutils.ml
        
        mutils.mli
        
        numCompat.ml
        
        numCompat.mli
        
        persistent_cache.ml
        
        persistent_cache.mli
        
        polynomial.ml
        
        polynomial.mli
        
        simplex.ml
        
        simplex.mli
        
        sos.ml
        
        sos.mli
        
        sos_lib.ml
        
        sos_lib.mli
        
        sos_types.ml
        
        sos_types.mli
        
        vect.ml
        
        vect.mli
        
        nsatz/
        
        g_nsatz.ml
        
        ideal.ml
        
        ideal.mli
        
        nsatz.ml
        
        nsatz.mli
        
        nsatz_plugin.a
        
        nsatz_plugin.cma
        
        nsatz_plugin.cmi
        
        nsatz_plugin.cmt
        
        nsatz_plugin.cmx
        
        nsatz_plugin.cmxa
        
        nsatz_plugin.cmxs
        
        nsatz_plugin.ml
        
        nsatz_plugin__G_nsatz.cmi
        
        nsatz_plugin__G_nsatz.cmt
        
        nsatz_plugin__G_nsatz.cmx
        
        nsatz_plugin__Ideal.cmi
        
        nsatz_plugin__Ideal.cmt
        
        nsatz_plugin__Ideal.cmti
        
        nsatz_plugin__Ideal.cmx
        
        nsatz_plugin__Nsatz.cmi
        
        nsatz_plugin__Nsatz.cmt
        
        nsatz_plugin__Nsatz.cmti
        
        nsatz_plugin__Nsatz.cmx
        
        nsatz_plugin__Polynom.cmi
        
        nsatz_plugin__Polynom.cmt
        
        nsatz_plugin__Polynom.cmti
        
        nsatz_plugin__Polynom.cmx
        
        nsatz_plugin__Utile.cmi
        
        nsatz_plugin__Utile.cmt
        
        nsatz_plugin__Utile.cmti
        
        nsatz_plugin__Utile.cmx
        
        polynom.ml
        
        polynom.mli
        
        utile.ml
        
        utile.mli
        
        number_string_notation/
        
        g_number_string.ml
        
        number.ml
        
        number.mli
        
        number_string_notation_plugin.a
        
        number_string_notation_plugin.cma
        
        number_string_notation_plugin.cmi
        
        number_string_notation_plugin.cmt
        
        number_string_notation_plugin.cmx
        
        number_string_notation_plugin.cmxa
        
        number_string_notation_plugin.cmxs
        
        number_string_notation_plugin.ml
        
        number_string_notation_plugin__G_number_string.cmi
        
        number_string_notation_plugin__G_number_string.cmt
        
        number_string_notation_plugin__G_number_string.cmx
        
        number_string_notation_plugin__Number.cmi
        
        number_string_notation_plugin__Number.cmt
        
        number_string_notation_plugin__Number.cmti
        
        number_string_notation_plugin__Number.cmx
        
        number_string_notation_plugin__String_notation.cmi
        
        number_string_notation_plugin__String_notation.cmt
        
        number_string_notation_plugin__String_notation.cmti
        
        number_string_notation_plugin__String_notation.cmx
        
        string_notation.ml
        
        string_notation.mli
        
        ring/
        
        g_ring.ml
        
        ring.ml
        
        ring.mli
        
        ring_ast.ml
        
        ring_ast.mli
        
        ring_plugin.a
        
        ring_plugin.cma
        
        ring_plugin.cmi
        
        ring_plugin.cmt
        
        ring_plugin.cmx
        
        ring_plugin.cmxa
        
        ring_plugin.cmxs
        
        ring_plugin.ml
        
        ring_plugin__G_ring.cmi
        
        ring_plugin__G_ring.cmt
        
        ring_plugin__G_ring.cmx
        
        ring_plugin__Ring.cmi
        
        ring_plugin__Ring.cmt
        
        ring_plugin__Ring.cmti
        
        ring_plugin__Ring.cmx
        
        ring_plugin__Ring_ast.cmi
        
        ring_plugin__Ring_ast.cmt
        
        ring_plugin__Ring_ast.cmti
        
        ring_plugin__Ring_ast.cmx
        
        rtauto/
        
        g_rtauto.ml
        
        proof_search.ml
        
        proof_search.mli
        
        refl_tauto.ml
        
        refl_tauto.mli
        
        rtauto_plugin.a
        
        rtauto_plugin.cma
        
        rtauto_plugin.cmi
        
        rtauto_plugin.cmt
        
        rtauto_plugin.cmx
        
        rtauto_plugin.cmxa
        
        rtauto_plugin.cmxs
        
        rtauto_plugin.ml
        
        rtauto_plugin__G_rtauto.cmi
        
        rtauto_plugin__G_rtauto.cmt
        
        rtauto_plugin__G_rtauto.cmx
        
        rtauto_plugin__Proof_search.cmi
        
        rtauto_plugin__Proof_search.cmt
        
        rtauto_plugin__Proof_search.cmti
        
        rtauto_plugin__Proof_search.cmx
        
        rtauto_plugin__Refl_tauto.cmi
        
        rtauto_plugin__Refl_tauto.cmt
        
        rtauto_plugin__Refl_tauto.cmti
        
        rtauto_plugin__Refl_tauto.cmx
        
        ssreflect/
        
        ssrast.mli
        
        ssrbwd.ml
        
        ssrbwd.mli
        
        ssrcommon.ml
        
        ssrcommon.mli
        
        ssreflect_plugin.a
        
        ssreflect_plugin.cma
        
        ssreflect_plugin.cmi
        
        ssreflect_plugin.cmt
        
        ssreflect_plugin.cmx
        
        ssreflect_plugin.cmxa
        
        ssreflect_plugin.cmxs
        
        ssreflect_plugin.ml
        
        ssreflect_plugin__Ssrast.cmi
        
        ssreflect_plugin__Ssrast.cmti
        
        ssreflect_plugin__Ssrbwd.cmi
        
        ssreflect_plugin__Ssrbwd.cmt
        
        ssreflect_plugin__Ssrbwd.cmti
        
        ssreflect_plugin__Ssrbwd.cmx
        
        ssreflect_plugin__Ssrcommon.cmi
        
        ssreflect_plugin__Ssrcommon.cmt
        
        ssreflect_plugin__Ssrcommon.cmti
        
        ssreflect_plugin__Ssrcommon.cmx
        
        ssreflect_plugin__Ssrelim.cmi
        
        ssreflect_plugin__Ssrelim.cmt
        
        ssreflect_plugin__Ssrelim.cmti
        
        ssreflect_plugin__Ssrelim.cmx
        
        ssreflect_plugin__Ssrequality.cmi
        
        ssreflect_plugin__Ssrequality.cmt
        
        ssreflect_plugin__Ssrequality.cmti
        
        ssreflect_plugin__Ssrequality.cmx
        
        ssreflect_plugin__Ssrfwd.cmi
        
        ssreflect_plugin__Ssrfwd.cmt
        
        ssreflect_plugin__Ssrfwd.cmti
        
        ssreflect_plugin__Ssrfwd.cmx
        
        ssreflect_plugin__Ssripats.cmi
        
        ssreflect_plugin__Ssripats.cmt
        
        ssreflect_plugin__Ssripats.cmti
        
        ssreflect_plugin__Ssripats.cmx
        
        ssreflect_plugin__Ssrparser.cmi
        
        ssreflect_plugin__Ssrparser.cmt
        
        ssreflect_plugin__Ssrparser.cmti
        
        ssreflect_plugin__Ssrparser.cmx
        
        ssreflect_plugin__Ssrprinters.cmi
        
        ssreflect_plugin__Ssrprinters.cmt
        
        ssreflect_plugin__Ssrprinters.cmti
        
        ssreflect_plugin__Ssrprinters.cmx
        
        ssreflect_plugin__Ssrtacticals.cmi
        
        ssreflect_plugin__Ssrtacticals.cmt
        
        ssreflect_plugin__Ssrtacticals.cmti
        
        ssreflect_plugin__Ssrtacticals.cmx
        
        ssreflect_plugin__Ssrvernac.cmi
        
        ssreflect_plugin__Ssrvernac.cmt
        
        ssreflect_plugin__Ssrvernac.cmti
        
        ssreflect_plugin__Ssrvernac.cmx
        
        ssreflect_plugin__Ssrview.cmi
        
        ssreflect_plugin__Ssrview.cmt
        
        ssreflect_plugin__Ssrview.cmti
        
        ssreflect_plugin__Ssrview.cmx
        
        ssrelim.ml
        
        ssrelim.mli
        
        ssrequality.ml
        
        ssrequality.mli
        
        ssrfwd.ml
        
        ssrfwd.mli
        
        ssripats.ml
        
        ssripats.mli
        
        ssrparser.ml
        
        ssrparser.mli
        
        ssrprinters.ml
        
        ssrprinters.mli
        
        ssrtacticals.ml
        
        ssrtacticals.mli
        
        ssrvernac.ml
        
        ssrvernac.mli
        
        ssrview.ml
        
        ssrview.mli
        
        ssrmatching/
        
        g_ssrmatching.ml
        
        g_ssrmatching.mli
        
        ssrmatching.ml
        
        ssrmatching.mli
        
        ssrmatching_plugin.a
        
        ssrmatching_plugin.cma
        
        ssrmatching_plugin.cmi
        
        ssrmatching_plugin.cmt
        
        ssrmatching_plugin.cmx
        
        ssrmatching_plugin.cmxa
        
        ssrmatching_plugin.cmxs
        
        ssrmatching_plugin.ml
        
        ssrmatching_plugin__G_ssrmatching.cmi
        
        ssrmatching_plugin__G_ssrmatching.cmt
        
        ssrmatching_plugin__G_ssrmatching.cmti
        
        ssrmatching_plugin__G_ssrmatching.cmx
        
        ssrmatching_plugin__Ssrmatching.cmi
        
        ssrmatching_plugin__Ssrmatching.cmt
        
        ssrmatching_plugin__Ssrmatching.cmti
        
        ssrmatching_plugin__Ssrmatching.cmx
        
        ssrsearch/
        
        g_search.ml
        
        ssrsearch_plugin.a
        
        ssrsearch_plugin.cma
        
        ssrsearch_plugin.cmi
        
        ssrsearch_plugin.cmt
        
        ssrsearch_plugin.cmx
        
        ssrsearch_plugin.cmxa
        
        ssrsearch_plugin.cmxs
        
        ssrsearch_plugin.ml
        
        ssrsearch_plugin__G_search.cmi
        
        ssrsearch_plugin__G_search.cmt
        
        ssrsearch_plugin__G_search.cmx
        
        tauto/
        
        tauto.ml
        
        tauto.mli
        
        tauto_plugin.a
        
        tauto_plugin.cma
        
        tauto_plugin.cmi
        
        tauto_plugin.cmt
        
        tauto_plugin.cmx
        
        tauto_plugin.cmxa
        
        tauto_plugin.cmxs
        
        tauto_plugin.ml
        
        tauto_plugin__Tauto.cmi
        
        tauto_plugin__Tauto.cmt
        
        tauto_plugin__Tauto.cmti
        
        tauto_plugin__Tauto.cmx
        
        tutorial/
        
        p0/
        
        g_tuto0.ml
        
        tuto0_main.ml
        
        tuto0_main.mli
        
        tuto0_plugin.a
        
        tuto0_plugin.cma
        
        tuto0_plugin.cmi
        
        tuto0_plugin.cmt
        
        tuto0_plugin.cmx
        
        tuto0_plugin.cmxa
        
        tuto0_plugin.cmxs
        
        tuto0_plugin.ml
        
        tuto0_plugin__G_tuto0.cmi
        
        tuto0_plugin__G_tuto0.cmt
        
        tuto0_plugin__G_tuto0.cmx
        
        tuto0_plugin__Tuto0_main.cmi
        
        tuto0_plugin__Tuto0_main.cmt
        
        tuto0_plugin__Tuto0_main.cmti
        
        tuto0_plugin__Tuto0_main.cmx
        
        p1/
        
        g_tuto1.ml
        
        inspector.ml
        
        inspector.mli
        
        simple_check.ml
        
        simple_check.mli
        
        simple_declare.ml
        
        simple_declare.mli
        
        simple_print.ml
        
        simple_print.mli
        
        tuto1_plugin.a
        
        tuto1_plugin.cma
        
        tuto1_plugin.cmi
        
        tuto1_plugin.cmt
        
        tuto1_plugin.cmx
        
        tuto1_plugin.cmxa
        
        tuto1_plugin.cmxs
        
        tuto1_plugin.ml
        
        tuto1_plugin__G_tuto1.cmi
        
        tuto1_plugin__G_tuto1.cmt
        
        tuto1_plugin__G_tuto1.cmx
        
        tuto1_plugin__Inspector.cmi
        
        tuto1_plugin__Inspector.cmt
        
        tuto1_plugin__Inspector.cmti
        
        tuto1_plugin__Inspector.cmx
        
        tuto1_plugin__Simple_check.cmi
        
        tuto1_plugin__Simple_check.cmt
        
        tuto1_plugin__Simple_check.cmti
        
        tuto1_plugin__Simple_check.cmx
        
        tuto1_plugin__Simple_declare.cmi
        
        tuto1_plugin__Simple_declare.cmt
        
        tuto1_plugin__Simple_declare.cmti
        
        tuto1_plugin__Simple_declare.cmx
        
        tuto1_plugin__Simple_print.cmi
        
        tuto1_plugin__Simple_print.cmt
        
        tuto1_plugin__Simple_print.cmti
        
        tuto1_plugin__Simple_print.cmx
        
        p2/
        
        counter.ml
        
        counter.mli
        
        custom.ml
        
        custom.mli
        
        g_tuto2.ml
        
        persistent_counter.ml
        
        persistent_counter.mli
        
        tuto2_plugin.a
        
        tuto2_plugin.cma
        
        tuto2_plugin.cmi
        
        tuto2_plugin.cmt
        
        tuto2_plugin.cmx
        
        tuto2_plugin.cmxa
        
        tuto2_plugin.cmxs
        
        tuto2_plugin.ml
        
        tuto2_plugin__Counter.cmi
        
        tuto2_plugin__Counter.cmt
        
        tuto2_plugin__Counter.cmti
        
        tuto2_plugin__Counter.cmx
        
        tuto2_plugin__Custom.cmi
        
        tuto2_plugin__Custom.cmt
        
        tuto2_plugin__Custom.cmti
        
        tuto2_plugin__Custom.cmx
        
        tuto2_plugin__G_tuto2.cmi
        
        tuto2_plugin__G_tuto2.cmt
        
        tuto2_plugin__G_tuto2.cmx
        
        tuto2_plugin__Persistent_counter.cmi
        
        tuto2_plugin__Persistent_counter.cmt
        
        tuto2_plugin__Persistent_counter.cmti
        
        tuto2_plugin__Persistent_counter.cmx
        
        p3/
        
        construction_game.ml
        
        construction_game.mli
        
        g_tuto3.ml
        
        tuto3_plugin.a
        
        tuto3_plugin.cma
        
        tuto3_plugin.cmi
        
        tuto3_plugin.cmt
        
        tuto3_plugin.cmx
        
        tuto3_plugin.cmxa
        
        tuto3_plugin.cmxs
        
        tuto3_plugin.ml
        
        tuto3_plugin__Construction_game.cmi
        
        tuto3_plugin__Construction_game.cmt
        
        tuto3_plugin__Construction_game.cmti
        
        tuto3_plugin__Construction_game.cmx
        
        tuto3_plugin__G_tuto3.cmi
        
        tuto3_plugin__G_tuto3.cmt
        
        tuto3_plugin__G_tuto3.cmx
        
        tuto3_plugin__Tuto_tactic.cmi
        
        tuto3_plugin__Tuto_tactic.cmt
        
        tuto3_plugin__Tuto_tactic.cmti
        
        tuto3_plugin__Tuto_tactic.cmx
        
        tuto_tactic.ml
        
        tuto_tactic.mli
        
        zify/
        
        g_zify.ml
        
        zify.ml
        
        zify.mli
        
        zify_plugin.a
        
        zify_plugin.cma
        
        zify_plugin.cmi
        
        zify_plugin.cmt
        
        zify_plugin.cmx
        
        zify_plugin.cmxa
        
        zify_plugin.cmxs
        
        zify_plugin.ml
        
        zify_plugin__G_zify.cmi
        
        zify_plugin__G_zify.cmt
        
        zify_plugin__G_zify.cmx
        
        zify_plugin__Zify.cmi
        
        zify_plugin__Zify.cmt
        
        zify_plugin__Zify.cmti
        
        zify_plugin__Zify.cmx
      - pretyping/
        
        arguments_renaming.cmi
        
        arguments_renaming.cmt
        
        arguments_renaming.cmti
        
        arguments_renaming.cmx
        
        arguments_renaming.ml
        
        arguments_renaming.mli
        
        cases.cmi
        
        cases.cmt
        
        cases.cmti
        
        cases.cmx
        
        cases.ml
        
        cases.mli
        
        cbv.cmi
        
        cbv.cmt
        
        cbv.cmti
        
        cbv.cmx
        
        cbv.ml
        
        cbv.mli
        
        coercion.cmi
        
        coercion.cmt
        
        coercion.cmti
        
        coercion.cmx
        
        coercion.ml
        
        coercion.mli
        
        coercionops.cmi
        
        coercionops.cmt
        
        coercionops.cmti
        
        coercionops.cmx
        
        coercionops.ml
        
        coercionops.mli
        
        constr_matching.cmi
        
        constr_matching.cmt
        
        constr_matching.cmti
        
        constr_matching.cmx
        
        constr_matching.ml
        
        constr_matching.mli
        
        detyping.cmi
        
        detyping.cmt
        
        detyping.cmti
        
        detyping.cmx
        
        detyping.ml
        
        detyping.mli
        
        evarconv.cmi
        
        evarconv.cmt
        
        evarconv.cmti
        
        evarconv.cmx
        
        evarconv.ml
        
        evarconv.mli
        
        evardefine.cmi
        
        evardefine.cmt
        
        evardefine.cmti
        
        evardefine.cmx
        
        evardefine.ml
        
        evardefine.mli
        
        evarsolve.cmi
        
        evarsolve.cmt
        
        evarsolve.cmti
        
        evarsolve.cmx
        
        evarsolve.ml
        
        evarsolve.mli
        
        find_subterm.cmi
        
        find_subterm.cmt
        
        find_subterm.cmti
        
        find_subterm.cmx
        
        find_subterm.ml
        
        find_subterm.mli
        
        geninterp.cmi
        
        geninterp.cmt
        
        geninterp.cmti
        
        geninterp.cmx
        
        geninterp.ml
        
        geninterp.mli
        
        globEnv.cmi
        
        globEnv.cmt
        
        globEnv.cmti
        
        globEnv.cmx
        
        globEnv.ml
        
        globEnv.mli
        
        glob_ops.cmi
        
        glob_ops.cmt
        
        glob_ops.cmti
        
        glob_ops.cmx
        
        glob_ops.ml
        
        glob_ops.mli
        
        glob_term.cmi
        
        glob_term.cmt
        
        glob_term.cmx
        
        glob_term.ml
        
        heads.cmi
        
        heads.cmt
        
        heads.cmti
        
        heads.cmx
        
        heads.ml
        
        heads.mli
        
        indrec.cmi
        
        indrec.cmt
        
        indrec.cmti
        
        indrec.cmx
        
        indrec.ml
        
        indrec.mli
        
        inductiveops.cmi
        
        inductiveops.cmt
        
        inductiveops.cmti
        
        inductiveops.cmx
        
        inductiveops.ml
        
        inductiveops.mli
        
        keys.cmi
        
        keys.cmt
        
        keys.cmti
        
        keys.cmx
        
        keys.ml
        
        keys.mli
        
        locus.cmi
        
        locus.cmt
        
        locus.cmx
        
        locus.ml
        
        locusops.cmi
        
        locusops.cmt
        
        locusops.cmti
        
        locusops.cmx
        
        locusops.ml
        
        locusops.mli
        
        ltac_pretype.cmi
        
        ltac_pretype.cmt
        
        ltac_pretype.cmx
        
        ltac_pretype.ml
        
        nativenorm.cmi
        
        nativenorm.cmt
        
        nativenorm.cmti
        
        nativenorm.cmx
        
        nativenorm.ml
        
        nativenorm.mli
        
        pattern.cmi
        
        pattern.cmt
        
        pattern.cmx
        
        pattern.ml
        
        patternops.cmi
        
        patternops.cmt
        
        patternops.cmti
        
        patternops.cmx
        
        patternops.ml
        
        patternops.mli
        
        pretype_errors.cmi
        
        pretype_errors.cmt
        
        pretype_errors.cmti
        
        pretype_errors.cmx
        
        pretype_errors.ml
        
        pretype_errors.mli
        
        pretyping.a
        
        pretyping.cma
        
        pretyping.cmi
        
        pretyping.cmt
        
        pretyping.cmti
        
        pretyping.cmx
        
        pretyping.cmxa
        
        pretyping.cmxs
        
        pretyping.ml
        
        pretyping.mli
        
        program.cmi
        
        program.cmt
        
        program.cmti
        
        program.cmx
        
        program.ml
        
        program.mli
        
        reductionops.cmi
        
        reductionops.cmt
        
        reductionops.cmti
        
        reductionops.cmx
        
        reductionops.ml
        
        reductionops.mli
        
        retyping.cmi
        
        retyping.cmt
        
        retyping.cmti
        
        retyping.cmx
        
        retyping.ml
        
        retyping.mli
        
        structures.cmi
        
        structures.cmt
        
        structures.cmti
        
        structures.cmx
        
        structures.ml
        
        structures.mli
        
        tacred.cmi
        
        tacred.cmt
        
        tacred.cmti
        
        tacred.cmx
        
        tacred.ml
        
        tacred.mli
        
        typeclasses.cmi
        
        typeclasses.cmt
        
        typeclasses.cmti
        
        typeclasses.cmx
        
        typeclasses.ml
        
        typeclasses.mli
        
        typeclasses_errors.cmi
        
        typeclasses_errors.cmt
        
        typeclasses_errors.cmti
        
        typeclasses_errors.cmx
        
        typeclasses_errors.ml
        
        typeclasses_errors.mli
        
        typing.cmi
        
        typing.cmt
        
        typing.cmti
        
        typing.cmx
        
        typing.ml
        
        typing.mli
        
        unification.cmi
        
        unification.cmt
        
        unification.cmti
        
        unification.cmx
        
        unification.ml
        
        unification.mli
        
        vnorm.cmi
        
        vnorm.cmt
        
        vnorm.cmti
        
        vnorm.cmx
        
        vnorm.ml
        
        vnorm.mli
      - printing/
        
        genprint.cmi
        
        genprint.cmt
        
        genprint.cmti
        
        genprint.cmx
        
        genprint.ml
        
        genprint.mli
        
        ppconstr.cmi
        
        ppconstr.cmt
        
        ppconstr.cmti
        
        ppconstr.cmx
        
        ppconstr.ml
        
        ppconstr.mli
        
        pputils.cmi
        
        pputils.cmt
        
        pputils.cmti
        
        pputils.cmx
        
        pputils.ml
        
        pputils.mli
        
        printer.cmi
        
        printer.cmt
        
        printer.cmti
        
        printer.cmx
        
        printer.ml
        
        printer.mli
        
        printing.a
        
        printing.cma
        
        printing.cmxa
        
        printing.cmxs
        
        proof_diffs.cmi
        
        proof_diffs.cmt
        
        proof_diffs.cmti
        
        proof_diffs.cmx
        
        proof_diffs.ml
        
        proof_diffs.mli
      - proofs/
        
        clenv.cmi
        
        clenv.cmt
        
        clenv.cmti
        
        clenv.cmx
        
        clenv.ml
        
        clenv.mli
        
        evar_refiner.cmi
        
        evar_refiner.cmt
        
        evar_refiner.cmti
        
        evar_refiner.cmx
        
        evar_refiner.ml
        
        evar_refiner.mli
        
        goal.cmi
        
        goal.cmt
        
        goal.cmti
        
        goal.cmx
        
        goal.ml
        
        goal.mli
        
        goal_select.cmi
        
        goal_select.cmt
        
        goal_select.cmti
        
        goal_select.cmx
        
        goal_select.ml
        
        goal_select.mli
        
        logic.cmi
        
        logic.cmt
        
        logic.cmti
        
        logic.cmx
        
        logic.ml
        
        logic.mli
        
        miscprint.cmi
        
        miscprint.cmt
        
        miscprint.cmti
        
        miscprint.cmx
        
        miscprint.ml
        
        miscprint.mli
        
        proof.cmi
        
        proof.cmt
        
        proof.cmti
        
        proof.cmx
        
        proof.ml
        
        proof.mli
        
        proof_bullet.cmi
        
        proof_bullet.cmt
        
        proof_bullet.cmti
        
        proof_bullet.cmx
        
        proof_bullet.ml
        
        proof_bullet.mli
        
        proofs.a
        
        proofs.cma
        
        proofs.cmxa
        
        proofs.cmxs
        
        refine.cmi
        
        refine.cmt
        
        refine.cmti
        
        refine.cmx
        
        refine.ml
        
        refine.mli
        
        tacmach.cmi
        
        tacmach.cmt
        
        tacmach.cmti
        
        tacmach.cmx
        
        tacmach.ml
        
        tacmach.mli
        
        tactypes.cmi
        
        tactypes.cmt
        
        tactypes.cmx
        
        tactypes.ml
      - revision
      - stm/
        
        asyncTaskQueue.cmi
        
        asyncTaskQueue.cmt
        
        asyncTaskQueue.cmti
        
        asyncTaskQueue.cmx
        
        asyncTaskQueue.ml
        
        asyncTaskQueue.mli
        
        coqworkmgrApi.cmi
        
        coqworkmgrApi.cmt
        
        coqworkmgrApi.cmti
        
        coqworkmgrApi.cmx
        
        coqworkmgrApi.ml
        
        coqworkmgrApi.mli
        
        dag.cmi
        
        dag.cmt
        
        dag.cmti
        
        dag.cmx
        
        dag.ml
        
        dag.mli
        
        partac.cmi
        
        partac.cmt
        
        partac.cmti
        
        partac.cmx
        
        partac.ml
        
        partac.mli
        
        proofBlockDelimiter.cmi
        
        proofBlockDelimiter.cmt
        
        proofBlockDelimiter.cmti
        
        proofBlockDelimiter.cmx
        
        proofBlockDelimiter.ml
        
        proofBlockDelimiter.mli
        
        spawned.cmi
        
        spawned.cmt
        
        spawned.cmti
        
        spawned.cmx
        
        spawned.ml
        
        spawned.mli
        
        stm.a
        
        stm.cma
        
        stm.cmi
        
        stm.cmt
        
        stm.cmti
        
        stm.cmx
        
        stm.cmxa
        
        stm.cmxs
        
        stm.ml
        
        stm.mli
        
        stmargs.cmi
        
        stmargs.cmt
        
        stmargs.cmti
        
        stmargs.cmx
        
        stmargs.ml
        
        stmargs.mli
        
        tQueue.cmi
        
        tQueue.cmt
        
        tQueue.cmti
        
        tQueue.cmx
        
        tQueue.ml
        
        tQueue.mli
        
        vcs.cmi
        
        vcs.cmt
        
        vcs.cmti
        
        vcs.cmx
        
        vcs.ml
        
        vcs.mli
        
        vio_checking.cmi
        
        vio_checking.cmt
        
        vio_checking.cmti
        
        vio_checking.cmx
        
        vio_checking.ml
        
        vio_checking.mli
        
        workerPool.cmi
        
        workerPool.cmt
        
        workerPool.cmti
        
        workerPool.cmx
        
        workerPool.ml
        
        workerPool.mli
      - sysinit/
        
        coqargs.cmi
        
        coqargs.cmt
        
        coqargs.cmti
        
        coqargs.cmx
        
        coqargs.ml
        
        coqargs.mli
        
        coqinit.cmi
        
        coqinit.cmt
        
        coqinit.cmti
        
        coqinit.cmx
        
        coqinit.ml
        
        coqinit.mli
        
        coqloadpath.cmi
        
        coqloadpath.cmt
        
        coqloadpath.cmti
        
        coqloadpath.cmx
        
        coqloadpath.ml
        
        coqloadpath.mli
        
        sysinit.a
        
        sysinit.cma
        
        sysinit.cmxa
        
        sysinit.cmxs
        
        usage.cmi
        
        usage.cmt
        
        usage.cmti
        
        usage.cmx
        
        usage.ml
        
        usage.mli
      - tactics/
        
        abstract.cmi
        
        abstract.cmt
        
        abstract.cmti
        
        abstract.cmx
        
        abstract.ml
        
        abstract.mli
        
        auto.cmi
        
        auto.cmt
        
        auto.cmti
        
        auto.cmx
        
        auto.ml
        
        auto.mli
        
        autorewrite.cmi
        
        autorewrite.cmt
        
        autorewrite.cmti
        
        autorewrite.cmx
        
        autorewrite.ml
        
        autorewrite.mli
        
        btermdn.cmi
        
        btermdn.cmt
        
        btermdn.cmti
        
        btermdn.cmx
        
        btermdn.ml
        
        btermdn.mli
        
        cbn.cmi
        
        cbn.cmt
        
        cbn.cmti
        
        cbn.cmx
        
        cbn.ml
        
        cbn.mli
        
        class_tactics.cmi
        
        class_tactics.cmt
        
        class_tactics.cmti
        
        class_tactics.cmx
        
        class_tactics.ml
        
        class_tactics.mli
        
        contradiction.cmi
        
        contradiction.cmt
        
        contradiction.cmti
        
        contradiction.cmx
        
        contradiction.ml
        
        contradiction.mli
        
        declareScheme.cmi
        
        declareScheme.cmt
        
        declareScheme.cmti
        
        declareScheme.cmx
        
        declareScheme.ml
        
        declareScheme.mli
        
        declareUctx.cmi
        
        declareUctx.cmt
        
        declareUctx.cmti
        
        declareUctx.cmx
        
        declareUctx.ml
        
        declareUctx.mli
        
        dn.cmi
        
        dn.cmt
        
        dn.cmti
        
        dn.cmx
        
        dn.ml
        
        dn.mli
        
        dnet.cmi
        
        dnet.cmt
        
        dnet.cmti
        
        dnet.cmx
        
        dnet.ml
        
        dnet.mli
        
        eauto.cmi
        
        eauto.cmt
        
        eauto.cmti
        
        eauto.cmx
        
        eauto.ml
        
        eauto.mli
        
        elim.cmi
        
        elim.cmt
        
        elim.cmti
        
        elim.cmx
        
        elim.ml
        
        elim.mli
        
        elimschemes.cmi
        
        elimschemes.cmt
        
        elimschemes.cmti
        
        elimschemes.cmx
        
        elimschemes.ml
        
        elimschemes.mli
        
        eqdecide.cmi
        
        eqdecide.cmt
        
        eqdecide.cmti
        
        eqdecide.cmx
        
        eqdecide.ml
        
        eqdecide.mli
        
        eqschemes.cmi
        
        eqschemes.cmt
        
        eqschemes.cmti
        
        eqschemes.cmx
        
        eqschemes.ml
        
        eqschemes.mli
        
        equality.cmi
        
        equality.cmt
        
        equality.cmti
        
        equality.cmx
        
        equality.ml
        
        equality.mli
        
        genredexpr.cmi
        
        genredexpr.cmt
        
        genredexpr.cmx
        
        genredexpr.ml
        
        hints.cmi
        
        hints.cmt
        
        hints.cmti
        
        hints.cmx
        
        hints.ml
        
        hints.mli
        
        hipattern.cmi
        
        hipattern.cmt
        
        hipattern.cmti
        
        hipattern.cmx
        
        hipattern.ml
        
        hipattern.mli
        
        ind_tables.cmi
        
        ind_tables.cmt
        
        ind_tables.cmti
        
        ind_tables.cmx
        
        ind_tables.ml
        
        ind_tables.mli
        
        inv.cmi
        
        inv.cmt
        
        inv.cmti
        
        inv.cmx
        
        inv.ml
        
        inv.mli
        
        ppred.cmi
        
        ppred.cmt
        
        ppred.cmti
        
        ppred.cmx
        
        ppred.ml
        
        ppred.mli
        
        redexpr.cmi
        
        redexpr.cmt
        
        redexpr.cmti
        
        redexpr.cmx
        
        redexpr.ml
        
        redexpr.mli
        
        redops.cmi
        
        redops.cmt
        
        redops.cmti
        
        redops.cmx
        
        redops.ml
        
        redops.mli
        
        tacticals.cmi
        
        tacticals.cmt
        
        tacticals.cmti
        
        tacticals.cmx
        
        tacticals.ml
        
        tacticals.mli
        
        tactics.a
        
        tactics.cma
        
        tactics.cmi
        
        tactics.cmt
        
        tactics.cmti
        
        tactics.cmx
        
        tactics.cmxa
        
        tactics.cmxs
        
        tactics.ml
        
        tactics.mli
        
        term_dnet.cmi
        
        term_dnet.cmt
        
        term_dnet.cmti
        
        term_dnet.cmx
        
        term_dnet.ml
        
        term_dnet.mli
      - tools/
        
        CoqMakefile.in
        
        TimeFileMaker.py
        
        coqdoc/
        
        coqdoc.css
        
        coqdoc.sty
        
        make-both-single-timing-files.py
        
        make-both-time-files.py
        
        make-one-time-file.py
      - top_printers/
        
        top_printers.a
        
        top_printers.cma
        
        top_printers.cmi
        
        top_printers.cmt
        
        top_printers.cmti
        
        top_printers.cmx
        
        top_printers.cmxa
        
        top_printers.cmxs
        
        top_printers.ml
        
        top_printers.mli
      - toplevel/
        
        ccompile.cmi
        
        ccompile.cmt
        
        ccompile.cmti
        
        ccompile.cmx
        
        ccompile.ml
        
        ccompile.mli
        
        coqc.cmi
        
        coqc.cmt
        
        coqc.cmti
        
        coqc.cmx
        
        coqc.ml
        
        coqc.mli
        
        coqcargs.cmi
        
        coqcargs.cmt
        
        coqcargs.cmti
        
        coqcargs.cmx
        
        coqcargs.ml
        
        coqcargs.mli
        
        coqloop.cmi
        
        coqloop.cmt
        
        coqloop.cmti
        
        coqloop.cmx
        
        coqloop.ml
        
        coqloop.mli
        
        coqrc.cmi
        
        coqrc.cmt
        
        coqrc.cmti
        
        coqrc.cmx
        
        coqrc.ml
        
        coqrc.mli
        
        coqtop.cmi
        
        coqtop.cmt
        
        coqtop.cmti
        
        coqtop.cmx
        
        coqtop.ml
        
        coqtop.mli
        
        g_toplevel.cmi
        
        g_toplevel.cmt
        
        g_toplevel.cmx
        
        g_toplevel.ml
        
        toplevel.a
        
        toplevel.cma
        
        toplevel.cmxa
        
        toplevel.cmxs
        
        vernac.cmi
        
        vernac.cmt
        
        vernac.cmti
        
        vernac.cmx
        
        vernac.ml
        
        vernac.mli
        
        workerLoop.cmi
        
        workerLoop.cmt
        
        workerLoop.cmti
        
        workerLoop.cmx
        
        workerLoop.ml
        
        workerLoop.mli
      - vernac/
        
        assumptions.cmi
        
        assumptions.cmt
        
        assumptions.cmti
        
        assumptions.cmx
        
        assumptions.ml
        
        assumptions.mli
        
        attributes.cmi
        
        attributes.cmt
        
        attributes.cmti
        
        attributes.cmx
        
        attributes.ml
        
        attributes.mli
        
        auto_ind_decl.cmi
        
        auto_ind_decl.cmt
        
        auto_ind_decl.cmti
        
        auto_ind_decl.cmx
        
        auto_ind_decl.ml
        
        auto_ind_decl.mli
        
        canonical.cmi
        
        canonical.cmt
        
        canonical.cmti
        
        canonical.cmx
        
        canonical.ml
        
        canonical.mli
        
        classes.cmi
        
        classes.cmt
        
        classes.cmti
        
        classes.cmx
        
        classes.ml
        
        classes.mli
        
        comArguments.cmi
        
        comArguments.cmt
        
        comArguments.cmti
        
        comArguments.cmx
        
        comArguments.ml
        
        comArguments.mli
        
        comAssumption.cmi
        
        comAssumption.cmt
        
        comAssumption.cmti
        
        comAssumption.cmx
        
        comAssumption.ml
        
        comAssumption.mli
        
        comCoercion.cmi
        
        comCoercion.cmt
        
        comCoercion.cmti
        
        comCoercion.cmx
        
        comCoercion.ml
        
        comCoercion.mli
        
        comDefinition.cmi
        
        comDefinition.cmt
        
        comDefinition.cmti
        
        comDefinition.cmx
        
        comDefinition.ml
        
        comDefinition.mli
        
        comFixpoint.cmi
        
        comFixpoint.cmt
        
        comFixpoint.cmti
        
        comFixpoint.cmx
        
        comFixpoint.ml
        
        comFixpoint.mli
        
        comHints.cmi
        
        comHints.cmt
        
        comHints.cmti
        
        comHints.cmx
        
        comHints.ml
        
        comHints.mli
        
        comInductive.cmi
        
        comInductive.cmt
        
        comInductive.cmti
        
        comInductive.cmx
        
        comInductive.ml
        
        comInductive.mli
        
        comPrimitive.cmi
        
        comPrimitive.cmt
        
        comPrimitive.cmti
        
        comPrimitive.cmx
        
        comPrimitive.ml
        
        comPrimitive.mli
        
        comProgramFixpoint.cmi
        
        comProgramFixpoint.cmt
        
        comProgramFixpoint.cmti
        
        comProgramFixpoint.cmx
        
        comProgramFixpoint.ml
        
        comProgramFixpoint.mli
        
        comSearch.cmi
        
        comSearch.cmt
        
        comSearch.cmti
        
        comSearch.cmx
        
        comSearch.ml
        
        comSearch.mli
        
        comTactic.cmi
        
        comTactic.cmt
        
        comTactic.cmti
        
        comTactic.cmx
        
        comTactic.ml
        
        comTactic.mli
        
        debugHook.cmi
        
        debugHook.cmt
        
        debugHook.cmti
        
        debugHook.cmx
        
        debugHook.ml
        
        debugHook.mli
        
        declare.cmi
        
        declare.cmt
        
        declare.cmti
        
        declare.cmx
        
        declare.ml
        
        declare.mli
        
        declareInd.cmi
        
        declareInd.cmt
        
        declareInd.cmti
        
        declareInd.cmx
        
        declareInd.ml
        
        declareInd.mli
        
        declareUniv.cmi
        
        declareUniv.cmt
        
        declareUniv.cmti
        
        declareUniv.cmx
        
        declareUniv.ml
        
        declareUniv.mli
        
        declaremods.cmi
        
        declaremods.cmt
        
        declaremods.cmti
        
        declaremods.cmx
        
        declaremods.ml
        
        declaremods.mli
        
        egramcoq.cmi
        
        egramcoq.cmt
        
        egramcoq.cmti
        
        egramcoq.cmx
        
        egramcoq.ml
        
        egramcoq.mli
        
        egramml.cmi
        
        egramml.cmt
        
        egramml.cmti
        
        egramml.cmx
        
        egramml.ml
        
        egramml.mli
        
        g_proofs.cmi
        
        g_proofs.cmt
        
        g_proofs.cmx
        
        g_proofs.ml
        
        g_vernac.cmi
        
        g_vernac.cmt
        
        g_vernac.cmx
        
        g_vernac.ml
        
        himsg.cmi
        
        himsg.cmt
        
        himsg.cmti
        
        himsg.cmx
        
        himsg.ml
        
        himsg.mli
        
        indschemes.cmi
        
        indschemes.cmt
        
        indschemes.cmti
        
        indschemes.cmx
        
        indschemes.ml
        
        indschemes.mli
        
        library.cmi
        
        library.cmt
        
        library.cmti
        
        library.cmx
        
        library.ml
        
        library.mli
        
        loadpath.cmi
        
        loadpath.cmt
        
        loadpath.cmti
        
        loadpath.cmx
        
        loadpath.ml
        
        loadpath.mli
        
        locality.cmi
        
        locality.cmt
        
        locality.cmti
        
        locality.cmx
        
        locality.ml
        
        locality.mli
        
        metasyntax.cmi
        
        metasyntax.cmt
        
        metasyntax.cmti
        
        metasyntax.cmx
        
        metasyntax.ml
        
        metasyntax.mli
        
        mltop.cmi
        
        mltop.cmt
        
        mltop.cmti
        
        mltop.cmx
        
        mltop.ml
        
        mltop.mli
        
        ppvernac.cmi
        
        ppvernac.cmt
        
        ppvernac.cmti
        
        ppvernac.cmx
        
        ppvernac.ml
        
        ppvernac.mli
        
        prettyp.cmi
        
        prettyp.cmt
        
        prettyp.cmti
        
        prettyp.cmx
        
        prettyp.ml
        
        prettyp.mli
        
        printmod.cmi
        
        printmod.cmt
        
        printmod.cmti
        
        printmod.cmx
        
        printmod.ml
        
        printmod.mli
        
        proof_using.cmi
        
        proof_using.cmt
        
        proof_using.cmti
        
        proof_using.cmx
        
        proof_using.ml
        
        proof_using.mli
        
        pvernac.cmi
        
        pvernac.cmt
        
        pvernac.cmti
        
        pvernac.cmx
        
        pvernac.ml
        
        pvernac.mli
        
        recLemmas.cmi
        
        recLemmas.cmt
        
        recLemmas.cmti
        
        recLemmas.cmx
        
        recLemmas.ml
        
        recLemmas.mli
        
        record.cmi
        
        record.cmt
        
        record.cmti
        
        record.cmx
        
        record.ml
        
        record.mli
        
        retrieveObl.cmi
        
        retrieveObl.cmt
        
        retrieveObl.cmti
        
        retrieveObl.cmx
        
        retrieveObl.ml
        
        retrieveObl.mli
        
        search.cmi
        
        search.cmt
        
        search.cmti
        
        search.cmx
        
        search.ml
        
        search.mli
        
        topfmt.cmi
        
        topfmt.cmt
        
        topfmt.cmti
        
        topfmt.cmx
        
        topfmt.ml
        
        topfmt.mli
        
        vernac.a
        
        vernac.cma
        
        vernac.cmxa
        
        vernac.cmxs
        
        vernac_classifier.cmi
        
        vernac_classifier.cmt
        
        vernac_classifier.cmti
        
        vernac_classifier.cmx
        
        vernac_classifier.ml
        
        vernac_classifier.mli
        
        vernacentries.cmi
        
        vernacentries.cmt
        
        vernacentries.cmti
        
        vernacentries.cmx
        
        vernacentries.ml
        
        vernacentries.mli
        
        vernacexpr.cmi
        
        vernacexpr.cmt
        
        vernacexpr.cmx
        
        vernacexpr.ml
        
        vernacextend.cmi
        
        vernacextend.cmt
        
        vernacextend.cmti
        
        vernacextend.cmx
        
        vernacextend.ml
        
        vernacextend.mli
        
        vernacinterp.cmi
        
        vernacinterp.cmt
        
        vernacinterp.cmti
        
        vernacinterp.cmx
        
        vernacinterp.ml
        
        vernacinterp.mli
        
        vernacprop.cmi
        
        vernacprop.cmt
        
        vernacprop.cmti
        
        vernacprop.cmx
        
        vernacprop.ml
        
        vernacprop.mli
        
        vernacstate.cmi
        
        vernacstate.cmt
        
        vernacstate.cmti
        
        vernacstate.cmx
        
        vernacstate.ml
        
        vernacstate.mli
      - vm/
        
        coqrun.a
        
        coqrun.cma
        
        coqrun.cmi
        
        coqrun.cmt
        
        coqrun.cmx
        
        coqrun.cmxa
        
        coqrun.cmxs
        
        coqrun.ml
        
        libcoqrun_stubs.a
    - coq-doc/
      - opam
    - stublibs/
      - dllcoqrun_stubs.so
- share/
  - doc/
    - coq-core/
      - README.md
  - licenses/
    - coq-core/
      - LICENSE
  - man/
    - man1/
      - coq-tex.1.gz
      - coq_makefile.1.gz
      - coqc.1.gz
      - coqchk.1.gz
      - coqdep.1.gz
      - coqdoc.1.gz
      - coqnative.1.gz
      - coqtop.1.gz
      - coqtop.byte.1.gz
      - coqtop.opt.1.gz
      - coqwc.1.gz
  - texlive/
    - texmf-dist/
      - tex/
        
        latex/
        
        misc/
        
        coqdoc.sty

Sources on Pagure