kpriv/pkgsrc
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity
pkgsrc/lang/coq/PLIST
tonio 6f37dbf143 Update lang/coq to 8.3 
Main changes:
Includes a new tactic (nsatz, standing for Hilbert's NullStellensatz, that
extends ring to systems of polynomial equations) and a few new libraries (a
certification of mergesort, a new library of finite sets with computational and
logical contents separated).

This version also comes with many improvements of existing features, especially
regarding the tactics, the module system, extraction, the type classes, the
program command, libraries, coqdoc. Here is an excerpt:
* new operator <+ for conveniently chaining application of functors
* new round of extension of the modular library of arithmetic
* support for matching terms with binders in Ltac,
* linking notations in coqdoc,
* quote tactic now working on arbitrary expressions,
* Lemma and co accept parameters that are automatically introduced,
* interactive proofs in module types,
* a beautifying coqc option for pretty-printing files

See the file CHANGES for a full log of changes.
2010-11-14 20:53:02 +00:00

934 lines
33 KiB
Text
Raw Blame History

@comment $NetBSD: PLIST,v 1.11 2010/11/14 20:53:02 tonio Exp $
bin/coq-tex
bin/coq_makefile
bin/coqc
bin/coqchk
bin/coqdep
bin/coqdoc
${PLIST.coqide}bin/coqide
bin/coqmktop
bin/coqtop
bin/coqtop.byte
${PLIST.coqide}bin/coqide.byte
bin/coqwc
bin/gallina
lib/coq/config/coq_config.cmi
lib/coq/config/coq_config.cmo
lib/coq/config/coq_config.cmx
lib/coq/config/coq_config.o
lib/coq/dllcoqrun.so
lib/coq/ide/.coqide-gtk2rc
lib/coq/ide/FAQ
${PLIST.coqide}lib/coq/ide/command_windows.cmi
${PLIST.coqide}lib/coq/ide/config_lexer.cmi
${PLIST.coqide}lib/coq/ide/config_parser.cmi
${PLIST.coqide}lib/coq/ide/coq.cmi
lib/coq/ide/coq.png
${PLIST.coqide}lib/coq/ide/coq_commands.cmi
${PLIST.coqide}lib/coq/ide/coq_lex.cmi
${PLIST.coqide}lib/coq/ide/coq_tactics.cmi
${PLIST.coqide}lib/coq/ide/coqide.cmi
${PLIST.coqide}lib/coq/ide/gtk_parsing.cmi
${PLIST.coqide}lib/coq/ide/ide.a
${PLIST.coqide}lib/coq/ide/ide.cma
${PLIST.coqide}lib/coq/ide/ide.cmxa
${PLIST.coqide}lib/coq/ide/ideutils.cmi
${PLIST.coqide}lib/coq/ide/preferences.cmi
${PLIST.coqide}lib/coq/ide/tags.cmi
${PLIST.coqide}lib/coq/ide/typed_notebook.cmi
${PLIST.coqide}lib/coq/ide/undo.cmi
${PLIST.coqide}lib/coq/ide/utf8_convert.cmi
${PLIST.coqide}lib/coq/ide/utils/config_file.cmi
${PLIST.coqide}lib/coq/ide/utils/configwin.cmi
${PLIST.coqide}lib/coq/ide/utils/configwin_ihm.cmi
${PLIST.coqide}lib/coq/ide/utils/configwin_keys.cmi
${PLIST.coqide}lib/coq/ide/utils/configwin_messages.cmi
${PLIST.coqide}lib/coq/ide/utils/configwin_types.cmi
${PLIST.coqide}lib/coq/ide/utils/editable_cells.cmi
${PLIST.coqide}lib/coq/ide/utils/okey.cmi
lib/coq/interp/constrextern.cmi
lib/coq/interp/constrintern.cmi
lib/coq/interp/coqlib.cmi
lib/coq/interp/dumpglob.cmi
lib/coq/interp/genarg.cmi
lib/coq/interp/implicit_quantifiers.cmi
lib/coq/interp/interp.a
lib/coq/interp/interp.cma
lib/coq/interp/interp.cmxa
lib/coq/interp/modintern.cmi
lib/coq/interp/notation.cmi
lib/coq/interp/ppextend.cmi
lib/coq/interp/reserve.cmi
lib/coq/interp/smartlocate.cmi
lib/coq/interp/syntax_def.cmi
lib/coq/interp/topconstr.cmi
lib/coq/kernel/cbytecodes.cmi
lib/coq/kernel/cbytegen.cmi
lib/coq/kernel/cemitcodes.cmi
lib/coq/kernel/closure.cmi
lib/coq/kernel/conv_oracle.cmi
lib/coq/kernel/cooking.cmi
lib/coq/kernel/copcodes.cmi
lib/coq/kernel/csymtable.cmi
lib/coq/kernel/declarations.cmi
lib/coq/kernel/entries.cmi
lib/coq/kernel/environ.cmi
lib/coq/kernel/esubst.cmi
lib/coq/kernel/indtypes.cmi
lib/coq/kernel/inductive.cmi
lib/coq/kernel/kernel.a
lib/coq/kernel/kernel.cma
lib/coq/kernel/kernel.cmxa
lib/coq/kernel/mod_subst.cmi
lib/coq/kernel/mod_typing.cmi
lib/coq/kernel/modops.cmi
lib/coq/kernel/names.cmi
lib/coq/kernel/pre_env.cmi
lib/coq/kernel/reduction.cmi
lib/coq/kernel/retroknowledge.cmi
lib/coq/kernel/safe_typing.cmi
lib/coq/kernel/sign.cmi
lib/coq/kernel/subtyping.cmi
lib/coq/kernel/term.cmi
lib/coq/kernel/term_typing.cmi
lib/coq/kernel/type_errors.cmi
lib/coq/kernel/typeops.cmi
lib/coq/kernel/univ.cmi
lib/coq/kernel/vconv.cmi
lib/coq/kernel/vm.cmi
lib/coq/lib/bigint.cmi
lib/coq/lib/bstack.cmi
lib/coq/lib/compat.cmi
lib/coq/lib/dnet.cmi
lib/coq/lib/dyn.cmi
lib/coq/lib/edit.cmi
lib/coq/lib/envars.cmi
lib/coq/lib/explore.cmi
lib/coq/lib/flags.cmi
lib/coq/lib/fmap.cmi
lib/coq/lib/fset.cmi
lib/coq/lib/gmap.cmi
lib/coq/lib/gmapl.cmi
lib/coq/lib/gset.cmi
lib/coq/lib/hashcons.cmi
lib/coq/lib/heap.cmi
lib/coq/lib/lib.a
lib/coq/lib/lib.cma
lib/coq/lib/lib.cmxa
lib/coq/lib/option.cmi
lib/coq/lib/pp.cmi
lib/coq/lib/pp_control.cmi
lib/coq/lib/predicate.cmi
lib/coq/lib/profile.cmi
lib/coq/lib/rtree.cmi
lib/coq/lib/segmenttree.cmi
lib/coq/lib/system.cmi
lib/coq/lib/tlm.cmi
lib/coq/lib/tries.cmi
lib/coq/lib/unicodetable.cmi
lib/coq/lib/util.cmi
lib/coq/libcoqrun.a
lib/coq/library/decl_kinds.cmi
lib/coq/library/declare.cmi
lib/coq/library/declaremods.cmi
lib/coq/library/decls.cmi
lib/coq/library/dischargedhypsmap.cmi
lib/coq/library/global.cmi
lib/coq/library/goptions.cmi
lib/coq/library/heads.cmi
lib/coq/library/impargs.cmi
lib/coq/library/lib.cmi
lib/coq/library/libnames.cmi
lib/coq/library/libobject.cmi
lib/coq/library/library.a
lib/coq/library/library.cma
lib/coq/library/library.cmi
lib/coq/library/library.cmxa
lib/coq/library/nameops.cmi
lib/coq/library/nametab.cmi
lib/coq/library/states.cmi
lib/coq/library/summary.cmi
lib/coq/parsing/egrammar.cmi
lib/coq/parsing/extend.cmi
lib/coq/parsing/extrawit.cmi
lib/coq/parsing/g_constr.cmi
lib/coq/parsing/g_decl_mode.cmi
lib/coq/parsing/g_ltac.cmi
lib/coq/parsing/g_prim.cmi
lib/coq/parsing/g_proofs.cmi
lib/coq/parsing/g_tactic.cmi
lib/coq/parsing/g_vernac.cmi
lib/coq/parsing/g_xml.cmi
lib/coq/parsing/grammar.cma
lib/coq/parsing/highparsing.a
lib/coq/parsing/highparsing.cma
lib/coq/parsing/highparsing.cmxa
lib/coq/parsing/lexer.cmi
lib/coq/parsing/parsing.a
lib/coq/parsing/parsing.cma
lib/coq/parsing/parsing.cmxa
lib/coq/parsing/pcoq.cmi
lib/coq/parsing/ppconstr.cmi
lib/coq/parsing/ppdecl_proof.cmi
lib/coq/parsing/pptactic.cmi
lib/coq/parsing/ppvernac.cmi
lib/coq/parsing/prettyp.cmi
lib/coq/parsing/printer.cmi
lib/coq/parsing/printmod.cmi
lib/coq/parsing/tactic_printer.cmi
lib/coq/plugins/cc/cc_plugin.a
lib/coq/plugins/cc/cc_plugin.cma
lib/coq/plugins/cc/cc_plugin.cmxa
lib/coq/plugins/cc/cc_plugin_mod.cmi
lib/coq/plugins/cc/ccalgo.cmi
lib/coq/plugins/cc/ccproof.cmi
lib/coq/plugins/cc/cctac.cmi
lib/coq/plugins/cc/g_congruence.cmi
lib/coq/plugins/dp/Dp.vo
lib/coq/plugins/dp/dp.cmi
lib/coq/plugins/dp/dp_plugin.a
lib/coq/plugins/dp/dp_plugin.cma
lib/coq/plugins/dp/dp_plugin.cmxa
lib/coq/plugins/dp/dp_plugin_mod.cmi
lib/coq/plugins/dp/dp_why.cmi
lib/coq/plugins/dp/dp_zenon.cmi
lib/coq/plugins/dp/g_dp.cmi
lib/coq/plugins/extraction/ExtrOcamlBasic.vo
lib/coq/plugins/extraction/ExtrOcamlBigIntConv.vo
lib/coq/plugins/extraction/ExtrOcamlIntConv.vo
lib/coq/plugins/extraction/ExtrOcamlNatBigInt.vo
lib/coq/plugins/extraction/ExtrOcamlNatInt.vo
lib/coq/plugins/extraction/ExtrOcamlString.vo
lib/coq/plugins/extraction/ExtrOcamlZBigInt.vo
lib/coq/plugins/extraction/ExtrOcamlZInt.vo
lib/coq/plugins/extraction/common.cmi
lib/coq/plugins/extraction/extract_env.cmi
lib/coq/plugins/extraction/extraction.cmi
lib/coq/plugins/extraction/extraction_plugin.a
lib/coq/plugins/extraction/extraction_plugin.cma
lib/coq/plugins/extraction/extraction_plugin.cmxa
lib/coq/plugins/extraction/extraction_plugin_mod.cmi
lib/coq/plugins/extraction/g_extraction.cmi
lib/coq/plugins/extraction/haskell.cmi
lib/coq/plugins/extraction/mlutil.cmi
lib/coq/plugins/extraction/modutil.cmi
lib/coq/plugins/extraction/ocaml.cmi
lib/coq/plugins/extraction/scheme.cmi
lib/coq/plugins/extraction/table.cmi
lib/coq/plugins/field/LegacyField.vo
lib/coq/plugins/field/LegacyField_Compl.vo
lib/coq/plugins/field/LegacyField_Tactic.vo
lib/coq/plugins/field/LegacyField_Theory.vo
lib/coq/plugins/field/field.cmi
lib/coq/plugins/field/field_plugin.a
lib/coq/plugins/field/field_plugin.cma
lib/coq/plugins/field/field_plugin.cmxa
lib/coq/plugins/field/field_plugin_mod.cmi
lib/coq/plugins/firstorder/formula.cmi
lib/coq/plugins/firstorder/g_ground.cmi
lib/coq/plugins/firstorder/ground.cmi
lib/coq/plugins/firstorder/ground_plugin.a
lib/coq/plugins/firstorder/ground_plugin.cma
lib/coq/plugins/firstorder/ground_plugin.cmxa
lib/coq/plugins/firstorder/ground_plugin_mod.cmi
lib/coq/plugins/firstorder/instances.cmi
lib/coq/plugins/firstorder/rules.cmi
lib/coq/plugins/firstorder/sequent.cmi
lib/coq/plugins/firstorder/unify.cmi
lib/coq/plugins/fourier/Fourier.vo
lib/coq/plugins/fourier/Fourier_util.vo
lib/coq/plugins/fourier/fourier.cmi
lib/coq/plugins/fourier/fourierR.cmi
lib/coq/plugins/fourier/fourier_plugin.a
lib/coq/plugins/fourier/fourier_plugin.cma
lib/coq/plugins/fourier/fourier_plugin.cmxa
lib/coq/plugins/fourier/fourier_plugin_mod.cmi
lib/coq/plugins/fourier/g_fourier.cmi
lib/coq/plugins/funind/Recdef.vo
lib/coq/plugins/funind/functional_principles_proofs.cmi
lib/coq/plugins/funind/functional_principles_types.cmi
lib/coq/plugins/funind/g_indfun.cmi
lib/coq/plugins/funind/indfun.cmi
lib/coq/plugins/funind/indfun_common.cmi
lib/coq/plugins/funind/invfun.cmi
lib/coq/plugins/funind/merge.cmi
lib/coq/plugins/funind/rawterm_to_relation.cmi
lib/coq/plugins/funind/rawtermops.cmi
lib/coq/plugins/funind/recdef.cmi
lib/coq/plugins/funind/recdef_plugin.a
lib/coq/plugins/funind/recdef_plugin.cma
lib/coq/plugins/funind/recdef_plugin.cmxa
lib/coq/plugins/funind/recdef_plugin_mod.cmi
lib/coq/plugins/micromega/CheckerMaker.vo
lib/coq/plugins/micromega/Env.vo
lib/coq/plugins/micromega/EnvRing.vo
lib/coq/plugins/micromega/OrderedRing.vo
lib/coq/plugins/micromega/Psatz.vo
lib/coq/plugins/micromega/QMicromega.vo
lib/coq/plugins/micromega/RMicromega.vo
lib/coq/plugins/micromega/Refl.vo
lib/coq/plugins/micromega/RingMicromega.vo
lib/coq/plugins/micromega/Tauto.vo
lib/coq/plugins/micromega/VarMap.vo
lib/coq/plugins/micromega/ZCoeff.vo
lib/coq/plugins/micromega/ZMicromega.vo
lib/coq/plugins/micromega/certificate.cmi
lib/coq/plugins/micromega/coq_micromega.cmi
lib/coq/plugins/micromega/csdpcert
lib/coq/plugins/micromega/g_micromega.cmi
lib/coq/plugins/micromega/mfourier.cmi
lib/coq/plugins/micromega/micromega.cmi
lib/coq/plugins/micromega/micromega_plugin.a
lib/coq/plugins/micromega/micromega_plugin.cma
lib/coq/plugins/micromega/micromega_plugin.cmxa
lib/coq/plugins/micromega/micromega_plugin_mod.cmi
lib/coq/plugins/micromega/mutils.cmi
lib/coq/plugins/micromega/persistent_cache.cmi
lib/coq/plugins/micromega/sos_types.cmi
lib/coq/plugins/nsatz/Nsatz.vo
lib/coq/plugins/nsatz/ideal.cmi
lib/coq/plugins/nsatz/nsatz.cmi
lib/coq/plugins/nsatz/nsatz_plugin.a
lib/coq/plugins/nsatz/nsatz_plugin.cma
lib/coq/plugins/nsatz/nsatz_plugin.cmxa
lib/coq/plugins/nsatz/nsatz_plugin_mod.cmi
lib/coq/plugins/nsatz/polynom.cmi
lib/coq/plugins/nsatz/utile.cmi
lib/coq/plugins/omega/Omega.vo
lib/coq/plugins/omega/OmegaLemmas.vo
lib/coq/plugins/omega/OmegaPlugin.vo
lib/coq/plugins/omega/PreOmega.vo
lib/coq/plugins/omega/coq_omega.cmi
lib/coq/plugins/omega/g_omega.cmi
lib/coq/plugins/omega/omega.cmi
lib/coq/plugins/omega/omega_plugin.a
lib/coq/plugins/omega/omega_plugin.cma
lib/coq/plugins/omega/omega_plugin.cmxa
lib/coq/plugins/omega/omega_plugin_mod.cmi
lib/coq/plugins/quote/Quote.vo
lib/coq/plugins/quote/g_quote.cmi
lib/coq/plugins/quote/quote.cmi
lib/coq/plugins/quote/quote_plugin.a
lib/coq/plugins/quote/quote_plugin.cma
lib/coq/plugins/quote/quote_plugin.cmxa
lib/coq/plugins/quote/quote_plugin_mod.cmi
lib/coq/plugins/ring/LegacyArithRing.vo
lib/coq/plugins/ring/LegacyNArithRing.vo
lib/coq/plugins/ring/LegacyRing.vo
lib/coq/plugins/ring/LegacyRing_theory.vo
lib/coq/plugins/ring/LegacyZArithRing.vo
lib/coq/plugins/ring/Ring_abstract.vo
lib/coq/plugins/ring/Ring_normalize.vo
lib/coq/plugins/ring/Setoid_ring.vo
lib/coq/plugins/ring/Setoid_ring_normalize.vo
lib/coq/plugins/ring/Setoid_ring_theory.vo
lib/coq/plugins/ring/g_ring.cmi
lib/coq/plugins/ring/ring.cmi
lib/coq/plugins/ring/ring_plugin.a
lib/coq/plugins/ring/ring_plugin.cma
lib/coq/plugins/ring/ring_plugin.cmxa
lib/coq/plugins/ring/ring_plugin_mod.cmi
lib/coq/plugins/romega/ROmega.vo
lib/coq/plugins/romega/ReflOmegaCore.vo
lib/coq/plugins/romega/const_omega.cmi
lib/coq/plugins/romega/g_romega.cmi
lib/coq/plugins/romega/refl_omega.cmi
lib/coq/plugins/romega/romega_plugin.a
lib/coq/plugins/romega/romega_plugin.cma
lib/coq/plugins/romega/romega_plugin.cmxa
lib/coq/plugins/romega/romega_plugin_mod.cmi
lib/coq/plugins/rtauto/Bintree.vo
lib/coq/plugins/rtauto/Rtauto.vo
lib/coq/plugins/rtauto/g_rtauto.cmi
lib/coq/plugins/rtauto/proof_search.cmi
lib/coq/plugins/rtauto/refl_tauto.cmi
lib/coq/plugins/rtauto/rtauto_plugin.a
lib/coq/plugins/rtauto/rtauto_plugin.cma
lib/coq/plugins/rtauto/rtauto_plugin.cmxa
lib/coq/plugins/rtauto/rtauto_plugin_mod.cmi
lib/coq/plugins/setoid_ring/ArithRing.vo
lib/coq/plugins/setoid_ring/BinList.vo
lib/coq/plugins/setoid_ring/Field.vo
lib/coq/plugins/setoid_ring/Field_tac.vo
lib/coq/plugins/setoid_ring/Field_theory.vo
lib/coq/plugins/setoid_ring/InitialRing.vo
lib/coq/plugins/setoid_ring/NArithRing.vo
lib/coq/plugins/setoid_ring/RealField.vo
lib/coq/plugins/setoid_ring/Ring.vo
lib/coq/plugins/setoid_ring/Ring_base.vo
lib/coq/plugins/setoid_ring/Ring_equiv.vo
lib/coq/plugins/setoid_ring/Ring_polynom.vo
lib/coq/plugins/setoid_ring/Ring_tac.vo
lib/coq/plugins/setoid_ring/Ring_theory.vo
lib/coq/plugins/setoid_ring/ZArithRing.vo
lib/coq/plugins/setoid_ring/newring.cmi
lib/coq/plugins/setoid_ring/newring_plugin.a
lib/coq/plugins/setoid_ring/newring_plugin.cma
lib/coq/plugins/setoid_ring/newring_plugin.cmxa
lib/coq/plugins/setoid_ring/newring_plugin_mod.cmi
lib/coq/plugins/subtac/eterm.cmi
lib/coq/plugins/subtac/g_subtac.cmi
lib/coq/plugins/subtac/subtac.cmi
lib/coq/plugins/subtac/subtac_cases.cmi
lib/coq/plugins/subtac/subtac_classes.cmi
lib/coq/plugins/subtac/subtac_coercion.cmi
lib/coq/plugins/subtac/subtac_command.cmi
lib/coq/plugins/subtac/subtac_errors.cmi
lib/coq/plugins/subtac/subtac_obligations.cmi
lib/coq/plugins/subtac/subtac_plugin.a
lib/coq/plugins/subtac/subtac_plugin.cma
lib/coq/plugins/subtac/subtac_plugin.cmxa
lib/coq/plugins/subtac/subtac_plugin_mod.cmi
lib/coq/plugins/subtac/subtac_pretyping.cmi
lib/coq/plugins/subtac/subtac_pretyping_F.cmi
lib/coq/plugins/subtac/subtac_utils.cmi
lib/coq/plugins/syntax/ascii_syntax.cmi
lib/coq/plugins/syntax/ascii_syntax_plugin.a
lib/coq/plugins/syntax/ascii_syntax_plugin.cma
lib/coq/plugins/syntax/ascii_syntax_plugin.cmxa
lib/coq/plugins/syntax/ascii_syntax_plugin_mod.cmi
lib/coq/plugins/syntax/nat_syntax.cmi
lib/coq/plugins/syntax/nat_syntax_plugin.a
lib/coq/plugins/syntax/nat_syntax_plugin.cma
lib/coq/plugins/syntax/nat_syntax_plugin.cmxa
lib/coq/plugins/syntax/nat_syntax_plugin_mod.cmi
lib/coq/plugins/syntax/numbers_syntax.cmi
lib/coq/plugins/syntax/numbers_syntax_plugin.a
lib/coq/plugins/syntax/numbers_syntax_plugin.cma
lib/coq/plugins/syntax/numbers_syntax_plugin.cmxa
lib/coq/plugins/syntax/numbers_syntax_plugin_mod.cmi
lib/coq/plugins/syntax/r_syntax.cmi
lib/coq/plugins/syntax/r_syntax_plugin.a
lib/coq/plugins/syntax/r_syntax_plugin.cma
lib/coq/plugins/syntax/r_syntax_plugin.cmxa
lib/coq/plugins/syntax/r_syntax_plugin_mod.cmi
lib/coq/plugins/syntax/string_syntax.cmi
lib/coq/plugins/syntax/string_syntax_plugin.a
lib/coq/plugins/syntax/string_syntax_plugin.cma
lib/coq/plugins/syntax/string_syntax_plugin.cmxa
lib/coq/plugins/syntax/string_syntax_plugin_mod.cmi
lib/coq/plugins/syntax/z_syntax.cmi
lib/coq/plugins/syntax/z_syntax_plugin.a
lib/coq/plugins/syntax/z_syntax_plugin.cma
lib/coq/plugins/syntax/z_syntax_plugin.cmxa
lib/coq/plugins/syntax/z_syntax_plugin_mod.cmi
lib/coq/plugins/xml/acic.cmi
lib/coq/plugins/xml/acic2Xml.cmi
lib/coq/plugins/xml/cic2Xml.cmi
lib/coq/plugins/xml/cic2acic.cmi
lib/coq/plugins/xml/doubleTypeInference.cmi
lib/coq/plugins/xml/dumptree.cmi
lib/coq/plugins/xml/proof2aproof.cmi
lib/coq/plugins/xml/proofTree2Xml.cmi
lib/coq/plugins/xml/unshare.cmi
lib/coq/plugins/xml/xml.cmi
lib/coq/plugins/xml/xml_plugin.a
lib/coq/plugins/xml/xml_plugin.cma
lib/coq/plugins/xml/xml_plugin.cmxa
lib/coq/plugins/xml/xml_plugin_mod.cmi
lib/coq/plugins/xml/xmlcommand.cmi
lib/coq/plugins/xml/xmlentries.cmi
lib/coq/pretyping/cases.cmi
lib/coq/pretyping/cbv.cmi
lib/coq/pretyping/classops.cmi
lib/coq/pretyping/clenv.cmi
lib/coq/pretyping/coercion.cmi
lib/coq/pretyping/detyping.cmi
lib/coq/pretyping/evarconv.cmi
lib/coq/pretyping/evarutil.cmi
lib/coq/pretyping/evd.cmi
lib/coq/pretyping/indrec.cmi
lib/coq/pretyping/inductiveops.cmi
lib/coq/pretyping/matching.cmi
lib/coq/pretyping/namegen.cmi
lib/coq/pretyping/pattern.cmi
lib/coq/pretyping/pretype_errors.cmi
lib/coq/pretyping/pretyping.a
lib/coq/pretyping/pretyping.cma
lib/coq/pretyping/pretyping.cmi
lib/coq/pretyping/pretyping.cmxa
lib/coq/pretyping/rawterm.cmi
lib/coq/pretyping/recordops.cmi
lib/coq/pretyping/reductionops.cmi
lib/coq/pretyping/retyping.cmi
lib/coq/pretyping/tacred.cmi
lib/coq/pretyping/term_dnet.cmi
lib/coq/pretyping/termops.cmi
lib/coq/pretyping/typeclasses.cmi
lib/coq/pretyping/typeclasses_errors.cmi
lib/coq/pretyping/typing.cmi
lib/coq/pretyping/unification.cmi
lib/coq/pretyping/vnorm.cmi
lib/coq/proofs/clenvtac.cmi
lib/coq/proofs/decl_mode.cmi
lib/coq/proofs/evar_refiner.cmi
lib/coq/proofs/logic.cmi
lib/coq/proofs/pfedit.cmi
lib/coq/proofs/proof_trees.cmi
lib/coq/proofs/proof_type.cmi
lib/coq/proofs/proofs.a
lib/coq/proofs/proofs.cma
lib/coq/proofs/proofs.cmxa
lib/coq/proofs/redexpr.cmi
lib/coq/proofs/refiner.cmi
lib/coq/proofs/tacexpr.cmi
lib/coq/proofs/tacmach.cmi
lib/coq/proofs/tactic_debug.cmi
lib/coq/states/initial.coq
lib/coq/tactics/auto.cmi
lib/coq/tactics/autorewrite.cmi
lib/coq/tactics/btermdn.cmi
lib/coq/tactics/class_tactics.cmi
lib/coq/tactics/contradiction.cmi
lib/coq/tactics/decl_interp.cmi
lib/coq/tactics/decl_proof_instr.cmi
lib/coq/tactics/dhyp.cmi
lib/coq/tactics/dn.cmi
lib/coq/tactics/eauto.cmi
lib/coq/tactics/elim.cmi
lib/coq/tactics/elimschemes.cmi
lib/coq/tactics/eqdecide.cmi
lib/coq/tactics/eqschemes.cmi
lib/coq/tactics/equality.cmi
lib/coq/tactics/evar_tactics.cmi
lib/coq/tactics/extraargs.cmi
lib/coq/tactics/extratactics.cmi
lib/coq/tactics/hiddentac.cmi
lib/coq/tactics/hightactics.a
lib/coq/tactics/hightactics.cma
lib/coq/tactics/hightactics.cmxa
lib/coq/tactics/hipattern.cmi
lib/coq/tactics/inv.cmi
lib/coq/tactics/leminv.cmi
lib/coq/tactics/nbtermdn.cmi
lib/coq/tactics/refine.cmi
lib/coq/tactics/rewrite.cmi
lib/coq/tactics/tacinterp.cmi
lib/coq/tactics/tactic_option.cmi
lib/coq/tactics/tacticals.cmi
lib/coq/tactics/tactics.a
lib/coq/tactics/tactics.cma
lib/coq/tactics/tactics.cmi
lib/coq/tactics/tactics.cmxa
lib/coq/tactics/tauto.cmi
lib/coq/tactics/termdn.cmi
lib/coq/theories/Arith/Arith.vo
lib/coq/theories/Arith/Arith_base.vo
lib/coq/theories/Arith/Between.vo
lib/coq/theories/Arith/Bool_nat.vo
lib/coq/theories/Arith/Compare.vo
lib/coq/theories/Arith/Compare_dec.vo
lib/coq/theories/Arith/Div2.vo
lib/coq/theories/Arith/EqNat.vo
lib/coq/theories/Arith/Euclid.vo
lib/coq/theories/Arith/Even.vo
lib/coq/theories/Arith/Factorial.vo
lib/coq/theories/Arith/Gt.vo
lib/coq/theories/Arith/Le.vo
lib/coq/theories/Arith/Lt.vo
lib/coq/theories/Arith/Max.vo
lib/coq/theories/Arith/Min.vo
lib/coq/theories/Arith/MinMax.vo
lib/coq/theories/Arith/Minus.vo
lib/coq/theories/Arith/Mult.vo
lib/coq/theories/Arith/NatOrderedType.vo
lib/coq/theories/Arith/Peano_dec.vo
lib/coq/theories/Arith/Plus.vo
lib/coq/theories/Arith/Wf_nat.vo
lib/coq/theories/Bool/Bool.vo
lib/coq/theories/Bool/BoolEq.vo
lib/coq/theories/Bool/Bvector.vo
lib/coq/theories/Bool/DecBool.vo
lib/coq/theories/Bool/IfProp.vo
lib/coq/theories/Bool/Sumbool.vo
lib/coq/theories/Bool/Zerob.vo
lib/coq/theories/Classes/EquivDec.vo
lib/coq/theories/Classes/Equivalence.vo
lib/coq/theories/Classes/Init.vo
lib/coq/theories/Classes/Morphisms.vo
lib/coq/theories/Classes/Morphisms_Prop.vo
lib/coq/theories/Classes/Morphisms_Relations.vo
lib/coq/theories/Classes/RelationClasses.vo
lib/coq/theories/Classes/RelationPairs.vo
lib/coq/theories/Classes/SetoidClass.vo
lib/coq/theories/Classes/SetoidDec.vo
lib/coq/theories/Classes/SetoidTactics.vo
lib/coq/theories/FSets/FMapAVL.vo
lib/coq/theories/FSets/FMapFacts.vo
lib/coq/theories/FSets/FMapFullAVL.vo
lib/coq/theories/FSets/FMapInterface.vo
lib/coq/theories/FSets/FMapList.vo
lib/coq/theories/FSets/FMapPositive.vo
lib/coq/theories/FSets/FMapWeakList.vo
lib/coq/theories/FSets/FMaps.vo
lib/coq/theories/FSets/FSetAVL.vo
lib/coq/theories/FSets/FSetBridge.vo
lib/coq/theories/FSets/FSetCompat.vo
lib/coq/theories/FSets/FSetDecide.vo
lib/coq/theories/FSets/FSetEqProperties.vo
lib/coq/theories/FSets/FSetFacts.vo
lib/coq/theories/FSets/FSetInterface.vo
lib/coq/theories/FSets/FSetList.vo
lib/coq/theories/FSets/FSetPositive.vo
lib/coq/theories/FSets/FSetProperties.vo
lib/coq/theories/FSets/FSetToFiniteSet.vo
lib/coq/theories/FSets/FSetWeakList.vo
lib/coq/theories/FSets/FSets.vo
lib/coq/theories/Init/Datatypes.vo
lib/coq/theories/Init/Logic.vo
lib/coq/theories/Init/Logic_Type.vo
lib/coq/theories/Init/Notations.vo
lib/coq/theories/Init/Peano.vo
lib/coq/theories/Init/Prelude.vo
lib/coq/theories/Init/Specif.vo
lib/coq/theories/Init/Tactics.vo
lib/coq/theories/Init/Wf.vo
lib/coq/theories/Lists/List.vo
lib/coq/theories/Lists/ListSet.vo
lib/coq/theories/Lists/ListTactics.vo
lib/coq/theories/Lists/SetoidList.vo
lib/coq/theories/Lists/StreamMemo.vo
lib/coq/theories/Lists/Streams.vo
lib/coq/theories/Lists/TheoryList.vo
lib/coq/theories/Logic/Berardi.vo
lib/coq/theories/Logic/ChoiceFacts.vo
lib/coq/theories/Logic/Classical.vo
lib/coq/theories/Logic/ClassicalChoice.vo
lib/coq/theories/Logic/ClassicalDescription.vo
lib/coq/theories/Logic/ClassicalEpsilon.vo
lib/coq/theories/Logic/ClassicalFacts.vo
lib/coq/theories/Logic/ClassicalUniqueChoice.vo
lib/coq/theories/Logic/Classical_Pred_Set.vo
lib/coq/theories/Logic/Classical_Pred_Type.vo
lib/coq/theories/Logic/Classical_Prop.vo
lib/coq/theories/Logic/Classical_Type.vo
lib/coq/theories/Logic/ConstructiveEpsilon.vo
lib/coq/theories/Logic/Decidable.vo
lib/coq/theories/Logic/Description.vo
lib/coq/theories/Logic/Diaconescu.vo
lib/coq/theories/Logic/Epsilon.vo
lib/coq/theories/Logic/Eqdep.vo
lib/coq/theories/Logic/EqdepFacts.vo
lib/coq/theories/Logic/Eqdep_dec.vo
lib/coq/theories/Logic/FunctionalExtensionality.vo
lib/coq/theories/Logic/Hurkens.vo
lib/coq/theories/Logic/IndefiniteDescription.vo
lib/coq/theories/Logic/JMeq.vo
lib/coq/theories/Logic/ProofIrrelevance.vo
lib/coq/theories/Logic/ProofIrrelevanceFacts.vo
lib/coq/theories/Logic/RelationalChoice.vo
lib/coq/theories/Logic/SetIsType.vo
lib/coq/theories/MSets/MSetAVL.vo
lib/coq/theories/MSets/MSetDecide.vo
lib/coq/theories/MSets/MSetEqProperties.vo
lib/coq/theories/MSets/MSetFacts.vo
lib/coq/theories/MSets/MSetInterface.vo
lib/coq/theories/MSets/MSetList.vo
lib/coq/theories/MSets/MSetPositive.vo
lib/coq/theories/MSets/MSetProperties.vo
lib/coq/theories/MSets/MSetToFiniteSet.vo
lib/coq/theories/MSets/MSetWeakList.vo
lib/coq/theories/MSets/MSets.vo
lib/coq/theories/NArith/BinNat.vo
lib/coq/theories/NArith/BinPos.vo
lib/coq/theories/NArith/NArith.vo
lib/coq/theories/NArith/NOrderedType.vo
lib/coq/theories/NArith/Ndec.vo
lib/coq/theories/NArith/Ndigits.vo
lib/coq/theories/NArith/Ndist.vo
lib/coq/theories/NArith/Nminmax.vo
lib/coq/theories/NArith/Nnat.vo
lib/coq/theories/NArith/POrderedType.vo
lib/coq/theories/NArith/Pminmax.vo
lib/coq/theories/NArith/Pnat.vo
lib/coq/theories/Numbers/BigNumPrelude.vo
lib/coq/theories/Numbers/Cyclic/Abstract/CyclicAxioms.vo
lib/coq/theories/Numbers/Cyclic/Abstract/NZCyclic.vo
lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.vo
lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.vo
lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.vo
lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.vo
lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.vo
lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.vo
lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.vo
lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.vo
lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.vo
lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.vo
lib/coq/theories/Numbers/Cyclic/Int31/Cyclic31.vo
lib/coq/theories/Numbers/Cyclic/Int31/Int31.vo
lib/coq/theories/Numbers/Cyclic/Int31/Ring31.vo
lib/coq/theories/Numbers/Cyclic/ZModulo/ZModulo.vo
lib/coq/theories/Numbers/Integer/Abstract/ZAdd.vo
lib/coq/theories/Numbers/Integer/Abstract/ZAddOrder.vo
lib/coq/theories/Numbers/Integer/Abstract/ZAxioms.vo
lib/coq/theories/Numbers/Integer/Abstract/ZBase.vo
lib/coq/theories/Numbers/Integer/Abstract/ZDivEucl.vo
lib/coq/theories/Numbers/Integer/Abstract/ZDivFloor.vo
lib/coq/theories/Numbers/Integer/Abstract/ZDivTrunc.vo
lib/coq/theories/Numbers/Integer/Abstract/ZLt.vo
lib/coq/theories/Numbers/Integer/Abstract/ZMul.vo
lib/coq/theories/Numbers/Integer/Abstract/ZMulOrder.vo
lib/coq/theories/Numbers/Integer/Abstract/ZProperties.vo
lib/coq/theories/Numbers/Integer/Abstract/ZSgnAbs.vo
lib/coq/theories/Numbers/Integer/BigZ/BigZ.vo
lib/coq/theories/Numbers/Integer/BigZ/ZMake.vo
lib/coq/theories/Numbers/Integer/Binary/ZBinary.vo
lib/coq/theories/Numbers/Integer/NatPairs/ZNatPairs.vo
lib/coq/theories/Numbers/Integer/SpecViaZ/ZSig.vo
lib/coq/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.vo
lib/coq/theories/Numbers/NaryFunctions.vo
lib/coq/theories/Numbers/NatInt/NZAdd.vo
lib/coq/theories/Numbers/NatInt/NZAddOrder.vo
lib/coq/theories/Numbers/NatInt/NZAxioms.vo
lib/coq/theories/Numbers/NatInt/NZBase.vo
lib/coq/theories/Numbers/NatInt/NZDiv.vo
lib/coq/theories/Numbers/NatInt/NZDomain.vo
lib/coq/theories/Numbers/NatInt/NZMul.vo
lib/coq/theories/Numbers/NatInt/NZMulOrder.vo
lib/coq/theories/Numbers/NatInt/NZOrder.vo
lib/coq/theories/Numbers/NatInt/NZProperties.vo
lib/coq/theories/Numbers/Natural/Abstract/NAdd.vo
lib/coq/theories/Numbers/Natural/Abstract/NAddOrder.vo
lib/coq/theories/Numbers/Natural/Abstract/NAxioms.vo
lib/coq/theories/Numbers/Natural/Abstract/NBase.vo
lib/coq/theories/Numbers/Natural/Abstract/NDefOps.vo
lib/coq/theories/Numbers/Natural/Abstract/NDiv.vo
lib/coq/theories/Numbers/Natural/Abstract/NIso.vo
lib/coq/theories/Numbers/Natural/Abstract/NMulOrder.vo
lib/coq/theories/Numbers/Natural/Abstract/NOrder.vo
lib/coq/theories/Numbers/Natural/Abstract/NProperties.vo
lib/coq/theories/Numbers/Natural/Abstract/NStrongRec.vo
lib/coq/theories/Numbers/Natural/Abstract/NSub.vo
lib/coq/theories/Numbers/Natural/BigN/BigN.vo
lib/coq/theories/Numbers/Natural/BigN/NMake.vo
lib/coq/theories/Numbers/Natural/BigN/NMake_gen.vo
lib/coq/theories/Numbers/Natural/BigN/Nbasic.vo
lib/coq/theories/Numbers/Natural/Binary/NBinary.vo
lib/coq/theories/Numbers/Natural/Peano/NPeano.vo
lib/coq/theories/Numbers/Natural/SpecViaZ/NSig.vo
lib/coq/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.vo
lib/coq/theories/Numbers/NumPrelude.vo
lib/coq/theories/Numbers/Rational/BigQ/BigQ.vo
lib/coq/theories/Numbers/Rational/BigQ/QMake.vo
lib/coq/theories/Numbers/Rational/SpecViaQ/QSig.vo
lib/coq/theories/Program/Basics.vo
lib/coq/theories/Program/Combinators.vo
lib/coq/theories/Program/Equality.vo
lib/coq/theories/Program/Program.vo
lib/coq/theories/Program/Subset.vo
lib/coq/theories/Program/Syntax.vo
lib/coq/theories/Program/Tactics.vo
lib/coq/theories/Program/Utils.vo
lib/coq/theories/Program/Wf.vo
lib/coq/theories/QArith/QArith.vo
lib/coq/theories/QArith/QArith_base.vo
lib/coq/theories/QArith/QOrderedType.vo
lib/coq/theories/QArith/Qabs.vo
lib/coq/theories/QArith/Qcanon.vo
lib/coq/theories/QArith/Qfield.vo
lib/coq/theories/QArith/Qminmax.vo
lib/coq/theories/QArith/Qpower.vo
lib/coq/theories/QArith/Qreals.vo
lib/coq/theories/QArith/Qreduction.vo
lib/coq/theories/QArith/Qring.vo
lib/coq/theories/QArith/Qround.vo
lib/coq/theories/Reals/Alembert.vo
lib/coq/theories/Reals/AltSeries.vo
lib/coq/theories/Reals/ArithProp.vo
lib/coq/theories/Reals/Binomial.vo
lib/coq/theories/Reals/Cauchy_prod.vo
lib/coq/theories/Reals/Cos_plus.vo
lib/coq/theories/Reals/Cos_rel.vo
lib/coq/theories/Reals/DiscrR.vo
lib/coq/theories/Reals/Exp_prop.vo
lib/coq/theories/Reals/Integration.vo
lib/coq/theories/Reals/LegacyRfield.vo
lib/coq/theories/Reals/MVT.vo
lib/coq/theories/Reals/NewtonInt.vo
lib/coq/theories/Reals/PSeries_reg.vo
lib/coq/theories/Reals/PartSum.vo
lib/coq/theories/Reals/RIneq.vo
lib/coq/theories/Reals/RList.vo
lib/coq/theories/Reals/ROrderedType.vo
lib/coq/theories/Reals/R_Ifp.vo
lib/coq/theories/Reals/R_sqr.vo
lib/coq/theories/Reals/R_sqrt.vo
lib/coq/theories/Reals/Ranalysis.vo
lib/coq/theories/Reals/Ranalysis1.vo
lib/coq/theories/Reals/Ranalysis2.vo
lib/coq/theories/Reals/Ranalysis3.vo
lib/coq/theories/Reals/Ranalysis4.vo
lib/coq/theories/Reals/Raxioms.vo
lib/coq/theories/Reals/Rbase.vo
lib/coq/theories/Reals/Rbasic_fun.vo
lib/coq/theories/Reals/Rcomplete.vo
lib/coq/theories/Reals/Rdefinitions.vo
lib/coq/theories/Reals/Rderiv.vo
lib/coq/theories/Reals/Reals.vo
lib/coq/theories/Reals/Rfunctions.vo
lib/coq/theories/Reals/Rgeom.vo
lib/coq/theories/Reals/RiemannInt.vo
lib/coq/theories/Reals/RiemannInt_SF.vo
lib/coq/theories/Reals/Rlimit.vo
lib/coq/theories/Reals/Rlogic.vo
lib/coq/theories/Reals/Rminmax.vo
lib/coq/theories/Reals/Rpow_def.vo
lib/coq/theories/Reals/Rpower.vo
lib/coq/theories/Reals/Rprod.vo
lib/coq/theories/Reals/Rseries.vo
lib/coq/theories/Reals/Rsigma.vo
lib/coq/theories/Reals/Rsqrt_def.vo
lib/coq/theories/Reals/Rtopology.vo
lib/coq/theories/Reals/Rtrigo.vo
lib/coq/theories/Reals/Rtrigo_alt.vo
lib/coq/theories/Reals/Rtrigo_calc.vo
lib/coq/theories/Reals/Rtrigo_def.vo
lib/coq/theories/Reals/Rtrigo_fun.vo
lib/coq/theories/Reals/Rtrigo_reg.vo
lib/coq/theories/Reals/SeqProp.vo
lib/coq/theories/Reals/SeqSeries.vo
lib/coq/theories/Reals/SplitAbsolu.vo
lib/coq/theories/Reals/SplitRmult.vo
lib/coq/theories/Reals/Sqrt_reg.vo
lib/coq/theories/Relations/Operators_Properties.vo
lib/coq/theories/Relations/Relation_Definitions.vo
lib/coq/theories/Relations/Relation_Operators.vo
lib/coq/theories/Relations/Relations.vo
lib/coq/theories/Setoids/Setoid.vo
lib/coq/theories/Sets/Classical_sets.vo
lib/coq/theories/Sets/Constructive_sets.vo
lib/coq/theories/Sets/Cpo.vo
lib/coq/theories/Sets/Ensembles.vo
lib/coq/theories/Sets/Finite_sets.vo
lib/coq/theories/Sets/Finite_sets_facts.vo
lib/coq/theories/Sets/Image.vo
lib/coq/theories/Sets/Infinite_sets.vo
lib/coq/theories/Sets/Integers.vo
lib/coq/theories/Sets/Multiset.vo
lib/coq/theories/Sets/Partial_Order.vo
lib/coq/theories/Sets/Permut.vo
lib/coq/theories/Sets/Powerset.vo
lib/coq/theories/Sets/Powerset_Classical_facts.vo
lib/coq/theories/Sets/Powerset_facts.vo
lib/coq/theories/Sets/Relations_1.vo
lib/coq/theories/Sets/Relations_1_facts.vo
lib/coq/theories/Sets/Relations_2.vo
lib/coq/theories/Sets/Relations_2_facts.vo
lib/coq/theories/Sets/Relations_3.vo
lib/coq/theories/Sets/Relations_3_facts.vo
lib/coq/theories/Sets/Uniset.vo
lib/coq/theories/Sorting/Heap.vo
lib/coq/theories/Sorting/Mergesort.vo
lib/coq/theories/Sorting/PermutEq.vo
lib/coq/theories/Sorting/PermutSetoid.vo
lib/coq/theories/Sorting/Permutation.vo
lib/coq/theories/Sorting/Sorted.vo
lib/coq/theories/Sorting/Sorting.vo
lib/coq/theories/Strings/Ascii.vo
lib/coq/theories/Strings/String.vo
lib/coq/theories/Structures/DecidableType.vo
lib/coq/theories/Structures/DecidableTypeEx.vo
lib/coq/theories/Structures/Equalities.vo
lib/coq/theories/Structures/EqualitiesFacts.vo
lib/coq/theories/Structures/GenericMinMax.vo
lib/coq/theories/Structures/OrderedType.vo
lib/coq/theories/Structures/OrderedTypeAlt.vo
lib/coq/theories/Structures/OrderedTypeEx.vo
lib/coq/theories/Structures/Orders.vo
lib/coq/theories/Structures/OrdersAlt.vo
lib/coq/theories/Structures/OrdersEx.vo
lib/coq/theories/Structures/OrdersFacts.vo
lib/coq/theories/Structures/OrdersLists.vo
lib/coq/theories/Structures/OrdersTac.vo
lib/coq/theories/Unicode/Utf8.vo
lib/coq/theories/Unicode/Utf8_core.vo
lib/coq/theories/Wellfounded/Disjoint_Union.vo
lib/coq/theories/Wellfounded/Inclusion.vo
lib/coq/theories/Wellfounded/Inverse_Image.vo
lib/coq/theories/Wellfounded/Lexicographic_Exponentiation.vo
lib/coq/theories/Wellfounded/Lexicographic_Product.vo
lib/coq/theories/Wellfounded/Transitive_Closure.vo
lib/coq/theories/Wellfounded/Union.vo
lib/coq/theories/Wellfounded/Well_Ordering.vo
lib/coq/theories/Wellfounded/Wellfounded.vo
lib/coq/theories/ZArith/BinInt.vo
lib/coq/theories/ZArith/Int.vo
lib/coq/theories/ZArith/Wf_Z.vo
lib/coq/theories/ZArith/ZArith.vo
lib/coq/theories/ZArith/ZArith_base.vo
lib/coq/theories/ZArith/ZArith_dec.vo
lib/coq/theories/ZArith/ZOdiv.vo
lib/coq/theories/ZArith/ZOdiv_def.vo
lib/coq/theories/ZArith/ZOrderedType.vo
lib/coq/theories/ZArith/Zabs.vo
lib/coq/theories/ZArith/Zbool.vo
lib/coq/theories/ZArith/Zcompare.vo
lib/coq/theories/ZArith/Zcomplements.vo
lib/coq/theories/ZArith/Zdigits.vo
lib/coq/theories/ZArith/Zdiv.vo
lib/coq/theories/ZArith/Zeven.vo
lib/coq/theories/ZArith/Zgcd_alt.vo
lib/coq/theories/ZArith/Zhints.vo
lib/coq/theories/ZArith/Zlogarithm.vo
lib/coq/theories/ZArith/Zmax.vo
lib/coq/theories/ZArith/Zmin.vo
lib/coq/theories/ZArith/Zminmax.vo
lib/coq/theories/ZArith/Zmisc.vo
lib/coq/theories/ZArith/Znat.vo
lib/coq/theories/ZArith/Znumtheory.vo
lib/coq/theories/ZArith/Zorder.vo
lib/coq/theories/ZArith/Zpow_def.vo
lib/coq/theories/ZArith/Zpow_facts.vo
lib/coq/theories/ZArith/Zpower.vo
lib/coq/theories/ZArith/Zsqrt.vo
lib/coq/theories/ZArith/Zwf.vo
lib/coq/theories/ZArith/auxiliary.vo
lib/coq/tools/coqdoc/coqdoc.css
lib/coq/tools/coqdoc/coqdoc.sty
lib/coq/toplevel/auto_ind_decl.cmi
lib/coq/toplevel/autoinstance.cmi
lib/coq/toplevel/cerrors.cmi
lib/coq/toplevel/class.cmi
lib/coq/toplevel/classes.cmi
lib/coq/toplevel/command.cmi
lib/coq/toplevel/coqinit.cmi
lib/coq/toplevel/coqtop.cmi
lib/coq/toplevel/discharge.cmi
lib/coq/toplevel/himsg.cmi
lib/coq/toplevel/ind_tables.cmi
lib/coq/toplevel/indschemes.cmi
lib/coq/toplevel/lemmas.cmi
lib/coq/toplevel/libtypes.cmi
lib/coq/toplevel/metasyntax.cmi
lib/coq/toplevel/mltop.cmi
lib/coq/toplevel/record.cmi
lib/coq/toplevel/search.cmi
lib/coq/toplevel/toplevel.a
lib/coq/toplevel/toplevel.cma
lib/coq/toplevel/toplevel.cmi
lib/coq/toplevel/toplevel.cmxa
lib/coq/toplevel/usage.cmi
lib/coq/toplevel/vernac.cmi
lib/coq/toplevel/vernacentries.cmi
lib/coq/toplevel/vernacexpr.cmi
lib/coq/toplevel/vernacinterp.cmi
lib/coq/toplevel/whelp.cmi
man/man1/coq-tex.1
man/man1/coq_makefile.1
man/man1/coqc.1
man/man1/coqchk.1
man/man1/coqdep.1
man/man1/coqdoc.1
man/man1/coqide.1
man/man1/coqmktop.1
man/man1/coqtop.1
man/man1/coqtop.byte.1
man/man1/coqwc.1
man/man1/gallina.1
share/emacs/site-lisp/coq-db.el
share/emacs/site-lisp/coq-font-lock.el
share/emacs/site-lisp/coq-inferior.el
share/emacs/site-lisp/coq-syntax.el
share/emacs/site-lisp/coq.el
share/emacs/site-lisp/coqdoc.sty
@pkgdir lib/coq/user-contrib
Reference in a new issue View git blame Copy permalink