| Index | index by Group | index by Distribution | index by Vendor | index by creation date | index by Name | Mirrors | Help | Search |
| Name: coq | Distribution: Fedora Project |
| Version: 8.3pl2 | Vendor: Fedora Project |
| Release: 2.fc15 | Build date: Wed Jun 15 21:51:38 2011 |
| Group: Applications/Engineering | Build host: x86-04.phx2.fedoraproject.org |
| Size: 136454873 | Source RPM: coq-8.3pl2-2.fc15.src.rpm |
| Packager: Fedora Project | |
| Url: http://coq.inria.fr/ | |
| Summary: Proof management system | |
Coq is a formal proof management system. It allows for the development of theorems through first order logic that are mechanically checked by the machine. Sets of definitions and theorems can be saved as compiled modules and loaded into the system. This package provides the main Coq binary without an optional IDE, Coqide.
LGPLv2
* Wed Jun 15 2011 Jerry James <loganjerry@gmail.com> - 8.3pl2-2
- Remove workaround for bad documentation link in 8.3pl1, fixed in 8.3pl2
- Revert change in 8.3pl1-1 to split arch-specific stuff from noarch stuff.
Coq tactics are written in ocaml, which compiles to arch-specific files,
and those files are stored in the same place as the noarch proof files.
- Move tutorial code into main package; it is small and we can then leave
all the rest of the documentation as noarch
* Tue Apr 26 2011 Jerry James <loganjerry@gmail.com> - 8.3pl2-1
- New upstream release
- Change the list of supported arches to match the ocaml list, except for
ppc64, which is missing hevea
* Mon Apr 04 2011 Jerry James <loganjerry@gmail.com> - 8.3pl1-2
- Change the mime type to application/x-coq, and inherit from text/plain
(bz 530254)
* Thu Mar 31 2011 Jerry James <loganjerry@gmail.com> - 8.3pl1-1
- New upstream release
- Drop BuildRoot tag and clean section
- Drop all patches (all merged or otherwise fixed upstream)
- Comply with latest Ocaml packaging specs
- Identify xdg-open as the default web browser
- Comply with the emacs packaging guidelines, and build an XEmacs package
- The -doc and -emacs* subpackages are now noarch
- Workaround bug 691913
- Drop PostScript documentation; it's identical to PDF documentation
- Deal with arch-specific files in /usr/share; install everything to libdir,
then move the noarch stuff to datadir, but leave symlinks behind
- Add a new mime type application/x-coqide and use it in the desktop file
- Add post and postun scripts
* Tue Feb 08 2011 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 8.2pl1-2
- Rebuilt for https://fedoraproject.org/wiki/Fedora_15_Mass_Rebuild
* Wed Aug 05 2009 Alan Dunn <amdunn@gmail.com> - 8.2pl1-1
- New upstream release
- Eliminated modification of tar_base_name that occurred for only version 8.2
- Added reference to bugzilla bug for ppc64 ExcludeArch
- HTML form of documentation seems to no longer be distributed -> must generate
Decided for consistency to generate all documentation
- Additional file for iconv - documentation license file
- Changed tutorial directory name, now also using bundled version
of tutorial
* Fri Jul 24 2009 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 8.2-2
- Rebuilt for https://fedoraproject.org/wiki/Fedora_12_Mass_Rebuild
* Thu Jun 18 2009 Alan Dunn <amdunn@gmail.com> - 8.2-1
- New upstream release
- Seems documentation license has changed or wasn't explicitly stated
before, fixed (is ok Fedora license)
- Added versioning to documentation
- Removed special OCaml, TeX logic for Fedora < 9 (no longer relevant)
- Dropped makefile patch for compiling grammar.cma (fixed in Coq 8.2)
- Dropped cmxa-install patch (fixed in Coq 8.2)
- Changed makefile-strip patch and name (not yet fixed upstream...)
- Changed check.patch -> coq-check-(version).patch, slightly changed
for 8.2 (not yet fixed upstream...)
- Dropped parser-renaming makefile-parser.patch, parser-man.patch
(fixed in Coq 8.2)
- Dropped coq-lablgtk-2.12.patch (fixed in Coq 8.2)
- Changed way source (.v) files are installed
- Stopped addition of other icon file (icon fixed in Coq 8.2)
- Bytecode executables are now "clean" (not build with custom -> don't
need to configure prelink around these)
- define -> global
- Added ExcludeArch sparc64
* Wed Jun 17 2009 S390x secondary arch maintainer <fedora-s390x@lists.fedoraproject.org> 8.1pl4-3.1
- ExcludeArch s390, s390x as we don't have OCaml on those archs
* Wed Mar 04 2009 Alan Dunn <amdunn@gmail.com> - 8.1pl4-3
- Minor change to cmxa-install patch instruction
- Fixed to work with lablgtk 2.12
* Tue Feb 24 2009 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 8.1pl4-2
- Rebuilt for https://fedoraproject.org/wiki/Fedora_11_Mass_Rebuild
* Fri Dec 05 2008 Richard W.M. Jones <rjones@redhat.com> - 8.1pl4-1
- New upstream version 8.1pl4.
- Attempt to rebuild against OCaml 3.11.0.
- Run make with VERBOSE=1 so we can see the actual commands.
- Pass -camlp5dir to configure so it uses camlp5 (overriding existence
of camlp4 if it happens to be installed).
* Wed Oct 22 2008 Alan Dunn <amdunn@gmail.com> 8.1pl3-5
- Added Coq .v files into the main package at user request.
* Tue Sep 09 2008 Alan Dunn <amdunn@gmail.com> 8.1pl3-4
- Added creation of prelink blacklist for any bytecode files.
- Fixed execstack status for binaries.
* Tue Aug 05 2008 Alan Dunn <amdunn@gmail.com> 8.1pl3-3
- Changed parser to coq-parser to avoid name conflict with
coda-client.
- Made make process noisy again.
* Sun Jul 20 2008 Alan Dunn <amdunn@gmail.com> 8.1pl3-2.1
- Minor bump for Fedora 8 to bring it into line with the rest.
* Thu Jul 17 2008 Alan Dunn <amdunn@gmail.com> 8.1pl3-2
- Added check for Fedora distribution number to allow for Fedora 8 release.
* Sat Jun 14 2008 Alan Dunn <amdunn@gmail.com> 8.1pl3-1
- Initial Fedora RPM version.
/usr/bin/coq-tex /usr/bin/coq_makefile /usr/bin/coqc /usr/bin/coqchk /usr/bin/coqchk.opt /usr/bin/coqdep /usr/bin/coqdoc /usr/bin/coqmktop /usr/bin/coqtop /usr/bin/coqtop.byte /usr/bin/coqtop.opt /usr/bin/coqwc /usr/bin/gallina /usr/lib64/coq /usr/lib64/coq/RecTutorial /usr/lib64/coq/RecTutorial/RecTutorial /usr/lib64/coq/RecTutorial/RecTutorial.v /usr/lib64/coq/config /usr/lib64/coq/config/coq_config.cmi /usr/lib64/coq/config/coq_config.cmo /usr/lib64/coq/config/coq_config.cmx /usr/lib64/coq/config/coq_config.o /usr/lib64/coq/dllcoqrun.so /usr/lib64/coq/interp /usr/lib64/coq/interp/constrextern.cmi /usr/lib64/coq/interp/constrintern.cmi /usr/lib64/coq/interp/coqlib.cmi /usr/lib64/coq/interp/dumpglob.cmi /usr/lib64/coq/interp/genarg.cmi /usr/lib64/coq/interp/implicit_quantifiers.cmi /usr/lib64/coq/interp/interp.cma /usr/lib64/coq/interp/modintern.cmi /usr/lib64/coq/interp/notation.cmi /usr/lib64/coq/interp/ppextend.cmi /usr/lib64/coq/interp/reserve.cmi /usr/lib64/coq/interp/smartlocate.cmi /usr/lib64/coq/interp/syntax_def.cmi /usr/lib64/coq/interp/topconstr.cmi /usr/lib64/coq/kernel /usr/lib64/coq/kernel/cbytecodes.cmi /usr/lib64/coq/kernel/cbytegen.cmi /usr/lib64/coq/kernel/cemitcodes.cmi /usr/lib64/coq/kernel/closure.cmi /usr/lib64/coq/kernel/conv_oracle.cmi /usr/lib64/coq/kernel/cooking.cmi /usr/lib64/coq/kernel/copcodes.cmi /usr/lib64/coq/kernel/csymtable.cmi /usr/lib64/coq/kernel/declarations.cmi /usr/lib64/coq/kernel/entries.cmi /usr/lib64/coq/kernel/environ.cmi /usr/lib64/coq/kernel/esubst.cmi /usr/lib64/coq/kernel/indtypes.cmi /usr/lib64/coq/kernel/inductive.cmi /usr/lib64/coq/kernel/kernel.cma /usr/lib64/coq/kernel/mod_subst.cmi /usr/lib64/coq/kernel/mod_typing.cmi /usr/lib64/coq/kernel/modops.cmi /usr/lib64/coq/kernel/names.cmi /usr/lib64/coq/kernel/pre_env.cmi /usr/lib64/coq/kernel/reduction.cmi /usr/lib64/coq/kernel/retroknowledge.cmi /usr/lib64/coq/kernel/safe_typing.cmi /usr/lib64/coq/kernel/sign.cmi /usr/lib64/coq/kernel/subtyping.cmi /usr/lib64/coq/kernel/term.cmi /usr/lib64/coq/kernel/term_typing.cmi /usr/lib64/coq/kernel/type_errors.cmi /usr/lib64/coq/kernel/typeops.cmi /usr/lib64/coq/kernel/univ.cmi /usr/lib64/coq/kernel/vconv.cmi /usr/lib64/coq/kernel/vm.cmi /usr/lib64/coq/lib /usr/lib64/coq/lib/bigint.cmi /usr/lib64/coq/lib/bstack.cmi /usr/lib64/coq/lib/compat.cmi /usr/lib64/coq/lib/dnet.cmi /usr/lib64/coq/lib/dyn.cmi /usr/lib64/coq/lib/edit.cmi /usr/lib64/coq/lib/envars.cmi /usr/lib64/coq/lib/explore.cmi /usr/lib64/coq/lib/flags.cmi /usr/lib64/coq/lib/fmap.cmi /usr/lib64/coq/lib/fset.cmi /usr/lib64/coq/lib/gmap.cmi /usr/lib64/coq/lib/gmapl.cmi /usr/lib64/coq/lib/gset.cmi /usr/lib64/coq/lib/hashcons.cmi /usr/lib64/coq/lib/heap.cmi /usr/lib64/coq/lib/lib.cma /usr/lib64/coq/lib/option.cmi /usr/lib64/coq/lib/pp.cmi /usr/lib64/coq/lib/pp_control.cmi /usr/lib64/coq/lib/predicate.cmi /usr/lib64/coq/lib/profile.cmi /usr/lib64/coq/lib/rtree.cmi /usr/lib64/coq/lib/segmenttree.cmi /usr/lib64/coq/lib/system.cmi /usr/lib64/coq/lib/tlm.cmi /usr/lib64/coq/lib/tries.cmi /usr/lib64/coq/lib/unicodetable.cmi /usr/lib64/coq/lib/util.cmi /usr/lib64/coq/library /usr/lib64/coq/library/decl_kinds.cmi /usr/lib64/coq/library/declare.cmi /usr/lib64/coq/library/declaremods.cmi /usr/lib64/coq/library/decls.cmi /usr/lib64/coq/library/dischargedhypsmap.cmi /usr/lib64/coq/library/global.cmi /usr/lib64/coq/library/goptions.cmi /usr/lib64/coq/library/heads.cmi /usr/lib64/coq/library/impargs.cmi /usr/lib64/coq/library/lib.cmi /usr/lib64/coq/library/libnames.cmi /usr/lib64/coq/library/libobject.cmi /usr/lib64/coq/library/library.cma /usr/lib64/coq/library/library.cmi /usr/lib64/coq/library/nameops.cmi /usr/lib64/coq/library/nametab.cmi /usr/lib64/coq/library/states.cmi /usr/lib64/coq/library/summary.cmi /usr/lib64/coq/parsing /usr/lib64/coq/parsing/egrammar.cmi /usr/lib64/coq/parsing/extend.cmi /usr/lib64/coq/parsing/extrawit.cmi /usr/lib64/coq/parsing/g_constr.cmi /usr/lib64/coq/parsing/g_decl_mode.cmi /usr/lib64/coq/parsing/g_ltac.cmi /usr/lib64/coq/parsing/g_prim.cmi /usr/lib64/coq/parsing/g_proofs.cmi /usr/lib64/coq/parsing/g_tactic.cmi /usr/lib64/coq/parsing/g_vernac.cmi /usr/lib64/coq/parsing/g_xml.cmi /usr/lib64/coq/parsing/grammar.cma /usr/lib64/coq/parsing/highparsing.cma /usr/lib64/coq/parsing/lexer.cmi /usr/lib64/coq/parsing/parsing.cma /usr/lib64/coq/parsing/pcoq.cmi /usr/lib64/coq/parsing/ppconstr.cmi /usr/lib64/coq/parsing/ppdecl_proof.cmi /usr/lib64/coq/parsing/pptactic.cmi /usr/lib64/coq/parsing/ppvernac.cmi /usr/lib64/coq/parsing/prettyp.cmi /usr/lib64/coq/parsing/printer.cmi /usr/lib64/coq/parsing/printmod.cmi /usr/lib64/coq/parsing/tactic_printer.cmi /usr/lib64/coq/plugins /usr/lib64/coq/plugins/cc /usr/lib64/coq/plugins/cc/cc_plugin.cma /usr/lib64/coq/plugins/cc/cc_plugin.cmxs /usr/lib64/coq/plugins/cc/cc_plugin_mod.cmi /usr/lib64/coq/plugins/cc/ccalgo.cmi /usr/lib64/coq/plugins/cc/ccproof.cmi /usr/lib64/coq/plugins/cc/cctac.cmi /usr/lib64/coq/plugins/cc/g_congruence.cmi /usr/lib64/coq/plugins/dp /usr/lib64/coq/plugins/dp/Dp.vo /usr/lib64/coq/plugins/dp/dp.cmi /usr/lib64/coq/plugins/dp/dp_plugin.cma /usr/lib64/coq/plugins/dp/dp_plugin.cmxs /usr/lib64/coq/plugins/dp/dp_plugin_mod.cmi /usr/lib64/coq/plugins/dp/dp_why.cmi /usr/lib64/coq/plugins/dp/dp_zenon.cmi /usr/lib64/coq/plugins/dp/fol.cmi /usr/lib64/coq/plugins/dp/g_dp.cmi /usr/lib64/coq/plugins/extraction /usr/lib64/coq/plugins/extraction/ExtrOcamlBasic.vo /usr/lib64/coq/plugins/extraction/ExtrOcamlBigIntConv.vo /usr/lib64/coq/plugins/extraction/ExtrOcamlIntConv.vo /usr/lib64/coq/plugins/extraction/ExtrOcamlNatBigInt.vo /usr/lib64/coq/plugins/extraction/ExtrOcamlNatInt.vo /usr/lib64/coq/plugins/extraction/ExtrOcamlString.vo /usr/lib64/coq/plugins/extraction/ExtrOcamlZBigInt.vo /usr/lib64/coq/plugins/extraction/ExtrOcamlZInt.vo /usr/lib64/coq/plugins/extraction/common.cmi /usr/lib64/coq/plugins/extraction/extract_env.cmi /usr/lib64/coq/plugins/extraction/extraction.cmi /usr/lib64/coq/plugins/extraction/extraction_plugin.cma /usr/lib64/coq/plugins/extraction/extraction_plugin.cmxs /usr/lib64/coq/plugins/extraction/extraction_plugin_mod.cmi /usr/lib64/coq/plugins/extraction/g_extraction.cmi /usr/lib64/coq/plugins/extraction/haskell.cmi /usr/lib64/coq/plugins/extraction/miniml.cmi /usr/lib64/coq/plugins/extraction/mlutil.cmi /usr/lib64/coq/plugins/extraction/modutil.cmi /usr/lib64/coq/plugins/extraction/ocaml.cmi /usr/lib64/coq/plugins/extraction/scheme.cmi /usr/lib64/coq/plugins/extraction/table.cmi /usr/lib64/coq/plugins/field /usr/lib64/coq/plugins/field/LegacyField.vo /usr/lib64/coq/plugins/field/LegacyField_Compl.vo /usr/lib64/coq/plugins/field/LegacyField_Tactic.vo /usr/lib64/coq/plugins/field/LegacyField_Theory.vo /usr/lib64/coq/plugins/field/field.cmi /usr/lib64/coq/plugins/field/field_plugin.cma /usr/lib64/coq/plugins/field/field_plugin.cmxs /usr/lib64/coq/plugins/field/field_plugin_mod.cmi /usr/lib64/coq/plugins/firstorder /usr/lib64/coq/plugins/firstorder/formula.cmi /usr/lib64/coq/plugins/firstorder/g_ground.cmi /usr/lib64/coq/plugins/firstorder/ground.cmi /usr/lib64/coq/plugins/firstorder/ground_plugin.cma /usr/lib64/coq/plugins/firstorder/ground_plugin.cmxs /usr/lib64/coq/plugins/firstorder/ground_plugin_mod.cmi /usr/lib64/coq/plugins/firstorder/instances.cmi /usr/lib64/coq/plugins/firstorder/rules.cmi /usr/lib64/coq/plugins/firstorder/sequent.cmi /usr/lib64/coq/plugins/firstorder/unify.cmi /usr/lib64/coq/plugins/fourier /usr/lib64/coq/plugins/fourier/Fourier.vo /usr/lib64/coq/plugins/fourier/Fourier_util.vo /usr/lib64/coq/plugins/fourier/fourier.cmi /usr/lib64/coq/plugins/fourier/fourierR.cmi /usr/lib64/coq/plugins/fourier/fourier_plugin.cma /usr/lib64/coq/plugins/fourier/fourier_plugin.cmxs /usr/lib64/coq/plugins/fourier/fourier_plugin_mod.cmi /usr/lib64/coq/plugins/fourier/g_fourier.cmi /usr/lib64/coq/plugins/funind /usr/lib64/coq/plugins/funind/Recdef.vo /usr/lib64/coq/plugins/funind/functional_principles_proofs.cmi /usr/lib64/coq/plugins/funind/functional_principles_types.cmi /usr/lib64/coq/plugins/funind/g_indfun.cmi /usr/lib64/coq/plugins/funind/indfun.cmi /usr/lib64/coq/plugins/funind/indfun_common.cmi /usr/lib64/coq/plugins/funind/invfun.cmi /usr/lib64/coq/plugins/funind/merge.cmi /usr/lib64/coq/plugins/funind/rawterm_to_relation.cmi /usr/lib64/coq/plugins/funind/rawtermops.cmi /usr/lib64/coq/plugins/funind/recdef.cmi /usr/lib64/coq/plugins/funind/recdef_plugin.cma /usr/lib64/coq/plugins/funind/recdef_plugin.cmxs /usr/lib64/coq/plugins/funind/recdef_plugin_mod.cmi /usr/lib64/coq/plugins/micromega /usr/lib64/coq/plugins/micromega/CheckerMaker.vo /usr/lib64/coq/plugins/micromega/Env.vo /usr/lib64/coq/plugins/micromega/EnvRing.vo /usr/lib64/coq/plugins/micromega/OrderedRing.vo /usr/lib64/coq/plugins/micromega/Psatz.vo /usr/lib64/coq/plugins/micromega/QMicromega.vo /usr/lib64/coq/plugins/micromega/RMicromega.vo /usr/lib64/coq/plugins/micromega/Refl.vo /usr/lib64/coq/plugins/micromega/RingMicromega.vo /usr/lib64/coq/plugins/micromega/Tauto.vo /usr/lib64/coq/plugins/micromega/VarMap.vo /usr/lib64/coq/plugins/micromega/ZCoeff.vo /usr/lib64/coq/plugins/micromega/ZMicromega.vo /usr/lib64/coq/plugins/micromega/certificate.cmi /usr/lib64/coq/plugins/micromega/coq_micromega.cmi /usr/lib64/coq/plugins/micromega/csdpcert /usr/lib64/coq/plugins/micromega/g_micromega.cmi /usr/lib64/coq/plugins/micromega/mfourier.cmi /usr/lib64/coq/plugins/micromega/micromega.cmi /usr/lib64/coq/plugins/micromega/micromega_plugin.cma /usr/lib64/coq/plugins/micromega/micromega_plugin.cmxs /usr/lib64/coq/plugins/micromega/micromega_plugin_mod.cmi /usr/lib64/coq/plugins/micromega/mutils.cmi /usr/lib64/coq/plugins/micromega/persistent_cache.cmi /usr/lib64/coq/plugins/micromega/sos_lib.cmi /usr/lib64/coq/plugins/micromega/sos_types.cmi /usr/lib64/coq/plugins/nsatz /usr/lib64/coq/plugins/nsatz/Nsatz.vo /usr/lib64/coq/plugins/nsatz/ideal.cmi /usr/lib64/coq/plugins/nsatz/nsatz.cmi /usr/lib64/coq/plugins/nsatz/nsatz_plugin.cma /usr/lib64/coq/plugins/nsatz/nsatz_plugin.cmxs /usr/lib64/coq/plugins/nsatz/nsatz_plugin_mod.cmi /usr/lib64/coq/plugins/nsatz/polynom.cmi /usr/lib64/coq/plugins/nsatz/utile.cmi /usr/lib64/coq/plugins/omega /usr/lib64/coq/plugins/omega/Omega.vo /usr/lib64/coq/plugins/omega/OmegaLemmas.vo /usr/lib64/coq/plugins/omega/OmegaPlugin.vo /usr/lib64/coq/plugins/omega/PreOmega.vo /usr/lib64/coq/plugins/omega/coq_omega.cmi /usr/lib64/coq/plugins/omega/g_omega.cmi /usr/lib64/coq/plugins/omega/omega.cmi /usr/lib64/coq/plugins/omega/omega_plugin.cma /usr/lib64/coq/plugins/omega/omega_plugin.cmxs /usr/lib64/coq/plugins/omega/omega_plugin_mod.cmi /usr/lib64/coq/plugins/quote /usr/lib64/coq/plugins/quote/Quote.vo /usr/lib64/coq/plugins/quote/g_quote.cmi /usr/lib64/coq/plugins/quote/quote.cmi /usr/lib64/coq/plugins/quote/quote_plugin.cma /usr/lib64/coq/plugins/quote/quote_plugin.cmxs /usr/lib64/coq/plugins/quote/quote_plugin_mod.cmi /usr/lib64/coq/plugins/ring /usr/lib64/coq/plugins/ring/LegacyArithRing.vo /usr/lib64/coq/plugins/ring/LegacyNArithRing.vo /usr/lib64/coq/plugins/ring/LegacyRing.vo /usr/lib64/coq/plugins/ring/LegacyRing_theory.vo /usr/lib64/coq/plugins/ring/LegacyZArithRing.vo /usr/lib64/coq/plugins/ring/Ring_abstract.vo /usr/lib64/coq/plugins/ring/Ring_normalize.vo /usr/lib64/coq/plugins/ring/Setoid_ring.vo /usr/lib64/coq/plugins/ring/Setoid_ring_normalize.vo /usr/lib64/coq/plugins/ring/Setoid_ring_theory.vo /usr/lib64/coq/plugins/ring/g_ring.cmi /usr/lib64/coq/plugins/ring/ring.cmi /usr/lib64/coq/plugins/ring/ring_plugin.cma /usr/lib64/coq/plugins/ring/ring_plugin.cmxs /usr/lib64/coq/plugins/ring/ring_plugin_mod.cmi /usr/lib64/coq/plugins/romega /usr/lib64/coq/plugins/romega/ROmega.vo /usr/lib64/coq/plugins/romega/ReflOmegaCore.vo /usr/lib64/coq/plugins/romega/const_omega.cmi /usr/lib64/coq/plugins/romega/g_romega.cmi /usr/lib64/coq/plugins/romega/refl_omega.cmi /usr/lib64/coq/plugins/romega/romega_plugin.cma /usr/lib64/coq/plugins/romega/romega_plugin.cmxs /usr/lib64/coq/plugins/romega/romega_plugin_mod.cmi /usr/lib64/coq/plugins/rtauto /usr/lib64/coq/plugins/rtauto/Bintree.vo /usr/lib64/coq/plugins/rtauto/Rtauto.vo /usr/lib64/coq/plugins/rtauto/g_rtauto.cmi /usr/lib64/coq/plugins/rtauto/proof_search.cmi /usr/lib64/coq/plugins/rtauto/refl_tauto.cmi /usr/lib64/coq/plugins/rtauto/rtauto_plugin.cma /usr/lib64/coq/plugins/rtauto/rtauto_plugin.cmxs /usr/lib64/coq/plugins/rtauto/rtauto_plugin_mod.cmi /usr/lib64/coq/plugins/setoid_ring /usr/lib64/coq/plugins/setoid_ring/ArithRing.vo /usr/lib64/coq/plugins/setoid_ring/BinList.vo /usr/lib64/coq/plugins/setoid_ring/Field.vo /usr/lib64/coq/plugins/setoid_ring/Field_tac.vo /usr/lib64/coq/plugins/setoid_ring/Field_theory.vo /usr/lib64/coq/plugins/setoid_ring/InitialRing.vo /usr/lib64/coq/plugins/setoid_ring/NArithRing.vo /usr/lib64/coq/plugins/setoid_ring/RealField.vo /usr/lib64/coq/plugins/setoid_ring/Ring.vo /usr/lib64/coq/plugins/setoid_ring/Ring_base.vo /usr/lib64/coq/plugins/setoid_ring/Ring_equiv.vo /usr/lib64/coq/plugins/setoid_ring/Ring_polynom.vo /usr/lib64/coq/plugins/setoid_ring/Ring_tac.vo /usr/lib64/coq/plugins/setoid_ring/Ring_theory.vo /usr/lib64/coq/plugins/setoid_ring/ZArithRing.vo /usr/lib64/coq/plugins/setoid_ring/newring.cmi /usr/lib64/coq/plugins/setoid_ring/newring_plugin.cma /usr/lib64/coq/plugins/setoid_ring/newring_plugin.cmxs /usr/lib64/coq/plugins/setoid_ring/newring_plugin_mod.cmi /usr/lib64/coq/plugins/subtac /usr/lib64/coq/plugins/subtac/eterm.cmi /usr/lib64/coq/plugins/subtac/g_subtac.cmi /usr/lib64/coq/plugins/subtac/subtac.cmi /usr/lib64/coq/plugins/subtac/subtac_cases.cmi /usr/lib64/coq/plugins/subtac/subtac_classes.cmi /usr/lib64/coq/plugins/subtac/subtac_coercion.cmi /usr/lib64/coq/plugins/subtac/subtac_command.cmi /usr/lib64/coq/plugins/subtac/subtac_errors.cmi /usr/lib64/coq/plugins/subtac/subtac_obligations.cmi /usr/lib64/coq/plugins/subtac/subtac_plugin.cma /usr/lib64/coq/plugins/subtac/subtac_plugin.cmxs /usr/lib64/coq/plugins/subtac/subtac_plugin_mod.cmi /usr/lib64/coq/plugins/subtac/subtac_pretyping.cmi /usr/lib64/coq/plugins/subtac/subtac_pretyping_F.cmi /usr/lib64/coq/plugins/subtac/subtac_utils.cmi /usr/lib64/coq/plugins/syntax /usr/lib64/coq/plugins/syntax/ascii_syntax.cmi /usr/lib64/coq/plugins/syntax/ascii_syntax_plugin.cma /usr/lib64/coq/plugins/syntax/ascii_syntax_plugin.cmxs /usr/lib64/coq/plugins/syntax/ascii_syntax_plugin_mod.cmi /usr/lib64/coq/plugins/syntax/nat_syntax.cmi /usr/lib64/coq/plugins/syntax/nat_syntax_plugin.cma /usr/lib64/coq/plugins/syntax/nat_syntax_plugin.cmxs /usr/lib64/coq/plugins/syntax/nat_syntax_plugin_mod.cmi /usr/lib64/coq/plugins/syntax/numbers_syntax.cmi /usr/lib64/coq/plugins/syntax/numbers_syntax_plugin.cma /usr/lib64/coq/plugins/syntax/numbers_syntax_plugin.cmxs /usr/lib64/coq/plugins/syntax/numbers_syntax_plugin_mod.cmi /usr/lib64/coq/plugins/syntax/r_syntax.cmi /usr/lib64/coq/plugins/syntax/r_syntax_plugin.cma /usr/lib64/coq/plugins/syntax/r_syntax_plugin.cmxs /usr/lib64/coq/plugins/syntax/r_syntax_plugin_mod.cmi /usr/lib64/coq/plugins/syntax/string_syntax.cmi /usr/lib64/coq/plugins/syntax/string_syntax_plugin.cma /usr/lib64/coq/plugins/syntax/string_syntax_plugin.cmxs /usr/lib64/coq/plugins/syntax/string_syntax_plugin_mod.cmi /usr/lib64/coq/plugins/syntax/z_syntax.cmi /usr/lib64/coq/plugins/syntax/z_syntax_plugin.cma /usr/lib64/coq/plugins/syntax/z_syntax_plugin.cmxs /usr/lib64/coq/plugins/syntax/z_syntax_plugin_mod.cmi /usr/lib64/coq/plugins/xml /usr/lib64/coq/plugins/xml/acic.cmi /usr/lib64/coq/plugins/xml/acic2Xml.cmi /usr/lib64/coq/plugins/xml/cic2Xml.cmi /usr/lib64/coq/plugins/xml/cic2acic.cmi /usr/lib64/coq/plugins/xml/doubleTypeInference.cmi /usr/lib64/coq/plugins/xml/dumptree.cmi /usr/lib64/coq/plugins/xml/proof2aproof.cmi /usr/lib64/coq/plugins/xml/proofTree2Xml.cmi /usr/lib64/coq/plugins/xml/unshare.cmi /usr/lib64/coq/plugins/xml/xml.cmi /usr/lib64/coq/plugins/xml/xml_plugin.cma /usr/lib64/coq/plugins/xml/xml_plugin.cmxs /usr/lib64/coq/plugins/xml/xml_plugin_mod.cmi /usr/lib64/coq/plugins/xml/xmlcommand.cmi /usr/lib64/coq/plugins/xml/xmlentries.cmi /usr/lib64/coq/pretyping /usr/lib64/coq/pretyping/cases.cmi /usr/lib64/coq/pretyping/cbv.cmi /usr/lib64/coq/pretyping/classops.cmi /usr/lib64/coq/pretyping/clenv.cmi /usr/lib64/coq/pretyping/coercion.cmi /usr/lib64/coq/pretyping/detyping.cmi /usr/lib64/coq/pretyping/evarconv.cmi /usr/lib64/coq/pretyping/evarutil.cmi /usr/lib64/coq/pretyping/evd.cmi /usr/lib64/coq/pretyping/indrec.cmi /usr/lib64/coq/pretyping/inductiveops.cmi /usr/lib64/coq/pretyping/matching.cmi /usr/lib64/coq/pretyping/namegen.cmi /usr/lib64/coq/pretyping/pattern.cmi /usr/lib64/coq/pretyping/pretype_errors.cmi /usr/lib64/coq/pretyping/pretyping.cma /usr/lib64/coq/pretyping/pretyping.cmi /usr/lib64/coq/pretyping/rawterm.cmi /usr/lib64/coq/pretyping/recordops.cmi /usr/lib64/coq/pretyping/reductionops.cmi /usr/lib64/coq/pretyping/retyping.cmi /usr/lib64/coq/pretyping/tacred.cmi /usr/lib64/coq/pretyping/term_dnet.cmi /usr/lib64/coq/pretyping/termops.cmi /usr/lib64/coq/pretyping/typeclasses.cmi /usr/lib64/coq/pretyping/typeclasses_errors.cmi /usr/lib64/coq/pretyping/typing.cmi /usr/lib64/coq/pretyping/unification.cmi /usr/lib64/coq/pretyping/vnorm.cmi /usr/lib64/coq/proofs /usr/lib64/coq/proofs/clenvtac.cmi /usr/lib64/coq/proofs/decl_expr.cmi /usr/lib64/coq/proofs/decl_mode.cmi /usr/lib64/coq/proofs/evar_refiner.cmi /usr/lib64/coq/proofs/logic.cmi /usr/lib64/coq/proofs/pfedit.cmi /usr/lib64/coq/proofs/proof_trees.cmi /usr/lib64/coq/proofs/proof_type.cmi /usr/lib64/coq/proofs/proofs.cma /usr/lib64/coq/proofs/redexpr.cmi /usr/lib64/coq/proofs/refiner.cmi /usr/lib64/coq/proofs/tacexpr.cmi /usr/lib64/coq/proofs/tacmach.cmi /usr/lib64/coq/proofs/tactic_debug.cmi /usr/lib64/coq/states /usr/lib64/coq/states/initial.coq /usr/lib64/coq/tactics /usr/lib64/coq/tactics/auto.cmi /usr/lib64/coq/tactics/autorewrite.cmi /usr/lib64/coq/tactics/btermdn.cmi /usr/lib64/coq/tactics/class_tactics.cmi /usr/lib64/coq/tactics/contradiction.cmi /usr/lib64/coq/tactics/decl_interp.cmi /usr/lib64/coq/tactics/decl_proof_instr.cmi /usr/lib64/coq/tactics/dhyp.cmi /usr/lib64/coq/tactics/dn.cmi /usr/lib64/coq/tactics/eauto.cmi /usr/lib64/coq/tactics/elim.cmi /usr/lib64/coq/tactics/elimschemes.cmi /usr/lib64/coq/tactics/eqdecide.cmi /usr/lib64/coq/tactics/eqschemes.cmi /usr/lib64/coq/tactics/equality.cmi /usr/lib64/coq/tactics/evar_tactics.cmi /usr/lib64/coq/tactics/extraargs.cmi /usr/lib64/coq/tactics/extratactics.cmi /usr/lib64/coq/tactics/hiddentac.cmi /usr/lib64/coq/tactics/hightactics.cma /usr/lib64/coq/tactics/hipattern.cmi /usr/lib64/coq/tactics/inv.cmi /usr/lib64/coq/tactics/leminv.cmi /usr/lib64/coq/tactics/nbtermdn.cmi /usr/lib64/coq/tactics/refine.cmi /usr/lib64/coq/tactics/rewrite.cmi /usr/lib64/coq/tactics/tacinterp.cmi /usr/lib64/coq/tactics/tactic_option.cmi /usr/lib64/coq/tactics/tacticals.cmi /usr/lib64/coq/tactics/tactics.cma /usr/lib64/coq/tactics/tactics.cmi /usr/lib64/coq/tactics/tauto.cmi /usr/lib64/coq/tactics/termdn.cmi /usr/lib64/coq/theories /usr/lib64/coq/theories/Arith /usr/lib64/coq/theories/Arith/Arith.v /usr/lib64/coq/theories/Arith/Arith.vo /usr/lib64/coq/theories/Arith/Arith_base.v /usr/lib64/coq/theories/Arith/Arith_base.vo /usr/lib64/coq/theories/Arith/Between.v /usr/lib64/coq/theories/Arith/Between.vo /usr/lib64/coq/theories/Arith/Bool_nat.v /usr/lib64/coq/theories/Arith/Bool_nat.vo /usr/lib64/coq/theories/Arith/Compare.v /usr/lib64/coq/theories/Arith/Compare.vo /usr/lib64/coq/theories/Arith/Compare_dec.v /usr/lib64/coq/theories/Arith/Compare_dec.vo /usr/lib64/coq/theories/Arith/Div2.v /usr/lib64/coq/theories/Arith/Div2.vo /usr/lib64/coq/theories/Arith/EqNat.v /usr/lib64/coq/theories/Arith/EqNat.vo /usr/lib64/coq/theories/Arith/Euclid.v /usr/lib64/coq/theories/Arith/Euclid.vo /usr/lib64/coq/theories/Arith/Even.v /usr/lib64/coq/theories/Arith/Even.vo /usr/lib64/coq/theories/Arith/Factorial.v /usr/lib64/coq/theories/Arith/Factorial.vo /usr/lib64/coq/theories/Arith/Gt.v /usr/lib64/coq/theories/Arith/Gt.vo /usr/lib64/coq/theories/Arith/Le.v /usr/lib64/coq/theories/Arith/Le.vo /usr/lib64/coq/theories/Arith/Lt.v /usr/lib64/coq/theories/Arith/Lt.vo /usr/lib64/coq/theories/Arith/Max.v /usr/lib64/coq/theories/Arith/Max.vo /usr/lib64/coq/theories/Arith/Min.v /usr/lib64/coq/theories/Arith/Min.vo /usr/lib64/coq/theories/Arith/MinMax.v /usr/lib64/coq/theories/Arith/MinMax.vo /usr/lib64/coq/theories/Arith/Minus.v /usr/lib64/coq/theories/Arith/Minus.vo /usr/lib64/coq/theories/Arith/Mult.v /usr/lib64/coq/theories/Arith/Mult.vo /usr/lib64/coq/theories/Arith/NatOrderedType.v /usr/lib64/coq/theories/Arith/NatOrderedType.vo /usr/lib64/coq/theories/Arith/Peano_dec.v /usr/lib64/coq/theories/Arith/Peano_dec.vo /usr/lib64/coq/theories/Arith/Plus.v /usr/lib64/coq/theories/Arith/Plus.vo /usr/lib64/coq/theories/Arith/Wf_nat.v /usr/lib64/coq/theories/Arith/Wf_nat.vo /usr/lib64/coq/theories/Bool /usr/lib64/coq/theories/Bool/Bool.v /usr/lib64/coq/theories/Bool/Bool.vo /usr/lib64/coq/theories/Bool/BoolEq.v /usr/lib64/coq/theories/Bool/BoolEq.vo /usr/lib64/coq/theories/Bool/Bvector.v /usr/lib64/coq/theories/Bool/Bvector.vo /usr/lib64/coq/theories/Bool/DecBool.v /usr/lib64/coq/theories/Bool/DecBool.vo /usr/lib64/coq/theories/Bool/IfProp.v /usr/lib64/coq/theories/Bool/IfProp.vo /usr/lib64/coq/theories/Bool/Sumbool.v /usr/lib64/coq/theories/Bool/Sumbool.vo /usr/lib64/coq/theories/Bool/Zerob.v /usr/lib64/coq/theories/Bool/Zerob.vo /usr/lib64/coq/theories/Classes /usr/lib64/coq/theories/Classes/EquivDec.v /usr/lib64/coq/theories/Classes/EquivDec.vo /usr/lib64/coq/theories/Classes/Equivalence.v /usr/lib64/coq/theories/Classes/Equivalence.vo /usr/lib64/coq/theories/Classes/Init.v /usr/lib64/coq/theories/Classes/Init.vo /usr/lib64/coq/theories/Classes/Morphisms.v /usr/lib64/coq/theories/Classes/Morphisms.vo /usr/lib64/coq/theories/Classes/Morphisms_Prop.v /usr/lib64/coq/theories/Classes/Morphisms_Prop.vo /usr/lib64/coq/theories/Classes/Morphisms_Relations.v /usr/lib64/coq/theories/Classes/Morphisms_Relations.vo /usr/lib64/coq/theories/Classes/RelationClasses.v /usr/lib64/coq/theories/Classes/RelationClasses.vo /usr/lib64/coq/theories/Classes/RelationPairs.v /usr/lib64/coq/theories/Classes/RelationPairs.vo /usr/lib64/coq/theories/Classes/SetoidClass.v /usr/lib64/coq/theories/Classes/SetoidClass.vo /usr/lib64/coq/theories/Classes/SetoidDec.v /usr/lib64/coq/theories/Classes/SetoidDec.vo /usr/lib64/coq/theories/Classes/SetoidTactics.v /usr/lib64/coq/theories/Classes/SetoidTactics.vo /usr/lib64/coq/theories/FSets /usr/lib64/coq/theories/FSets/FMapAVL.v /usr/lib64/coq/theories/FSets/FMapAVL.vo /usr/lib64/coq/theories/FSets/FMapFacts.v /usr/lib64/coq/theories/FSets/FMapFacts.vo /usr/lib64/coq/theories/FSets/FMapFullAVL.v /usr/lib64/coq/theories/FSets/FMapFullAVL.vo /usr/lib64/coq/theories/FSets/FMapInterface.v /usr/lib64/coq/theories/FSets/FMapInterface.vo /usr/lib64/coq/theories/FSets/FMapList.v /usr/lib64/coq/theories/FSets/FMapList.vo /usr/lib64/coq/theories/FSets/FMapPositive.v /usr/lib64/coq/theories/FSets/FMapPositive.vo /usr/lib64/coq/theories/FSets/FMapWeakList.v /usr/lib64/coq/theories/FSets/FMapWeakList.vo /usr/lib64/coq/theories/FSets/FMaps.v /usr/lib64/coq/theories/FSets/FMaps.vo /usr/lib64/coq/theories/FSets/FSetAVL.v /usr/lib64/coq/theories/FSets/FSetAVL.vo /usr/lib64/coq/theories/FSets/FSetBridge.v /usr/lib64/coq/theories/FSets/FSetBridge.vo /usr/lib64/coq/theories/FSets/FSetCompat.v /usr/lib64/coq/theories/FSets/FSetCompat.vo /usr/lib64/coq/theories/FSets/FSetDecide.v /usr/lib64/coq/theories/FSets/FSetDecide.vo /usr/lib64/coq/theories/FSets/FSetEqProperties.v /usr/lib64/coq/theories/FSets/FSetEqProperties.vo /usr/lib64/coq/theories/FSets/FSetFacts.v /usr/lib64/coq/theories/FSets/FSetFacts.vo /usr/lib64/coq/theories/FSets/FSetInterface.v /usr/lib64/coq/theories/FSets/FSetInterface.vo /usr/lib64/coq/theories/FSets/FSetList.v /usr/lib64/coq/theories/FSets/FSetList.vo /usr/lib64/coq/theories/FSets/FSetPositive.v /usr/lib64/coq/theories/FSets/FSetPositive.vo /usr/lib64/coq/theories/FSets/FSetProperties.v /usr/lib64/coq/theories/FSets/FSetProperties.vo /usr/lib64/coq/theories/FSets/FSetToFiniteSet.v /usr/lib64/coq/theories/FSets/FSetToFiniteSet.vo /usr/lib64/coq/theories/FSets/FSetWeakList.v /usr/lib64/coq/theories/FSets/FSetWeakList.vo /usr/lib64/coq/theories/FSets/FSets.v /usr/lib64/coq/theories/FSets/FSets.vo /usr/lib64/coq/theories/Init /usr/lib64/coq/theories/Init/Datatypes.v /usr/lib64/coq/theories/Init/Datatypes.vo /usr/lib64/coq/theories/Init/Logic.v /usr/lib64/coq/theories/Init/Logic.vo /usr/lib64/coq/theories/Init/Logic_Type.v /usr/lib64/coq/theories/Init/Logic_Type.vo /usr/lib64/coq/theories/Init/Notations.v /usr/lib64/coq/theories/Init/Notations.vo /usr/lib64/coq/theories/Init/Peano.v /usr/lib64/coq/theories/Init/Peano.vo /usr/lib64/coq/theories/Init/Prelude.v /usr/lib64/coq/theories/Init/Prelude.vo /usr/lib64/coq/theories/Init/Specif.v /usr/lib64/coq/theories/Init/Specif.vo /usr/lib64/coq/theories/Init/Tactics.v /usr/lib64/coq/theories/Init/Tactics.vo /usr/lib64/coq/theories/Init/Wf.v /usr/lib64/coq/theories/Init/Wf.vo /usr/lib64/coq/theories/Lists /usr/lib64/coq/theories/Lists/List.v /usr/lib64/coq/theories/Lists/List.vo /usr/lib64/coq/theories/Lists/ListSet.v /usr/lib64/coq/theories/Lists/ListSet.vo /usr/lib64/coq/theories/Lists/ListTactics.v /usr/lib64/coq/theories/Lists/ListTactics.vo /usr/lib64/coq/theories/Lists/SetoidList.v /usr/lib64/coq/theories/Lists/SetoidList.vo /usr/lib64/coq/theories/Lists/StreamMemo.v /usr/lib64/coq/theories/Lists/StreamMemo.vo /usr/lib64/coq/theories/Lists/Streams.v /usr/lib64/coq/theories/Lists/Streams.vo /usr/lib64/coq/theories/Lists/TheoryList.v /usr/lib64/coq/theories/Lists/TheoryList.vo /usr/lib64/coq/theories/Logic /usr/lib64/coq/theories/Logic/Berardi.v /usr/lib64/coq/theories/Logic/Berardi.vo /usr/lib64/coq/theories/Logic/ChoiceFacts.v /usr/lib64/coq/theories/Logic/ChoiceFacts.vo /usr/lib64/coq/theories/Logic/Classical.v /usr/lib64/coq/theories/Logic/Classical.vo /usr/lib64/coq/theories/Logic/ClassicalChoice.v /usr/lib64/coq/theories/Logic/ClassicalChoice.vo /usr/lib64/coq/theories/Logic/ClassicalDescription.v /usr/lib64/coq/theories/Logic/ClassicalDescription.vo /usr/lib64/coq/theories/Logic/ClassicalEpsilon.v /usr/lib64/coq/theories/Logic/ClassicalEpsilon.vo /usr/lib64/coq/theories/Logic/ClassicalFacts.v /usr/lib64/coq/theories/Logic/ClassicalFacts.vo /usr/lib64/coq/theories/Logic/ClassicalUniqueChoice.v /usr/lib64/coq/theories/Logic/ClassicalUniqueChoice.vo /usr/lib64/coq/theories/Logic/Classical_Pred_Set.v /usr/lib64/coq/theories/Logic/Classical_Pred_Set.vo /usr/lib64/coq/theories/Logic/Classical_Pred_Type.v /usr/lib64/coq/theories/Logic/Classical_Pred_Type.vo /usr/lib64/coq/theories/Logic/Classical_Prop.v /usr/lib64/coq/theories/Logic/Classical_Prop.vo /usr/lib64/coq/theories/Logic/Classical_Type.v /usr/lib64/coq/theories/Logic/Classical_Type.vo /usr/lib64/coq/theories/Logic/ConstructiveEpsilon.v /usr/lib64/coq/theories/Logic/ConstructiveEpsilon.vo /usr/lib64/coq/theories/Logic/Decidable.v /usr/lib64/coq/theories/Logic/Decidable.vo /usr/lib64/coq/theories/Logic/Description.v /usr/lib64/coq/theories/Logic/Description.vo /usr/lib64/coq/theories/Logic/Diaconescu.v /usr/lib64/coq/theories/Logic/Diaconescu.vo /usr/lib64/coq/theories/Logic/Epsilon.v /usr/lib64/coq/theories/Logic/Epsilon.vo /usr/lib64/coq/theories/Logic/Eqdep.v /usr/lib64/coq/theories/Logic/Eqdep.vo /usr/lib64/coq/theories/Logic/EqdepFacts.v /usr/lib64/coq/theories/Logic/EqdepFacts.vo /usr/lib64/coq/theories/Logic/Eqdep_dec.v /usr/lib64/coq/theories/Logic/Eqdep_dec.vo /usr/lib64/coq/theories/Logic/FunctionalExtensionality.v /usr/lib64/coq/theories/Logic/FunctionalExtensionality.vo /usr/lib64/coq/theories/Logic/Hurkens.v /usr/lib64/coq/theories/Logic/Hurkens.vo /usr/lib64/coq/theories/Logic/IndefiniteDescription.v /usr/lib64/coq/theories/Logic/IndefiniteDescription.vo /usr/lib64/coq/theories/Logic/JMeq.v /usr/lib64/coq/theories/Logic/JMeq.vo /usr/lib64/coq/theories/Logic/ProofIrrelevance.v /usr/lib64/coq/theories/Logic/ProofIrrelevance.vo /usr/lib64/coq/theories/Logic/ProofIrrelevanceFacts.v /usr/lib64/coq/theories/Logic/ProofIrrelevanceFacts.vo /usr/lib64/coq/theories/Logic/RelationalChoice.v /usr/lib64/coq/theories/Logic/RelationalChoice.vo /usr/lib64/coq/theories/Logic/SetIsType.v /usr/lib64/coq/theories/Logic/SetIsType.vo /usr/lib64/coq/theories/MSets /usr/lib64/coq/theories/MSets/MSetAVL.v /usr/lib64/coq/theories/MSets/MSetAVL.vo /usr/lib64/coq/theories/MSets/MSetDecide.v /usr/lib64/coq/theories/MSets/MSetDecide.vo /usr/lib64/coq/theories/MSets/MSetEqProperties.v /usr/lib64/coq/theories/MSets/MSetEqProperties.vo /usr/lib64/coq/theories/MSets/MSetFacts.v /usr/lib64/coq/theories/MSets/MSetFacts.vo /usr/lib64/coq/theories/MSets/MSetInterface.v /usr/lib64/coq/theories/MSets/MSetInterface.vo /usr/lib64/coq/theories/MSets/MSetList.v /usr/lib64/coq/theories/MSets/MSetList.vo /usr/lib64/coq/theories/MSets/MSetPositive.v /usr/lib64/coq/theories/MSets/MSetPositive.vo /usr/lib64/coq/theories/MSets/MSetProperties.v /usr/lib64/coq/theories/MSets/MSetProperties.vo /usr/lib64/coq/theories/MSets/MSetToFiniteSet.v /usr/lib64/coq/theories/MSets/MSetToFiniteSet.vo /usr/lib64/coq/theories/MSets/MSetWeakList.v /usr/lib64/coq/theories/MSets/MSetWeakList.vo /usr/lib64/coq/theories/MSets/MSets.v /usr/lib64/coq/theories/MSets/MSets.vo /usr/lib64/coq/theories/NArith /usr/lib64/coq/theories/NArith/BinNat.v /usr/lib64/coq/theories/NArith/BinNat.vo /usr/lib64/coq/theories/NArith/BinPos.v /usr/lib64/coq/theories/NArith/BinPos.vo /usr/lib64/coq/theories/NArith/NArith.v /usr/lib64/coq/theories/NArith/NArith.vo /usr/lib64/coq/theories/NArith/NOrderedType.v /usr/lib64/coq/theories/NArith/NOrderedType.vo /usr/lib64/coq/theories/NArith/Ndec.v /usr/lib64/coq/theories/NArith/Ndec.vo /usr/lib64/coq/theories/NArith/Ndigits.v /usr/lib64/coq/theories/NArith/Ndigits.vo /usr/lib64/coq/theories/NArith/Ndist.v /usr/lib64/coq/theories/NArith/Ndist.vo /usr/lib64/coq/theories/NArith/Nminmax.v /usr/lib64/coq/theories/NArith/Nminmax.vo /usr/lib64/coq/theories/NArith/Nnat.v /usr/lib64/coq/theories/NArith/Nnat.vo /usr/lib64/coq/theories/NArith/POrderedType.v /usr/lib64/coq/theories/NArith/POrderedType.vo /usr/lib64/coq/theories/NArith/Pminmax.v /usr/lib64/coq/theories/NArith/Pminmax.vo /usr/lib64/coq/theories/NArith/Pnat.v /usr/lib64/coq/theories/NArith/Pnat.vo /usr/lib64/coq/theories/Numbers /usr/lib64/coq/theories/Numbers/BigNumPrelude.v /usr/lib64/coq/theories/Numbers/BigNumPrelude.vo /usr/lib64/coq/theories/Numbers/Cyclic /usr/lib64/coq/theories/Numbers/Cyclic/Abstract /usr/lib64/coq/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v /usr/lib64/coq/theories/Numbers/Cyclic/Abstract/CyclicAxioms.vo /usr/lib64/coq/theories/Numbers/Cyclic/Abstract/NZCyclic.v /usr/lib64/coq/theories/Numbers/Cyclic/Abstract/NZCyclic.vo /usr/lib64/coq/theories/Numbers/Cyclic/DoubleCyclic /usr/lib64/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v /usr/lib64/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.vo /usr/lib64/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v /usr/lib64/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.vo /usr/lib64/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v /usr/lib64/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.vo /usr/lib64/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v /usr/lib64/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.vo /usr/lib64/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v /usr/lib64/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.vo /usr/lib64/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v /usr/lib64/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.vo /usr/lib64/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v /usr/lib64/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.vo /usr/lib64/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v /usr/lib64/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.vo /usr/lib64/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v /usr/lib64/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.vo /usr/lib64/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v /usr/lib64/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.vo /usr/lib64/coq/theories/Numbers/Cyclic/Int31 /usr/lib64/coq/theories/Numbers/Cyclic/Int31/Cyclic31.v /usr/lib64/coq/theories/Numbers/Cyclic/Int31/Cyclic31.vo /usr/lib64/coq/theories/Numbers/Cyclic/Int31/Int31.v /usr/lib64/coq/theories/Numbers/Cyclic/Int31/Int31.vo /usr/lib64/coq/theories/Numbers/Cyclic/Int31/Ring31.v /usr/lib64/coq/theories/Numbers/Cyclic/Int31/Ring31.vo /usr/lib64/coq/theories/Numbers/Cyclic/ZModulo /usr/lib64/coq/theories/Numbers/Cyclic/ZModulo/ZModulo.v /usr/lib64/coq/theories/Numbers/Cyclic/ZModulo/ZModulo.vo /usr/lib64/coq/theories/Numbers/Integer /usr/lib64/coq/theories/Numbers/Integer/Abstract /usr/lib64/coq/theories/Numbers/Integer/Abstract/ZAdd.v /usr/lib64/coq/theories/Numbers/Integer/Abstract/ZAdd.vo /usr/lib64/coq/theories/Numbers/Integer/Abstract/ZAddOrder.v /usr/lib64/coq/theories/Numbers/Integer/Abstract/ZAddOrder.vo /usr/lib64/coq/theories/Numbers/Integer/Abstract/ZAxioms.v /usr/lib64/coq/theories/Numbers/Integer/Abstract/ZAxioms.vo /usr/lib64/coq/theories/Numbers/Integer/Abstract/ZBase.v /usr/lib64/coq/theories/Numbers/Integer/Abstract/ZBase.vo /usr/lib64/coq/theories/Numbers/Integer/Abstract/ZDivEucl.v /usr/lib64/coq/theories/Numbers/Integer/Abstract/ZDivEucl.vo /usr/lib64/coq/theories/Numbers/Integer/Abstract/ZDivFloor.v /usr/lib64/coq/theories/Numbers/Integer/Abstract/ZDivFloor.vo /usr/lib64/coq/theories/Numbers/Integer/Abstract/ZDivTrunc.v /usr/lib64/coq/theories/Numbers/Integer/Abstract/ZDivTrunc.vo /usr/lib64/coq/theories/Numbers/Integer/Abstract/ZLt.v /usr/lib64/coq/theories/Numbers/Integer/Abstract/ZLt.vo /usr/lib64/coq/theories/Numbers/Integer/Abstract/ZMul.v /usr/lib64/coq/theories/Numbers/Integer/Abstract/ZMul.vo /usr/lib64/coq/theories/Numbers/Integer/Abstract/ZMulOrder.v /usr/lib64/coq/theories/Numbers/Integer/Abstract/ZMulOrder.vo /usr/lib64/coq/theories/Numbers/Integer/Abstract/ZProperties.v /usr/lib64/coq/theories/Numbers/Integer/Abstract/ZProperties.vo /usr/lib64/coq/theories/Numbers/Integer/Abstract/ZSgnAbs.v /usr/lib64/coq/theories/Numbers/Integer/Abstract/ZSgnAbs.vo /usr/lib64/coq/theories/Numbers/Integer/BigZ /usr/lib64/coq/theories/Numbers/Integer/BigZ/BigZ.v /usr/lib64/coq/theories/Numbers/Integer/BigZ/BigZ.vo /usr/lib64/coq/theories/Numbers/Integer/BigZ/ZMake.v /usr/lib64/coq/theories/Numbers/Integer/BigZ/ZMake.vo /usr/lib64/coq/theories/Numbers/Integer/Binary /usr/lib64/coq/theories/Numbers/Integer/Binary/ZBinary.v /usr/lib64/coq/theories/Numbers/Integer/Binary/ZBinary.vo /usr/lib64/coq/theories/Numbers/Integer/NatPairs /usr/lib64/coq/theories/Numbers/Integer/NatPairs/ZNatPairs.v /usr/lib64/coq/theories/Numbers/Integer/NatPairs/ZNatPairs.vo /usr/lib64/coq/theories/Numbers/Integer/SpecViaZ /usr/lib64/coq/theories/Numbers/Integer/SpecViaZ/ZSig.v /usr/lib64/coq/theories/Numbers/Integer/SpecViaZ/ZSig.vo /usr/lib64/coq/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v /usr/lib64/coq/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.vo /usr/lib64/coq/theories/Numbers/NaryFunctions.v /usr/lib64/coq/theories/Numbers/NaryFunctions.vo /usr/lib64/coq/theories/Numbers/NatInt /usr/lib64/coq/theories/Numbers/NatInt/NZAdd.v /usr/lib64/coq/theories/Numbers/NatInt/NZAdd.vo /usr/lib64/coq/theories/Numbers/NatInt/NZAddOrder.v /usr/lib64/coq/theories/Numbers/NatInt/NZAddOrder.vo /usr/lib64/coq/theories/Numbers/NatInt/NZAxioms.v /usr/lib64/coq/theories/Numbers/NatInt/NZAxioms.vo /usr/lib64/coq/theories/Numbers/NatInt/NZBase.v /usr/lib64/coq/theories/Numbers/NatInt/NZBase.vo /usr/lib64/coq/theories/Numbers/NatInt/NZDiv.v /usr/lib64/coq/theories/Numbers/NatInt/NZDiv.vo /usr/lib64/coq/theories/Numbers/NatInt/NZDomain.v /usr/lib64/coq/theories/Numbers/NatInt/NZDomain.vo /usr/lib64/coq/theories/Numbers/NatInt/NZMul.v /usr/lib64/coq/theories/Numbers/NatInt/NZMul.vo /usr/lib64/coq/theories/Numbers/NatInt/NZMulOrder.v /usr/lib64/coq/theories/Numbers/NatInt/NZMulOrder.vo /usr/lib64/coq/theories/Numbers/NatInt/NZOrder.v /usr/lib64/coq/theories/Numbers/NatInt/NZOrder.vo /usr/lib64/coq/theories/Numbers/NatInt/NZProperties.v /usr/lib64/coq/theories/Numbers/NatInt/NZProperties.vo /usr/lib64/coq/theories/Numbers/Natural /usr/lib64/coq/theories/Numbers/Natural/Abstract /usr/lib64/coq/theories/Numbers/Natural/Abstract/NAdd.v /usr/lib64/coq/theories/Numbers/Natural/Abstract/NAdd.vo /usr/lib64/coq/theories/Numbers/Natural/Abstract/NAddOrder.v /usr/lib64/coq/theories/Numbers/Natural/Abstract/NAddOrder.vo /usr/lib64/coq/theories/Numbers/Natural/Abstract/NAxioms.v /usr/lib64/coq/theories/Numbers/Natural/Abstract/NAxioms.vo /usr/lib64/coq/theories/Numbers/Natural/Abstract/NBase.v /usr/lib64/coq/theories/Numbers/Natural/Abstract/NBase.vo /usr/lib64/coq/theories/Numbers/Natural/Abstract/NDefOps.v /usr/lib64/coq/theories/Numbers/Natural/Abstract/NDefOps.vo /usr/lib64/coq/theories/Numbers/Natural/Abstract/NDiv.v /usr/lib64/coq/theories/Numbers/Natural/Abstract/NDiv.vo /usr/lib64/coq/theories/Numbers/Natural/Abstract/NIso.v /usr/lib64/coq/theories/Numbers/Natural/Abstract/NIso.vo /usr/lib64/coq/theories/Numbers/Natural/Abstract/NMulOrder.v /usr/lib64/coq/theories/Numbers/Natural/Abstract/NMulOrder.vo /usr/lib64/coq/theories/Numbers/Natural/Abstract/NOrder.v /usr/lib64/coq/theories/Numbers/Natural/Abstract/NOrder.vo /usr/lib64/coq/theories/Numbers/Natural/Abstract/NProperties.v /usr/lib64/coq/theories/Numbers/Natural/Abstract/NProperties.vo /usr/lib64/coq/theories/Numbers/Natural/Abstract/NStrongRec.v /usr/lib64/coq/theories/Numbers/Natural/Abstract/NStrongRec.vo /usr/lib64/coq/theories/Numbers/Natural/Abstract/NSub.v /usr/lib64/coq/theories/Numbers/Natural/Abstract/NSub.vo /usr/lib64/coq/theories/Numbers/Natural/BigN /usr/lib64/coq/theories/Numbers/Natural/BigN/BigN.v /usr/lib64/coq/theories/Numbers/Natural/BigN/BigN.vo /usr/lib64/coq/theories/Numbers/Natural/BigN/NMake.v /usr/lib64/coq/theories/Numbers/Natural/BigN/NMake.vo /usr/lib64/coq/theories/Numbers/Natural/BigN/NMake_gen.v /usr/lib64/coq/theories/Numbers/Natural/BigN/NMake_gen.vo /usr/lib64/coq/theories/Numbers/Natural/BigN/Nbasic.v /usr/lib64/coq/theories/Numbers/Natural/BigN/Nbasic.vo /usr/lib64/coq/theories/Numbers/Natural/Binary /usr/lib64/coq/theories/Numbers/Natural/Binary/NBinary.v /usr/lib64/coq/theories/Numbers/Natural/Binary/NBinary.vo /usr/lib64/coq/theories/Numbers/Natural/Peano /usr/lib64/coq/theories/Numbers/Natural/Peano/NPeano.v /usr/lib64/coq/theories/Numbers/Natural/Peano/NPeano.vo /usr/lib64/coq/theories/Numbers/Natural/SpecViaZ /usr/lib64/coq/theories/Numbers/Natural/SpecViaZ/NSig.v /usr/lib64/coq/theories/Numbers/Natural/SpecViaZ/NSig.vo /usr/lib64/coq/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v /usr/lib64/coq/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.vo /usr/lib64/coq/theories/Numbers/NumPrelude.v /usr/lib64/coq/theories/Numbers/NumPrelude.vo /usr/lib64/coq/theories/Numbers/Rational /usr/lib64/coq/theories/Numbers/Rational/BigQ /usr/lib64/coq/theories/Numbers/Rational/BigQ/BigQ.v /usr/lib64/coq/theories/Numbers/Rational/BigQ/BigQ.vo /usr/lib64/coq/theories/Numbers/Rational/BigQ/QMake.v /usr/lib64/coq/theories/Numbers/Rational/BigQ/QMake.vo /usr/lib64/coq/theories/Numbers/Rational/SpecViaQ /usr/lib64/coq/theories/Numbers/Rational/SpecViaQ/QSig.v /usr/lib64/coq/theories/Numbers/Rational/SpecViaQ/QSig.vo /usr/lib64/coq/theories/Program /usr/lib64/coq/theories/Program/Basics.v /usr/lib64/coq/theories/Program/Basics.vo /usr/lib64/coq/theories/Program/Combinators.v /usr/lib64/coq/theories/Program/Combinators.vo /usr/lib64/coq/theories/Program/Equality.v /usr/lib64/coq/theories/Program/Equality.vo /usr/lib64/coq/theories/Program/Program.v /usr/lib64/coq/theories/Program/Program.vo /usr/lib64/coq/theories/Program/Subset.v /usr/lib64/coq/theories/Program/Subset.vo /usr/lib64/coq/theories/Program/Syntax.v /usr/lib64/coq/theories/Program/Syntax.vo /usr/lib64/coq/theories/Program/Tactics.v /usr/lib64/coq/theories/Program/Tactics.vo /usr/lib64/coq/theories/Program/Utils.v /usr/lib64/coq/theories/Program/Utils.vo /usr/lib64/coq/theories/Program/Wf.v /usr/lib64/coq/theories/Program/Wf.vo /usr/lib64/coq/theories/QArith /usr/lib64/coq/theories/QArith/QArith.v /usr/lib64/coq/theories/QArith/QArith.vo /usr/lib64/coq/theories/QArith/QArith_base.v /usr/lib64/coq/theories/QArith/QArith_base.vo /usr/lib64/coq/theories/QArith/QOrderedType.v /usr/lib64/coq/theories/QArith/QOrderedType.vo /usr/lib64/coq/theories/QArith/Qabs.v /usr/lib64/coq/theories/QArith/Qabs.vo /usr/lib64/coq/theories/QArith/Qcanon.v /usr/lib64/coq/theories/QArith/Qcanon.vo /usr/lib64/coq/theories/QArith/Qfield.v /usr/lib64/coq/theories/QArith/Qfield.vo /usr/lib64/coq/theories/QArith/Qminmax.v /usr/lib64/coq/theories/QArith/Qminmax.vo /usr/lib64/coq/theories/QArith/Qpower.v /usr/lib64/coq/theories/QArith/Qpower.vo /usr/lib64/coq/theories/QArith/Qreals.v /usr/lib64/coq/theories/QArith/Qreals.vo /usr/lib64/coq/theories/QArith/Qreduction.v /usr/lib64/coq/theories/QArith/Qreduction.vo /usr/lib64/coq/theories/QArith/Qring.v /usr/lib64/coq/theories/QArith/Qring.vo /usr/lib64/coq/theories/QArith/Qround.v /usr/lib64/coq/theories/QArith/Qround.vo /usr/lib64/coq/theories/Reals /usr/lib64/coq/theories/Reals/Alembert.v /usr/lib64/coq/theories/Reals/Alembert.vo /usr/lib64/coq/theories/Reals/AltSeries.v /usr/lib64/coq/theories/Reals/AltSeries.vo /usr/lib64/coq/theories/Reals/ArithProp.v /usr/lib64/coq/theories/Reals/ArithProp.vo /usr/lib64/coq/theories/Reals/Binomial.v /usr/lib64/coq/theories/Reals/Binomial.vo /usr/lib64/coq/theories/Reals/Cauchy_prod.v /usr/lib64/coq/theories/Reals/Cauchy_prod.vo /usr/lib64/coq/theories/Reals/Cos_plus.v /usr/lib64/coq/theories/Reals/Cos_plus.vo /usr/lib64/coq/theories/Reals/Cos_rel.v /usr/lib64/coq/theories/Reals/Cos_rel.vo /usr/lib64/coq/theories/Reals/DiscrR.v /usr/lib64/coq/theories/Reals/DiscrR.vo /usr/lib64/coq/theories/Reals/Exp_prop.v /usr/lib64/coq/theories/Reals/Exp_prop.vo /usr/lib64/coq/theories/Reals/Integration.v /usr/lib64/coq/theories/Reals/Integration.vo /usr/lib64/coq/theories/Reals/LegacyRfield.v /usr/lib64/coq/theories/Reals/LegacyRfield.vo /usr/lib64/coq/theories/Reals/MVT.v /usr/lib64/coq/theories/Reals/MVT.vo /usr/lib64/coq/theories/Reals/NewtonInt.v /usr/lib64/coq/theories/Reals/NewtonInt.vo /usr/lib64/coq/theories/Reals/PSeries_reg.v /usr/lib64/coq/theories/Reals/PSeries_reg.vo /usr/lib64/coq/theories/Reals/PartSum.v /usr/lib64/coq/theories/Reals/PartSum.vo /usr/lib64/coq/theories/Reals/RIneq.v /usr/lib64/coq/theories/Reals/RIneq.vo /usr/lib64/coq/theories/Reals/RList.v /usr/lib64/coq/theories/Reals/RList.vo /usr/lib64/coq/theories/Reals/ROrderedType.v /usr/lib64/coq/theories/Reals/ROrderedType.vo /usr/lib64/coq/theories/Reals/R_Ifp.v /usr/lib64/coq/theories/Reals/R_Ifp.vo /usr/lib64/coq/theories/Reals/R_sqr.v /usr/lib64/coq/theories/Reals/R_sqr.vo /usr/lib64/coq/theories/Reals/R_sqrt.v /usr/lib64/coq/theories/Reals/R_sqrt.vo /usr/lib64/coq/theories/Reals/Ranalysis.v /usr/lib64/coq/theories/Reals/Ranalysis.vo /usr/lib64/coq/theories/Reals/Ranalysis1.v /usr/lib64/coq/theories/Reals/Ranalysis1.vo /usr/lib64/coq/theories/Reals/Ranalysis2.v /usr/lib64/coq/theories/Reals/Ranalysis2.vo /usr/lib64/coq/theories/Reals/Ranalysis3.v /usr/lib64/coq/theories/Reals/Ranalysis3.vo /usr/lib64/coq/theories/Reals/Ranalysis4.v /usr/lib64/coq/theories/Reals/Ranalysis4.vo /usr/lib64/coq/theories/Reals/Raxioms.v /usr/lib64/coq/theories/Reals/Raxioms.vo /usr/lib64/coq/theories/Reals/Rbase.v /usr/lib64/coq/theories/Reals/Rbase.vo /usr/lib64/coq/theories/Reals/Rbasic_fun.v /usr/lib64/coq/theories/Reals/Rbasic_fun.vo /usr/lib64/coq/theories/Reals/Rcomplete.v /usr/lib64/coq/theories/Reals/Rcomplete.vo /usr/lib64/coq/theories/Reals/Rdefinitions.v /usr/lib64/coq/theories/Reals/Rdefinitions.vo /usr/lib64/coq/theories/Reals/Rderiv.v /usr/lib64/coq/theories/Reals/Rderiv.vo /usr/lib64/coq/theories/Reals/Reals.v /usr/lib64/coq/theories/Reals/Reals.vo /usr/lib64/coq/theories/Reals/Rfunctions.v /usr/lib64/coq/theories/Reals/Rfunctions.vo /usr/lib64/coq/theories/Reals/Rgeom.v /usr/lib64/coq/theories/Reals/Rgeom.vo /usr/lib64/coq/theories/Reals/RiemannInt.v /usr/lib64/coq/theories/Reals/RiemannInt.vo /usr/lib64/coq/theories/Reals/RiemannInt_SF.v /usr/lib64/coq/theories/Reals/RiemannInt_SF.vo /usr/lib64/coq/theories/Reals/Rlimit.v /usr/lib64/coq/theories/Reals/Rlimit.vo /usr/lib64/coq/theories/Reals/Rlogic.v /usr/lib64/coq/theories/Reals/Rlogic.vo /usr/lib64/coq/theories/Reals/Rminmax.v /usr/lib64/coq/theories/Reals/Rminmax.vo /usr/lib64/coq/theories/Reals/Rpow_def.v /usr/lib64/coq/theories/Reals/Rpow_def.vo /usr/lib64/coq/theories/Reals/Rpower.v /usr/lib64/coq/theories/Reals/Rpower.vo /usr/lib64/coq/theories/Reals/Rprod.v /usr/lib64/coq/theories/Reals/Rprod.vo /usr/lib64/coq/theories/Reals/Rseries.v /usr/lib64/coq/theories/Reals/Rseries.vo /usr/lib64/coq/theories/Reals/Rsigma.v /usr/lib64/coq/theories/Reals/Rsigma.vo /usr/lib64/coq/theories/Reals/Rsqrt_def.v /usr/lib64/coq/theories/Reals/Rsqrt_def.vo /usr/lib64/coq/theories/Reals/Rtopology.v /usr/lib64/coq/theories/Reals/Rtopology.vo /usr/lib64/coq/theories/Reals/Rtrigo.v /usr/lib64/coq/theories/Reals/Rtrigo.vo /usr/lib64/coq/theories/Reals/Rtrigo_alt.v /usr/lib64/coq/theories/Reals/Rtrigo_alt.vo /usr/lib64/coq/theories/Reals/Rtrigo_calc.v /usr/lib64/coq/theories/Reals/Rtrigo_calc.vo /usr/lib64/coq/theories/Reals/Rtrigo_def.v /usr/lib64/coq/theories/Reals/Rtrigo_def.vo /usr/lib64/coq/theories/Reals/Rtrigo_fun.v /usr/lib64/coq/theories/Reals/Rtrigo_fun.vo /usr/lib64/coq/theories/Reals/Rtrigo_reg.v /usr/lib64/coq/theories/Reals/Rtrigo_reg.vo /usr/lib64/coq/theories/Reals/SeqProp.v /usr/lib64/coq/theories/Reals/SeqProp.vo /usr/lib64/coq/theories/Reals/SeqSeries.v /usr/lib64/coq/theories/Reals/SeqSeries.vo /usr/lib64/coq/theories/Reals/SplitAbsolu.v /usr/lib64/coq/theories/Reals/SplitAbsolu.vo /usr/lib64/coq/theories/Reals/SplitRmult.v /usr/lib64/coq/theories/Reals/SplitRmult.vo /usr/lib64/coq/theories/Reals/Sqrt_reg.v /usr/lib64/coq/theories/Reals/Sqrt_reg.vo /usr/lib64/coq/theories/Relations /usr/lib64/coq/theories/Relations/Operators_Properties.v /usr/lib64/coq/theories/Relations/Operators_Properties.vo /usr/lib64/coq/theories/Relations/Relation_Definitions.v /usr/lib64/coq/theories/Relations/Relation_Definitions.vo /usr/lib64/coq/theories/Relations/Relation_Operators.v /usr/lib64/coq/theories/Relations/Relation_Operators.vo /usr/lib64/coq/theories/Relations/Relations.v /usr/lib64/coq/theories/Relations/Relations.vo /usr/lib64/coq/theories/Setoids /usr/lib64/coq/theories/Setoids/Setoid.v /usr/lib64/coq/theories/Setoids/Setoid.vo /usr/lib64/coq/theories/Sets /usr/lib64/coq/theories/Sets/Classical_sets.v /usr/lib64/coq/theories/Sets/Classical_sets.vo /usr/lib64/coq/theories/Sets/Constructive_sets.v /usr/lib64/coq/theories/Sets/Constructive_sets.vo /usr/lib64/coq/theories/Sets/Cpo.v /usr/lib64/coq/theories/Sets/Cpo.vo /usr/lib64/coq/theories/Sets/Ensembles.v /usr/lib64/coq/theories/Sets/Ensembles.vo /usr/lib64/coq/theories/Sets/Finite_sets.v /usr/lib64/coq/theories/Sets/Finite_sets.vo /usr/lib64/coq/theories/Sets/Finite_sets_facts.v /usr/lib64/coq/theories/Sets/Finite_sets_facts.vo /usr/lib64/coq/theories/Sets/Image.v /usr/lib64/coq/theories/Sets/Image.vo /usr/lib64/coq/theories/Sets/Infinite_sets.v /usr/lib64/coq/theories/Sets/Infinite_sets.vo /usr/lib64/coq/theories/Sets/Integers.v /usr/lib64/coq/theories/Sets/Integers.vo /usr/lib64/coq/theories/Sets/Multiset.v /usr/lib64/coq/theories/Sets/Multiset.vo /usr/lib64/coq/theories/Sets/Partial_Order.v /usr/lib64/coq/theories/Sets/Partial_Order.vo /usr/lib64/coq/theories/Sets/Permut.v /usr/lib64/coq/theories/Sets/Permut.vo /usr/lib64/coq/theories/Sets/Powerset.v /usr/lib64/coq/theories/Sets/Powerset.vo /usr/lib64/coq/theories/Sets/Powerset_Classical_facts.v /usr/lib64/coq/theories/Sets/Powerset_Classical_facts.vo /usr/lib64/coq/theories/Sets/Powerset_facts.v /usr/lib64/coq/theories/Sets/Powerset_facts.vo /usr/lib64/coq/theories/Sets/Relations_1.v /usr/lib64/coq/theories/Sets/Relations_1.vo /usr/lib64/coq/theories/Sets/Relations_1_facts.v /usr/lib64/coq/theories/Sets/Relations_1_facts.vo /usr/lib64/coq/theories/Sets/Relations_2.v /usr/lib64/coq/theories/Sets/Relations_2.vo /usr/lib64/coq/theories/Sets/Relations_2_facts.v /usr/lib64/coq/theories/Sets/Relations_2_facts.vo /usr/lib64/coq/theories/Sets/Relations_3.v /usr/lib64/coq/theories/Sets/Relations_3.vo /usr/lib64/coq/theories/Sets/Relations_3_facts.v /usr/lib64/coq/theories/Sets/Relations_3_facts.vo /usr/lib64/coq/theories/Sets/Uniset.v /usr/lib64/coq/theories/Sets/Uniset.vo /usr/lib64/coq/theories/Sorting /usr/lib64/coq/theories/Sorting/Heap.v /usr/lib64/coq/theories/Sorting/Heap.vo /usr/lib64/coq/theories/Sorting/Mergesort.v /usr/lib64/coq/theories/Sorting/Mergesort.vo /usr/lib64/coq/theories/Sorting/PermutEq.v /usr/lib64/coq/theories/Sorting/PermutEq.vo /usr/lib64/coq/theories/Sorting/PermutSetoid.v /usr/lib64/coq/theories/Sorting/PermutSetoid.vo /usr/lib64/coq/theories/Sorting/Permutation.v /usr/lib64/coq/theories/Sorting/Permutation.vo /usr/lib64/coq/theories/Sorting/Sorted.v /usr/lib64/coq/theories/Sorting/Sorted.vo /usr/lib64/coq/theories/Sorting/Sorting.v /usr/lib64/coq/theories/Sorting/Sorting.vo /usr/lib64/coq/theories/Strings /usr/lib64/coq/theories/Strings/Ascii.v /usr/lib64/coq/theories/Strings/Ascii.vo /usr/lib64/coq/theories/Strings/String.v /usr/lib64/coq/theories/Strings/String.vo /usr/lib64/coq/theories/Structures /usr/lib64/coq/theories/Structures/DecidableType.v /usr/lib64/coq/theories/Structures/DecidableType.vo /usr/lib64/coq/theories/Structures/DecidableTypeEx.v /usr/lib64/coq/theories/Structures/DecidableTypeEx.vo /usr/lib64/coq/theories/Structures/Equalities.v /usr/lib64/coq/theories/Structures/Equalities.vo /usr/lib64/coq/theories/Structures/EqualitiesFacts.v /usr/lib64/coq/theories/Structures/EqualitiesFacts.vo /usr/lib64/coq/theories/Structures/GenericMinMax.v /usr/lib64/coq/theories/Structures/GenericMinMax.vo /usr/lib64/coq/theories/Structures/OrderedType.v /usr/lib64/coq/theories/Structures/OrderedType.vo /usr/lib64/coq/theories/Structures/OrderedTypeAlt.v /usr/lib64/coq/theories/Structures/OrderedTypeAlt.vo /usr/lib64/coq/theories/Structures/OrderedTypeEx.v /usr/lib64/coq/theories/Structures/OrderedTypeEx.vo /usr/lib64/coq/theories/Structures/Orders.v /usr/lib64/coq/theories/Structures/Orders.vo /usr/lib64/coq/theories/Structures/OrdersAlt.v /usr/lib64/coq/theories/Structures/OrdersAlt.vo /usr/lib64/coq/theories/Structures/OrdersEx.v /usr/lib64/coq/theories/Structures/OrdersEx.vo /usr/lib64/coq/theories/Structures/OrdersFacts.v /usr/lib64/coq/theories/Structures/OrdersFacts.vo /usr/lib64/coq/theories/Structures/OrdersLists.v /usr/lib64/coq/theories/Structures/OrdersLists.vo /usr/lib64/coq/theories/Structures/OrdersTac.v /usr/lib64/coq/theories/Structures/OrdersTac.vo /usr/lib64/coq/theories/Unicode /usr/lib64/coq/theories/Unicode/Utf8.v /usr/lib64/coq/theories/Unicode/Utf8.vo /usr/lib64/coq/theories/Unicode/Utf8_core.v /usr/lib64/coq/theories/Unicode/Utf8_core.vo /usr/lib64/coq/theories/Wellfounded /usr/lib64/coq/theories/Wellfounded/Disjoint_Union.v /usr/lib64/coq/theories/Wellfounded/Disjoint_Union.vo /usr/lib64/coq/theories/Wellfounded/Inclusion.v /usr/lib64/coq/theories/Wellfounded/Inclusion.vo /usr/lib64/coq/theories/Wellfounded/Inverse_Image.v /usr/lib64/coq/theories/Wellfounded/Inverse_Image.vo /usr/lib64/coq/theories/Wellfounded/Lexicographic_Exponentiation.v /usr/lib64/coq/theories/Wellfounded/Lexicographic_Exponentiation.vo /usr/lib64/coq/theories/Wellfounded/Lexicographic_Product.v /usr/lib64/coq/theories/Wellfounded/Lexicographic_Product.vo /usr/lib64/coq/theories/Wellfounded/Transitive_Closure.v /usr/lib64/coq/theories/Wellfounded/Transitive_Closure.vo /usr/lib64/coq/theories/Wellfounded/Union.v /usr/lib64/coq/theories/Wellfounded/Union.vo /usr/lib64/coq/theories/Wellfounded/Well_Ordering.v /usr/lib64/coq/theories/Wellfounded/Well_Ordering.vo /usr/lib64/coq/theories/Wellfounded/Wellfounded.v /usr/lib64/coq/theories/Wellfounded/Wellfounded.vo /usr/lib64/coq/theories/ZArith /usr/lib64/coq/theories/ZArith/BinInt.v /usr/lib64/coq/theories/ZArith/BinInt.vo /usr/lib64/coq/theories/ZArith/Int.v /usr/lib64/coq/theories/ZArith/Int.vo /usr/lib64/coq/theories/ZArith/Wf_Z.v /usr/lib64/coq/theories/ZArith/Wf_Z.vo /usr/lib64/coq/theories/ZArith/ZArith.v /usr/lib64/coq/theories/ZArith/ZArith.vo /usr/lib64/coq/theories/ZArith/ZArith_base.v /usr/lib64/coq/theories/ZArith/ZArith_base.vo /usr/lib64/coq/theories/ZArith/ZArith_dec.v /usr/lib64/coq/theories/ZArith/ZArith_dec.vo /usr/lib64/coq/theories/ZArith/ZOdiv.v /usr/lib64/coq/theories/ZArith/ZOdiv.vo /usr/lib64/coq/theories/ZArith/ZOdiv_def.v /usr/lib64/coq/theories/ZArith/ZOdiv_def.vo /usr/lib64/coq/theories/ZArith/ZOrderedType.v /usr/lib64/coq/theories/ZArith/ZOrderedType.vo /usr/lib64/coq/theories/ZArith/Zabs.v /usr/lib64/coq/theories/ZArith/Zabs.vo /usr/lib64/coq/theories/ZArith/Zbool.v /usr/lib64/coq/theories/ZArith/Zbool.vo /usr/lib64/coq/theories/ZArith/Zcompare.v /usr/lib64/coq/theories/ZArith/Zcompare.vo /usr/lib64/coq/theories/ZArith/Zcomplements.v /usr/lib64/coq/theories/ZArith/Zcomplements.vo /usr/lib64/coq/theories/ZArith/Zdigits.v /usr/lib64/coq/theories/ZArith/Zdigits.vo /usr/lib64/coq/theories/ZArith/Zdiv.v /usr/lib64/coq/theories/ZArith/Zdiv.vo /usr/lib64/coq/theories/ZArith/Zeven.v /usr/lib64/coq/theories/ZArith/Zeven.vo /usr/lib64/coq/theories/ZArith/Zgcd_alt.v /usr/lib64/coq/theories/ZArith/Zgcd_alt.vo /usr/lib64/coq/theories/ZArith/Zhints.v /usr/lib64/coq/theories/ZArith/Zhints.vo /usr/lib64/coq/theories/ZArith/Zlogarithm.v /usr/lib64/coq/theories/ZArith/Zlogarithm.vo /usr/lib64/coq/theories/ZArith/Zmax.v /usr/lib64/coq/theories/ZArith/Zmax.vo /usr/lib64/coq/theories/ZArith/Zmin.v /usr/lib64/coq/theories/ZArith/Zmin.vo /usr/lib64/coq/theories/ZArith/Zminmax.v /usr/lib64/coq/theories/ZArith/Zminmax.vo /usr/lib64/coq/theories/ZArith/Zmisc.v /usr/lib64/coq/theories/ZArith/Zmisc.vo /usr/lib64/coq/theories/ZArith/Znat.v /usr/lib64/coq/theories/ZArith/Znat.vo /usr/lib64/coq/theories/ZArith/Znumtheory.v /usr/lib64/coq/theories/ZArith/Znumtheory.vo /usr/lib64/coq/theories/ZArith/Zorder.v /usr/lib64/coq/theories/ZArith/Zorder.vo /usr/lib64/coq/theories/ZArith/Zpow_def.v /usr/lib64/coq/theories/ZArith/Zpow_def.vo /usr/lib64/coq/theories/ZArith/Zpow_facts.v /usr/lib64/coq/theories/ZArith/Zpow_facts.vo /usr/lib64/coq/theories/ZArith/Zpower.v /usr/lib64/coq/theories/ZArith/Zpower.vo /usr/lib64/coq/theories/ZArith/Zsqrt.v /usr/lib64/coq/theories/ZArith/Zsqrt.vo /usr/lib64/coq/theories/ZArith/Zwf.v /usr/lib64/coq/theories/ZArith/Zwf.vo /usr/lib64/coq/theories/ZArith/auxiliary.v /usr/lib64/coq/theories/ZArith/auxiliary.vo /usr/lib64/coq/tools /usr/lib64/coq/tools/coqdoc /usr/lib64/coq/tools/coqdoc/coqdoc.css /usr/lib64/coq/tools/coqdoc/coqdoc.sty /usr/lib64/coq/toplevel /usr/lib64/coq/toplevel/auto_ind_decl.cmi /usr/lib64/coq/toplevel/autoinstance.cmi /usr/lib64/coq/toplevel/cerrors.cmi /usr/lib64/coq/toplevel/class.cmi /usr/lib64/coq/toplevel/classes.cmi /usr/lib64/coq/toplevel/command.cmi /usr/lib64/coq/toplevel/coqinit.cmi /usr/lib64/coq/toplevel/coqtop.cmi /usr/lib64/coq/toplevel/discharge.cmi /usr/lib64/coq/toplevel/himsg.cmi /usr/lib64/coq/toplevel/ind_tables.cmi /usr/lib64/coq/toplevel/indschemes.cmi /usr/lib64/coq/toplevel/lemmas.cmi /usr/lib64/coq/toplevel/libtypes.cmi /usr/lib64/coq/toplevel/metasyntax.cmi /usr/lib64/coq/toplevel/mltop.cmi /usr/lib64/coq/toplevel/record.cmi /usr/lib64/coq/toplevel/search.cmi /usr/lib64/coq/toplevel/toplevel.cma /usr/lib64/coq/toplevel/toplevel.cmi /usr/lib64/coq/toplevel/usage.cmi /usr/lib64/coq/toplevel/vernac.cmi /usr/lib64/coq/toplevel/vernacentries.cmi /usr/lib64/coq/toplevel/vernacexpr.cmi /usr/lib64/coq/toplevel/vernacinterp.cmi /usr/lib64/coq/toplevel/whelp.cmi /usr/lib64/coq/user-contrib /usr/share/doc/coq-8.3pl2 /usr/share/doc/coq-8.3pl2/CHANGES /usr/share/doc/coq-8.3pl2/COMPATIBILITY /usr/share/doc/coq-8.3pl2/COPYRIGHT /usr/share/doc/coq-8.3pl2/CREDITS /usr/share/doc/coq-8.3pl2/INSTALL /usr/share/doc/coq-8.3pl2/LICENSE /usr/share/doc/coq-8.3pl2/README /usr/share/man/man1/coq-tex.1.gz /usr/share/man/man1/coq_makefile.1.gz /usr/share/man/man1/coqc.1.gz /usr/share/man/man1/coqchk.1.gz /usr/share/man/man1/coqdep.1.gz /usr/share/man/man1/coqdoc.1.gz /usr/share/man/man1/coqide.1.gz /usr/share/man/man1/coqmktop.1.gz /usr/share/man/man1/coqtop.1.gz /usr/share/man/man1/coqtop.byte.1.gz /usr/share/man/man1/coqtop.opt.1.gz /usr/share/man/man1/coqwc.1.gz /usr/share/man/man1/gallina.1.gz /usr/share/texmf/tex/latex/misc/coqdoc.sty
Generated by rpm2html 1.8.1
Fabrice Bellet, Mon May 20 07:32:46 2013