Index | index by Group | index by Distribution | index by Vendor | index by creation date | index by Name | Mirrors | Help | Search |
Name: coq-doc | Distribution: SUSE Linux Enterprise 15 SP4 |
Version: 8.13.2 | Vendor: openSUSE |
Release: bp154.1.1 | Build date: Thu Mar 17 17:17:11 2022 |
Group: Documentation/HTML | Build host: armbuild22 |
Size: 103355024 | Source RPM: coq-8.13.2-bp154.1.1.src.rpm |
Packager: https://bugs.opensuse.org | |
Url: https://coq.inria.fr/ | |
Summary: Documentation for coq |
HTML reference manual for Coq and full documentation of the standard library.
LGPL-2.1-only
* Sat Sep 04 2021 Aaron Puchert <aaronpuchert@alice-dsl.net> - Add documentation package based on github.com/coq/doc until we can build the documentation directly in OBS. * Mon Apr 12 2021 Aaron Puchert <aaronpuchert@alice-dsl.net> - Update to version 8.13.2. * Fix crash when using vm_compute on an irreducible PArray.set. * Fix crash when loading .vo files containing a vm_compute normalized primitive array. * Fix Ltac2.Array.init computational complexity. * Thu Feb 25 2021 Aaron Puchert <aaronpuchert@alice-dsl.net> - Update to version 8.13.1. * Fix arities of VM opcodes for some floating-point operations that could cause memory corruption. * Sun Feb 07 2021 Aaron Puchert <aaronpuchert@alice-dsl.net> - Update to version 8.13.0. * Introduction of primitive persistent arrays in the core language, implemented using imperative persistent arrays. * Introduction of definitional proof irrelevance for the equality type defined in the SProp sort. * Cumulative record and inductive type declarations can now specify the variance of their universes. * Various bugfixes and uniformization of behavior with respect to the use of implicit arguments and the handling of existential variables in declarations, unification and tactics. * New warning for unused variables in catch-all match branches that match multiple distinct patterns. * New warning for Hint commands outside sections without a locality attribute, whose goal is to eventually remove the fragile default behavior of importing hints only when using Require. The recommended fix is to declare hints as export, instead of the current default global, meaning that they are imported through Require Import only, not Require. * General support for boolean attributes. * Many improvements to the handling of notations, including number notations, recursive notations and notations with bindings. A new algorithm chooses the most precise notation available to print an expression, which might introduce changes in printing behavior. * Tactic improvements in lia and its zify preprocessing step, now supporting reasoning on boolean operators such as Z.leb and supporting primitive integers Int63. * Typing flags can now be specified per-constant / inductive. * Improvements to the reference manual including updated syntax descriptions that match Coq's grammar in several chapters, and splitting parts of the tactics chapter to independent sections. - Add build flag to turn off building of the IDE. * Sun Dec 13 2020 Aaron Puchert <aaronpuchert@alice-dsl.net> - Update to version 8.12.2. Fixes two impacting 8.12 regressions: * Fixed a regression causing notations mentioning a coercion to be ignored. * Fixed a regression causing incomplete inference of implicit arguments in exists. * Tue Nov 17 2020 Aaron Puchert <aaronpuchert@alice-dsl.net> - Update to version 8.12.1. This contains mostly bug fixes: * Polymorphic side-effects inside monomorphic definitions were incorrectly handled as not inlined. This allowed deriving an inconsistency. * Regression in error reporting after SSReflect's case tactic. A generic error message "Could not fill dependent hole in apply" was reported for any error following case or elim. * Several bugs with Search. * The details environment introduced in coqdoc in Coq 8.12 can now be used as advertised in the reference manual. * View menu "Display parentheses" introduced in CoqIDE in Coq 8.12 now works correctly. * Thu Aug 20 2020 Martin Liška <mliska@suse.cz> - Use memoryperjob constraint instead of %limit_build macro. * Tue Jul 28 2020 Aaron Puchert <aaronpuchert@alice-dsl.net> - Update to version 8.12.0. * New binder notation for non-maximal implicit arguments using [] allowing to set and see the implicit status of arguments immediately. * New notation Inductive "I A | x : s := ..." to distinguish the uniform from the non-uniform parameters in inductive definitions. * More robust and expressive treatment of implicit inductive parameters in inductive declarations. * Improvements in the treatment of implicit arguments and partially applied constants in notations, parsing of hexadecimal number notation and better handling of scopes and coercions for printing. * A correct and efficient coercion coherence checking algorithm, avoiding spurious or duplicate warnings. * An improved Search command which accepts complex queries. This takes precedence over the now deprecated ssreflect search. * Many additions and improvements of the standard library. * Improvements to the reference manual include a more logical organization of chapters along with updated syntax descriptions that match Coq's grammar in most but not all chapters. * Sat Jun 06 2020 Aaron Puchert <aaronpuchert@alice-dsl.net> - Update to version 8.11.2. * Fixed a kernel issue where using Require inside a section caused an anomaly when closing the section. * Fixed normalization in conclusion of custom induction scheme. * Fixed a loss of location of some tactic errors. * Ignore -native-compiler option when built without native compute support. * Fixed a segfault issue with CoqIDE completion. * Highlighting style is now consistently applied to all three buffers of CoqIDE. * Wed Apr 08 2020 Aaron Puchert <aaronpuchert@alice-dsl.net> - Update to version 8.11.1, with upstream support for OCaml 4.10. * Allow more inductive types in Unset Positivity Checking mode. * Fixed bugs in dealing with precedence of notations in custom entries. * In primitive floats, print a warning when parsing a decimal value that is not exactly a binary64 floating-point number. For instance, parsing 0.1 will print a warning whereas parsing 0.5 won't. * Fixed an issue in CoqIDE about compiling file paths containing spaces. * Fixed an issue where Extraction Implicit on the constructor of a record was leading to an anomaly. - Remove now obsolete ocaml-410-build.patch. * Sun Mar 29 2020 Aaron Puchert <aaronpuchert@alice-dsl.net> - The num library is required for OCaml 4.06 or later. - Add ocaml-410-build.patch: fix build with OCaml 4.10. * Thu Feb 06 2020 Aaron Puchert <aaronpuchert@alice-dsl.net> - Update to version 8.11.0. * Ltac2, a new tactic language for writing more robust larger scale tactics, with built-in support for datatypes and the multi-goal tactic monad. * Primitive floats are integrated in terms and follow the binary64 format of the IEEE 754 standard, as specified in the Coq.Float.Floats library. * Many other cleanups and improvements have been performed and are further described in the changelog. * Special note on compatibility: Fixed bugs of Export and Import that can have a significant impact on user developments. - Drop unneeded empty *.vos files. * Sat Nov 30 2019 Aaron Puchert <aaronpuchert@alice-dsl.net> - Update to version 8.10.2. * Fixed a critical bug of template polymorphism and nonlinear universes; * Fixed a few anomalies; * Fixed an 8.10 regression related to the printing of coercions associated to notations; * Fixed uneven dimensions of CoqIDE panels when window has been resized; * Fixed queries in CoqIDE. * Tue Nov 12 2019 Aaron Puchert <aaronpuchert@alice-dsl.net> - Update to version 8.10.0. * some quality-of-life bug fixes; * a critical bug fix related to template polymorphism; * native 63-bit machine integers; * a new sort of definitionally proof-irrelevant propositions: SProp; * private universes for opaque polymorphic constants; * string notations and numeral notations; * a new simplex-based proof engine for the tactics lia, nia, lra and nra; * new introduction patterns for SSReflect; * a tactic to rewrite under binders: under; * easy input of non-ASCII symbols in CoqIDE, which now uses GTK3. - Update to version 8.10.1. * Fix proof of False when using SProp * Fix an anomaly when unsolved evar in Add Ring * Fix Ltac regression in binding free names in uconstr * Fix handling of unicode input before space * Fix custom extraction of inductives to JSON - Update version requirements. * Tue Nov 12 2019 Aaron Puchert <aaronpuchert@alice-dsl.net> - Fix findlib build dependency. * Sun Nov 03 2019 Aaron Puchert <aaronpuchert@alice-dsl.net> - Use memory-constraints package to limit number of threads. - Add dependencies to fix installation issues. * Wed Sep 25 2019 Aaron Puchert <aaronpuchert@alice-dsl.net> - Prevent OOM by limiting the number of threads. * Tue Sep 24 2019 Aaron Puchert <aaronpuchert@alice-dsl.net> - Change license tag to LGPL-2.1-only. - Remove obsolete %defattr and other spec-cleaner suggestions. * Sat Aug 03 2019 Aaron Puchert <aaronpuchert@alice-dsl.net> - Update to version 8.9.0. * Kernel: mutually recursive records are now supported. * Notations: + Support for autonomous grammars of terms called “custom entries”. + Deprecated notations of the standard library will be removed in the next version of Coq, see the next subsection for a script to ease porting. + Added the "Numeral Notation" command for registering decimal numeral notations for custom types. * Tactics: Introduction tactics intro/intros on a goal that is an existential variable now force a refinement of the goal into a dependent product rather than failing. * Decision procedures: deprecation of tactic romega in favor of lia and removal of fourier, replaced by lra which subsumes it. * Proof language: focusing bracket { now supports named goals, e.g. [x]:{ will focus on a goal (existential variable) named x. * SSReflect: the implementation of delayed clear was simplified: the variables are always renamed using inaccessible names when the clear switch is processed and finally cleared at the end of the intro pattern. In addition to that, the use-and-discard flag {} typical of rewrite rules can now be also applied to views, e.g. => {}/v applies v and then clears v. See Section Introduction in the context. * Vernacular: + Experimental support for attributes on commands, as in "#[local] Lemma foo : bar". Tactics and tactic notations now support the deprecated attribute. + Removed deprecated commands "Arguments Scope" and "Implicit Arguments" in favor of "Arguments (scopes)" and "Arguments (implicits)". + New flag "Uniform Inductive Parameters" to avoid repeating uniform parameters in constructor declarations. + New commands "Hint Variables" and "Hint Constants" for controlling the opacity status of variables and constants in hint databases. It is recommended to always use these commands after creating a hint database with Create HintDb. + Multiple sections with the same name are now allowed. * Library: additions and changes in the VectorDef, Ascii, and String libraries. Syntax notations are now available only when using "Import" of libraries and not merely "Require". (Source of incompatibility, see Change Log for details) * Toplevels: coqtop and coqide can now display diffs between proof steps in color, using the Diffs option. * Documentation: we integrated a large number of fixes to the new Sphinx documentation. * Tools: removed gallina utility and homebrewed Emacs mode. - Update to version 8.9.1, which contains * some quality-of-life bug fixes, * many improvements to the documentation, * a critical bug fix related to primitive projections and native_compute. - Remove unnecessary dependencies: ncurses-devel is no longer needed, and the docs aren't build with TeX and hevea anymore. - Remove dependencies that are automatically detected. - Remove icon that is also available from the tarball. - Replace some identical files by symlinks. - Fix executable bits and shebangs. - Separate runtime from devel files by ending. - Use %license for LICENSE and CREDITS. - Be more explicit in %files. - Add mime type for Coq source files so they open with the IDE. - Add rpmlintrc for issues that are hard to fix. * Thu Oct 11 2018 ptrommler@icloud.com - update to 8.8.2 * Sun Jan 07 2018 ptrommler@icloud.com - update to 8.7.1 * Thu Nov 02 2017 ptrommler@icloud.com - update to 8.7.0 * I need this in class b/c coq-ide reads _CoqProject files * Thu Apr 13 2017 peter.trommler@ohm-hochschule.de - update to 8.6 from upstream * Fri Dec 02 2016 peter.trommler@ohm-hochschule.de - update to 8.5pl3 from upstream * Fri Oct 21 2016 peter.trommler@ohm-hochschule.de - update to 8.5pl2 from upstream * Sun Apr 10 2016 peter.trommler@ohm-hochschule.de - update to 8.5 from upstream
/usr/share/doc/packages/coq/refman /usr/share/doc/packages/coq/refman/.buildinfo /usr/share/doc/packages/coq/refman/_images /usr/share/doc/packages/coq/refman/_images/coqide-queries.png /usr/share/doc/packages/coq/refman/_images/coqide.png /usr/share/doc/packages/coq/refman/_images/diffs-coqide-compacted.png /usr/share/doc/packages/coq/refman/_images/diffs-coqide-multigoal.png /usr/share/doc/packages/coq/refman/_images/diffs-coqide-on.png /usr/share/doc/packages/coq/refman/_images/diffs-coqide-removed.png /usr/share/doc/packages/coq/refman/_images/diffs-coqtop-on3.png /usr/share/doc/packages/coq/refman/_images/diffs-error-message.png /usr/share/doc/packages/coq/refman/_images/diffs-show-proof.png /usr/share/doc/packages/coq/refman/_static /usr/share/doc/packages/coq/refman/_static/CoqNotations.ttf /usr/share/doc/packages/coq/refman/_static/ansi-dark.css /usr/share/doc/packages/coq/refman/_static/ansi.css /usr/share/doc/packages/coq/refman/_static/basic.css /usr/share/doc/packages/coq/refman/_static/coqdoc.css /usr/share/doc/packages/coq/refman/_static/coqide-queries.png /usr/share/doc/packages/coq/refman/_static/coqide.png /usr/share/doc/packages/coq/refman/_static/coqnotations.sty /usr/share/doc/packages/coq/refman/_static/css /usr/share/doc/packages/coq/refman/_static/css/badge_only.css /usr/share/doc/packages/coq/refman/_static/css/theme.css /usr/share/doc/packages/coq/refman/_static/diffs-coqide-compacted.png /usr/share/doc/packages/coq/refman/_static/diffs-coqide-multigoal.png /usr/share/doc/packages/coq/refman/_static/diffs-coqide-on.png /usr/share/doc/packages/coq/refman/_static/diffs-coqide-removed.png /usr/share/doc/packages/coq/refman/_static/diffs-coqtop-compacted.png /usr/share/doc/packages/coq/refman/_static/diffs-coqtop-multigoal.png /usr/share/doc/packages/coq/refman/_static/diffs-coqtop-on.png /usr/share/doc/packages/coq/refman/_static/diffs-coqtop-on3.png /usr/share/doc/packages/coq/refman/_static/diffs-error-message.png /usr/share/doc/packages/coq/refman/_static/diffs-show-proof.png /usr/share/doc/packages/coq/refman/_static/doctools.js /usr/share/doc/packages/coq/refman/_static/documentation_options.js /usr/share/doc/packages/coq/refman/_static/file.png /usr/share/doc/packages/coq/refman/_static/fonts /usr/share/doc/packages/coq/refman/_static/fonts/Inconsolata-Bold.ttf /usr/share/doc/packages/coq/refman/_static/fonts/Inconsolata-Regular.ttf /usr/share/doc/packages/coq/refman/_static/fonts/Inconsolata.ttf /usr/share/doc/packages/coq/refman/_static/fonts/Lato /usr/share/doc/packages/coq/refman/_static/fonts/Lato-Bold.ttf /usr/share/doc/packages/coq/refman/_static/fonts/Lato-Regular.ttf /usr/share/doc/packages/coq/refman/_static/fonts/Lato/lato-bold.eot /usr/share/doc/packages/coq/refman/_static/fonts/Lato/lato-bold.ttf /usr/share/doc/packages/coq/refman/_static/fonts/Lato/lato-bold.woff /usr/share/doc/packages/coq/refman/_static/fonts/Lato/lato-bold.woff2 /usr/share/doc/packages/coq/refman/_static/fonts/Lato/lato-bolditalic.eot /usr/share/doc/packages/coq/refman/_static/fonts/Lato/lato-bolditalic.ttf /usr/share/doc/packages/coq/refman/_static/fonts/Lato/lato-bolditalic.woff /usr/share/doc/packages/coq/refman/_static/fonts/Lato/lato-bolditalic.woff2 /usr/share/doc/packages/coq/refman/_static/fonts/Lato/lato-italic.eot /usr/share/doc/packages/coq/refman/_static/fonts/Lato/lato-italic.ttf /usr/share/doc/packages/coq/refman/_static/fonts/Lato/lato-italic.woff /usr/share/doc/packages/coq/refman/_static/fonts/Lato/lato-italic.woff2 /usr/share/doc/packages/coq/refman/_static/fonts/Lato/lato-regular.eot /usr/share/doc/packages/coq/refman/_static/fonts/Lato/lato-regular.ttf /usr/share/doc/packages/coq/refman/_static/fonts/Lato/lato-regular.woff /usr/share/doc/packages/coq/refman/_static/fonts/Lato/lato-regular.woff2 /usr/share/doc/packages/coq/refman/_static/fonts/RobotoSlab /usr/share/doc/packages/coq/refman/_static/fonts/RobotoSlab-Bold.ttf /usr/share/doc/packages/coq/refman/_static/fonts/RobotoSlab-Regular.ttf /usr/share/doc/packages/coq/refman/_static/fonts/RobotoSlab/roboto-slab-v7-bold.eot /usr/share/doc/packages/coq/refman/_static/fonts/RobotoSlab/roboto-slab-v7-bold.ttf /usr/share/doc/packages/coq/refman/_static/fonts/RobotoSlab/roboto-slab-v7-bold.woff /usr/share/doc/packages/coq/refman/_static/fonts/RobotoSlab/roboto-slab-v7-bold.woff2 /usr/share/doc/packages/coq/refman/_static/fonts/RobotoSlab/roboto-slab-v7-regular.eot /usr/share/doc/packages/coq/refman/_static/fonts/RobotoSlab/roboto-slab-v7-regular.ttf /usr/share/doc/packages/coq/refman/_static/fonts/RobotoSlab/roboto-slab-v7-regular.woff /usr/share/doc/packages/coq/refman/_static/fonts/RobotoSlab/roboto-slab-v7-regular.woff2 /usr/share/doc/packages/coq/refman/_static/fonts/fontawesome-webfont.eot /usr/share/doc/packages/coq/refman/_static/fonts/fontawesome-webfont.svg /usr/share/doc/packages/coq/refman/_static/fonts/fontawesome-webfont.ttf /usr/share/doc/packages/coq/refman/_static/fonts/fontawesome-webfont.woff /usr/share/doc/packages/coq/refman/_static/fonts/fontawesome-webfont.woff2 /usr/share/doc/packages/coq/refman/_static/jquery-3.4.1.js /usr/share/doc/packages/coq/refman/_static/jquery.js /usr/share/doc/packages/coq/refman/_static/js /usr/share/doc/packages/coq/refman/_static/js/modernizr.min.js /usr/share/doc/packages/coq/refman/_static/js/theme.js /usr/share/doc/packages/coq/refman/_static/language_data.js /usr/share/doc/packages/coq/refman/_static/minus.png /usr/share/doc/packages/coq/refman/_static/notations.css /usr/share/doc/packages/coq/refman/_static/notations.js /usr/share/doc/packages/coq/refman/_static/plus.png /usr/share/doc/packages/coq/refman/_static/pre-text.css /usr/share/doc/packages/coq/refman/_static/pygments.css /usr/share/doc/packages/coq/refman/_static/searchtools.js /usr/share/doc/packages/coq/refman/_static/underscore-1.3.1.js /usr/share/doc/packages/coq/refman/_static/underscore.js /usr/share/doc/packages/coq/refman/addendum /usr/share/doc/packages/coq/refman/addendum/canonical-structures.html /usr/share/doc/packages/coq/refman/addendum/extended-pattern-matching.html /usr/share/doc/packages/coq/refman/addendum/extraction.html /usr/share/doc/packages/coq/refman/addendum/generalized-rewriting.html /usr/share/doc/packages/coq/refman/addendum/implicit-coercions.html /usr/share/doc/packages/coq/refman/addendum/micromega.html /usr/share/doc/packages/coq/refman/addendum/miscellaneous-extensions.html /usr/share/doc/packages/coq/refman/addendum/nsatz.html /usr/share/doc/packages/coq/refman/addendum/omega.html /usr/share/doc/packages/coq/refman/addendum/parallel-proof-processing.html /usr/share/doc/packages/coq/refman/addendum/program.html /usr/share/doc/packages/coq/refman/addendum/ring.html /usr/share/doc/packages/coq/refman/addendum/sprop.html /usr/share/doc/packages/coq/refman/addendum/type-classes.html /usr/share/doc/packages/coq/refman/addendum/universe-polymorphism.html /usr/share/doc/packages/coq/refman/appendix /usr/share/doc/packages/coq/refman/appendix/history-and-changes /usr/share/doc/packages/coq/refman/appendix/history-and-changes/index.html /usr/share/doc/packages/coq/refman/appendix/indexes /usr/share/doc/packages/coq/refman/appendix/indexes/index.html /usr/share/doc/packages/coq/refman/changes.html /usr/share/doc/packages/coq/refman/coq-attrindex.html /usr/share/doc/packages/coq/refman/coq-cmdindex.html /usr/share/doc/packages/coq/refman/coq-exnindex.html /usr/share/doc/packages/coq/refman/coq-optindex.html /usr/share/doc/packages/coq/refman/coq-tacindex.html /usr/share/doc/packages/coq/refman/coq-thmindex.html /usr/share/doc/packages/coq/refman/genindex.html /usr/share/doc/packages/coq/refman/history.html /usr/share/doc/packages/coq/refman/index.html /usr/share/doc/packages/coq/refman/language /usr/share/doc/packages/coq/refman/language/cic.html /usr/share/doc/packages/coq/refman/language/coq-library.html /usr/share/doc/packages/coq/refman/language/core /usr/share/doc/packages/coq/refman/language/core/assumptions.html /usr/share/doc/packages/coq/refman/language/core/basic.html /usr/share/doc/packages/coq/refman/language/core/coinductive.html /usr/share/doc/packages/coq/refman/language/core/conversion.html /usr/share/doc/packages/coq/refman/language/core/definitions.html /usr/share/doc/packages/coq/refman/language/core/index.html /usr/share/doc/packages/coq/refman/language/core/inductive.html /usr/share/doc/packages/coq/refman/language/core/modules.html /usr/share/doc/packages/coq/refman/language/core/primitive.html /usr/share/doc/packages/coq/refman/language/core/records.html /usr/share/doc/packages/coq/refman/language/core/sections.html /usr/share/doc/packages/coq/refman/language/core/sorts.html /usr/share/doc/packages/coq/refman/language/core/variants.html /usr/share/doc/packages/coq/refman/language/extensions /usr/share/doc/packages/coq/refman/language/extensions/arguments-command.html /usr/share/doc/packages/coq/refman/language/extensions/canonical.html /usr/share/doc/packages/coq/refman/language/extensions/evars.html /usr/share/doc/packages/coq/refman/language/extensions/implicit-arguments.html /usr/share/doc/packages/coq/refman/language/extensions/index.html /usr/share/doc/packages/coq/refman/language/extensions/match.html /usr/share/doc/packages/coq/refman/language/gallina-extensions.html /usr/share/doc/packages/coq/refman/language/gallina-specification-language.html /usr/share/doc/packages/coq/refman/language/module-system.html /usr/share/doc/packages/coq/refman/license.html /usr/share/doc/packages/coq/refman/objects.inv /usr/share/doc/packages/coq/refman/practical-tools /usr/share/doc/packages/coq/refman/practical-tools/coq-commands.html /usr/share/doc/packages/coq/refman/practical-tools/coqide.html /usr/share/doc/packages/coq/refman/practical-tools/utilities.html /usr/share/doc/packages/coq/refman/proof-engine /usr/share/doc/packages/coq/refman/proof-engine/detailed-tactic-examples.html /usr/share/doc/packages/coq/refman/proof-engine/ltac.html /usr/share/doc/packages/coq/refman/proof-engine/ltac2.html /usr/share/doc/packages/coq/refman/proof-engine/proof-handling.html /usr/share/doc/packages/coq/refman/proof-engine/ssreflect-proof-language.html /usr/share/doc/packages/coq/refman/proof-engine/tactics.html /usr/share/doc/packages/coq/refman/proof-engine/vernacular-commands.html /usr/share/doc/packages/coq/refman/proofs /usr/share/doc/packages/coq/refman/proofs/automatic-tactics /usr/share/doc/packages/coq/refman/proofs/automatic-tactics/auto.html /usr/share/doc/packages/coq/refman/proofs/automatic-tactics/index.html /usr/share/doc/packages/coq/refman/proofs/automatic-tactics/logic.html /usr/share/doc/packages/coq/refman/proofs/creating-tactics /usr/share/doc/packages/coq/refman/proofs/creating-tactics/index.html /usr/share/doc/packages/coq/refman/proofs/writing-proofs /usr/share/doc/packages/coq/refman/proofs/writing-proofs/index.html /usr/share/doc/packages/coq/refman/proofs/writing-proofs/proof-mode.html /usr/share/doc/packages/coq/refman/proofs/writing-proofs/rewriting.html /usr/share/doc/packages/coq/refman/search.html /usr/share/doc/packages/coq/refman/searchindex.js /usr/share/doc/packages/coq/refman/std-glossindex.html /usr/share/doc/packages/coq/refman/user-extensions /usr/share/doc/packages/coq/refman/user-extensions/proof-schemes.html /usr/share/doc/packages/coq/refman/user-extensions/syntax-extensions.html /usr/share/doc/packages/coq/refman/using /usr/share/doc/packages/coq/refman/using/libraries /usr/share/doc/packages/coq/refman/using/libraries/funind.html /usr/share/doc/packages/coq/refman/using/libraries/index.html /usr/share/doc/packages/coq/refman/using/libraries/writing.html /usr/share/doc/packages/coq/refman/using/tools /usr/share/doc/packages/coq/refman/using/tools/coqdoc.html /usr/share/doc/packages/coq/refman/using/tools/index.html /usr/share/doc/packages/coq/refman/zebibliography.html /usr/share/doc/packages/coq/stdlib /usr/share/doc/packages/coq/stdlib/Coq.Arith.Arith.html /usr/share/doc/packages/coq/stdlib/Coq.Arith.Arith_base.html /usr/share/doc/packages/coq/stdlib/Coq.Arith.Between.html /usr/share/doc/packages/coq/stdlib/Coq.Arith.Bool_nat.html /usr/share/doc/packages/coq/stdlib/Coq.Arith.Compare.html /usr/share/doc/packages/coq/stdlib/Coq.Arith.Compare_dec.html /usr/share/doc/packages/coq/stdlib/Coq.Arith.Div2.html /usr/share/doc/packages/coq/stdlib/Coq.Arith.EqNat.html /usr/share/doc/packages/coq/stdlib/Coq.Arith.Euclid.html /usr/share/doc/packages/coq/stdlib/Coq.Arith.Even.html /usr/share/doc/packages/coq/stdlib/Coq.Arith.Factorial.html /usr/share/doc/packages/coq/stdlib/Coq.Arith.Gt.html /usr/share/doc/packages/coq/stdlib/Coq.Arith.Le.html /usr/share/doc/packages/coq/stdlib/Coq.Arith.Lt.html /usr/share/doc/packages/coq/stdlib/Coq.Arith.Max.html /usr/share/doc/packages/coq/stdlib/Coq.Arith.Min.html /usr/share/doc/packages/coq/stdlib/Coq.Arith.Minus.html /usr/share/doc/packages/coq/stdlib/Coq.Arith.Mult.html /usr/share/doc/packages/coq/stdlib/Coq.Arith.PeanoNat.html /usr/share/doc/packages/coq/stdlib/Coq.Arith.Peano_dec.html /usr/share/doc/packages/coq/stdlib/Coq.Arith.Plus.html /usr/share/doc/packages/coq/stdlib/Coq.Arith.Wf_nat.html /usr/share/doc/packages/coq/stdlib/Coq.Array.PArray.html /usr/share/doc/packages/coq/stdlib/Coq.Bool.Bool.html /usr/share/doc/packages/coq/stdlib/Coq.Bool.BoolEq.html /usr/share/doc/packages/coq/stdlib/Coq.Bool.BoolOrder.html /usr/share/doc/packages/coq/stdlib/Coq.Bool.Bvector.html /usr/share/doc/packages/coq/stdlib/Coq.Bool.DecBool.html /usr/share/doc/packages/coq/stdlib/Coq.Bool.IfProp.html /usr/share/doc/packages/coq/stdlib/Coq.Bool.Sumbool.html /usr/share/doc/packages/coq/stdlib/Coq.Bool.Zerob.html /usr/share/doc/packages/coq/stdlib/Coq.Classes.CEquivalence.html /usr/share/doc/packages/coq/stdlib/Coq.Classes.CMorphisms.html /usr/share/doc/packages/coq/stdlib/Coq.Classes.CRelationClasses.html /usr/share/doc/packages/coq/stdlib/Coq.Classes.DecidableClass.html /usr/share/doc/packages/coq/stdlib/Coq.Classes.EquivDec.html /usr/share/doc/packages/coq/stdlib/Coq.Classes.Equivalence.html /usr/share/doc/packages/coq/stdlib/Coq.Classes.Init.html /usr/share/doc/packages/coq/stdlib/Coq.Classes.Morphisms.html /usr/share/doc/packages/coq/stdlib/Coq.Classes.Morphisms_Prop.html /usr/share/doc/packages/coq/stdlib/Coq.Classes.Morphisms_Relations.html /usr/share/doc/packages/coq/stdlib/Coq.Classes.RelationClasses.html /usr/share/doc/packages/coq/stdlib/Coq.Classes.RelationPairs.html /usr/share/doc/packages/coq/stdlib/Coq.Classes.SetoidClass.html /usr/share/doc/packages/coq/stdlib/Coq.Classes.SetoidDec.html /usr/share/doc/packages/coq/stdlib/Coq.Classes.SetoidTactics.html /usr/share/doc/packages/coq/stdlib/Coq.Compat.AdmitAxiom.html /usr/share/doc/packages/coq/stdlib/Coq.Compat.Coq811.html /usr/share/doc/packages/coq/stdlib/Coq.Compat.Coq812.html /usr/share/doc/packages/coq/stdlib/Coq.Compat.Coq813.html /usr/share/doc/packages/coq/stdlib/Coq.FSets.FMapAVL.html /usr/share/doc/packages/coq/stdlib/Coq.FSets.FMapFacts.html /usr/share/doc/packages/coq/stdlib/Coq.FSets.FMapFullAVL.html /usr/share/doc/packages/coq/stdlib/Coq.FSets.FMapInterface.html /usr/share/doc/packages/coq/stdlib/Coq.FSets.FMapList.html /usr/share/doc/packages/coq/stdlib/Coq.FSets.FMapPositive.html /usr/share/doc/packages/coq/stdlib/Coq.FSets.FMapWeakList.html /usr/share/doc/packages/coq/stdlib/Coq.FSets.FMaps.html /usr/share/doc/packages/coq/stdlib/Coq.FSets.FSetAVL.html /usr/share/doc/packages/coq/stdlib/Coq.FSets.FSetBridge.html /usr/share/doc/packages/coq/stdlib/Coq.FSets.FSetCompat.html /usr/share/doc/packages/coq/stdlib/Coq.FSets.FSetDecide.html /usr/share/doc/packages/coq/stdlib/Coq.FSets.FSetEqProperties.html /usr/share/doc/packages/coq/stdlib/Coq.FSets.FSetFacts.html /usr/share/doc/packages/coq/stdlib/Coq.FSets.FSetInterface.html /usr/share/doc/packages/coq/stdlib/Coq.FSets.FSetList.html /usr/share/doc/packages/coq/stdlib/Coq.FSets.FSetPositive.html /usr/share/doc/packages/coq/stdlib/Coq.FSets.FSetProperties.html /usr/share/doc/packages/coq/stdlib/Coq.FSets.FSetToFiniteSet.html /usr/share/doc/packages/coq/stdlib/Coq.FSets.FSetWeakList.html /usr/share/doc/packages/coq/stdlib/Coq.FSets.FSets.html /usr/share/doc/packages/coq/stdlib/Coq.Floats.FloatAxioms.html /usr/share/doc/packages/coq/stdlib/Coq.Floats.FloatClass.html /usr/share/doc/packages/coq/stdlib/Coq.Floats.FloatLemmas.html /usr/share/doc/packages/coq/stdlib/Coq.Floats.FloatOps.html /usr/share/doc/packages/coq/stdlib/Coq.Floats.Floats.html /usr/share/doc/packages/coq/stdlib/Coq.Floats.PrimFloat.html /usr/share/doc/packages/coq/stdlib/Coq.Floats.SpecFloat.html /usr/share/doc/packages/coq/stdlib/Coq.Init.Byte.html /usr/share/doc/packages/coq/stdlib/Coq.Init.Datatypes.html /usr/share/doc/packages/coq/stdlib/Coq.Init.Decimal.html /usr/share/doc/packages/coq/stdlib/Coq.Init.Hexadecimal.html /usr/share/doc/packages/coq/stdlib/Coq.Init.Logic.html /usr/share/doc/packages/coq/stdlib/Coq.Init.Logic_Type.html /usr/share/doc/packages/coq/stdlib/Coq.Init.Ltac.html /usr/share/doc/packages/coq/stdlib/Coq.Init.Nat.html /usr/share/doc/packages/coq/stdlib/Coq.Init.Notations.html /usr/share/doc/packages/coq/stdlib/Coq.Init.Number.html /usr/share/doc/packages/coq/stdlib/Coq.Init.Numeral.html /usr/share/doc/packages/coq/stdlib/Coq.Init.Peano.html /usr/share/doc/packages/coq/stdlib/Coq.Init.Prelude.html /usr/share/doc/packages/coq/stdlib/Coq.Init.Specif.html /usr/share/doc/packages/coq/stdlib/Coq.Init.Tactics.html /usr/share/doc/packages/coq/stdlib/Coq.Init.Tauto.html /usr/share/doc/packages/coq/stdlib/Coq.Init.Wf.html /usr/share/doc/packages/coq/stdlib/Coq.Lists.List.html /usr/share/doc/packages/coq/stdlib/Coq.Lists.ListDec.html /usr/share/doc/packages/coq/stdlib/Coq.Lists.ListSet.html /usr/share/doc/packages/coq/stdlib/Coq.Lists.ListTactics.html /usr/share/doc/packages/coq/stdlib/Coq.Lists.SetoidList.html /usr/share/doc/packages/coq/stdlib/Coq.Lists.SetoidPermutation.html /usr/share/doc/packages/coq/stdlib/Coq.Lists.StreamMemo.html /usr/share/doc/packages/coq/stdlib/Coq.Lists.Streams.html /usr/share/doc/packages/coq/stdlib/Coq.Logic.Berardi.html /usr/share/doc/packages/coq/stdlib/Coq.Logic.ChoiceFacts.html /usr/share/doc/packages/coq/stdlib/Coq.Logic.Classical.html /usr/share/doc/packages/coq/stdlib/Coq.Logic.ClassicalChoice.html /usr/share/doc/packages/coq/stdlib/Coq.Logic.ClassicalDescription.html /usr/share/doc/packages/coq/stdlib/Coq.Logic.ClassicalEpsilon.html /usr/share/doc/packages/coq/stdlib/Coq.Logic.ClassicalFacts.html /usr/share/doc/packages/coq/stdlib/Coq.Logic.ClassicalUniqueChoice.html /usr/share/doc/packages/coq/stdlib/Coq.Logic.Classical_Pred_Type.html /usr/share/doc/packages/coq/stdlib/Coq.Logic.Classical_Prop.html /usr/share/doc/packages/coq/stdlib/Coq.Logic.ConstructiveEpsilon.html /usr/share/doc/packages/coq/stdlib/Coq.Logic.Decidable.html /usr/share/doc/packages/coq/stdlib/Coq.Logic.Description.html /usr/share/doc/packages/coq/stdlib/Coq.Logic.Diaconescu.html /usr/share/doc/packages/coq/stdlib/Coq.Logic.Epsilon.html /usr/share/doc/packages/coq/stdlib/Coq.Logic.Eqdep.html /usr/share/doc/packages/coq/stdlib/Coq.Logic.EqdepFacts.html /usr/share/doc/packages/coq/stdlib/Coq.Logic.Eqdep_dec.html /usr/share/doc/packages/coq/stdlib/Coq.Logic.ExtensionalFunctionRepresentative.html /usr/share/doc/packages/coq/stdlib/Coq.Logic.ExtensionalityFacts.html /usr/share/doc/packages/coq/stdlib/Coq.Logic.FinFun.html /usr/share/doc/packages/coq/stdlib/Coq.Logic.FunctionalExtensionality.html /usr/share/doc/packages/coq/stdlib/Coq.Logic.HLevels.html /usr/share/doc/packages/coq/stdlib/Coq.Logic.Hurkens.html /usr/share/doc/packages/coq/stdlib/Coq.Logic.IndefiniteDescription.html /usr/share/doc/packages/coq/stdlib/Coq.Logic.JMeq.html /usr/share/doc/packages/coq/stdlib/Coq.Logic.ProofIrrelevance.html /usr/share/doc/packages/coq/stdlib/Coq.Logic.ProofIrrelevanceFacts.html /usr/share/doc/packages/coq/stdlib/Coq.Logic.PropExtensionality.html /usr/share/doc/packages/coq/stdlib/Coq.Logic.PropExtensionalityFacts.html /usr/share/doc/packages/coq/stdlib/Coq.Logic.PropFacts.html /usr/share/doc/packages/coq/stdlib/Coq.Logic.RelationalChoice.html /usr/share/doc/packages/coq/stdlib/Coq.Logic.SetIsType.html /usr/share/doc/packages/coq/stdlib/Coq.Logic.SetoidChoice.html /usr/share/doc/packages/coq/stdlib/Coq.Logic.StrictProp.html /usr/share/doc/packages/coq/stdlib/Coq.Logic.WKL.html /usr/share/doc/packages/coq/stdlib/Coq.Logic.WeakFan.html /usr/share/doc/packages/coq/stdlib/Coq.MSets.MSetAVL.html /usr/share/doc/packages/coq/stdlib/Coq.MSets.MSetDecide.html /usr/share/doc/packages/coq/stdlib/Coq.MSets.MSetEqProperties.html /usr/share/doc/packages/coq/stdlib/Coq.MSets.MSetFacts.html /usr/share/doc/packages/coq/stdlib/Coq.MSets.MSetGenTree.html /usr/share/doc/packages/coq/stdlib/Coq.MSets.MSetInterface.html /usr/share/doc/packages/coq/stdlib/Coq.MSets.MSetList.html /usr/share/doc/packages/coq/stdlib/Coq.MSets.MSetPositive.html /usr/share/doc/packages/coq/stdlib/Coq.MSets.MSetProperties.html /usr/share/doc/packages/coq/stdlib/Coq.MSets.MSetRBT.html /usr/share/doc/packages/coq/stdlib/Coq.MSets.MSetToFiniteSet.html /usr/share/doc/packages/coq/stdlib/Coq.MSets.MSetWeakList.html /usr/share/doc/packages/coq/stdlib/Coq.MSets.MSets.html /usr/share/doc/packages/coq/stdlib/Coq.NArith.BinNat.html /usr/share/doc/packages/coq/stdlib/Coq.NArith.BinNatDef.html /usr/share/doc/packages/coq/stdlib/Coq.NArith.NArith.html /usr/share/doc/packages/coq/stdlib/Coq.NArith.Ndec.html /usr/share/doc/packages/coq/stdlib/Coq.NArith.Ndigits.html /usr/share/doc/packages/coq/stdlib/Coq.NArith.Ndist.html /usr/share/doc/packages/coq/stdlib/Coq.NArith.Ndiv_def.html /usr/share/doc/packages/coq/stdlib/Coq.NArith.Ngcd_def.html /usr/share/doc/packages/coq/stdlib/Coq.NArith.Nnat.html /usr/share/doc/packages/coq/stdlib/Coq.NArith.Nsqrt_def.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.AltBinNotations.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.BinNums.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Cyclic.Abstract.CyclicAxioms.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Cyclic.Abstract.DoubleType.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Cyclic.Abstract.NZCyclic.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Cyclic.Int31.Cyclic31.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Cyclic.Int31.Int31.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Cyclic.Int31.Ring31.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Cyclic.Int63.Cyclic63.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Cyclic.Int63.Int63.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Cyclic.Int63.Ring63.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Cyclic.ZModulo.ZModulo.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.DecimalFacts.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.DecimalN.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.DecimalNat.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.DecimalPos.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.DecimalQ.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.DecimalR.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.DecimalString.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.DecimalZ.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.HexadecimalFacts.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.HexadecimalN.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.HexadecimalNat.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.HexadecimalPos.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.HexadecimalQ.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.HexadecimalR.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.HexadecimalString.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.HexadecimalZ.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Integer.Abstract.ZAdd.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Integer.Abstract.ZAddOrder.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Integer.Abstract.ZAxioms.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Integer.Abstract.ZBase.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Integer.Abstract.ZBits.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Integer.Abstract.ZDivEucl.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Integer.Abstract.ZDivFloor.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Integer.Abstract.ZDivTrunc.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Integer.Abstract.ZGcd.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Integer.Abstract.ZLcm.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Integer.Abstract.ZLt.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Integer.Abstract.ZMaxMin.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Integer.Abstract.ZMul.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Integer.Abstract.ZMulOrder.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Integer.Abstract.ZParity.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Integer.Abstract.ZPow.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Integer.Abstract.ZProperties.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Integer.Abstract.ZSgnAbs.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Integer.Binary.ZBinary.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Integer.NatPairs.ZNatPairs.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.NaryFunctions.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.NatInt.NZAdd.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.NatInt.NZAddOrder.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.NatInt.NZAxioms.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.NatInt.NZBase.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.NatInt.NZBits.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.NatInt.NZDiv.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.NatInt.NZDomain.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.NatInt.NZGcd.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.NatInt.NZLog.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.NatInt.NZMul.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.NatInt.NZMulOrder.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.NatInt.NZOrder.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.NatInt.NZParity.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.NatInt.NZPow.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.NatInt.NZProperties.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.NatInt.NZSqrt.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Natural.Abstract.NAdd.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Natural.Abstract.NAddOrder.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Natural.Abstract.NAxioms.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Natural.Abstract.NBase.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Natural.Abstract.NBits.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Natural.Abstract.NDefOps.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Natural.Abstract.NDiv.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Natural.Abstract.NGcd.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Natural.Abstract.NIso.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Natural.Abstract.NLcm.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Natural.Abstract.NLog.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Natural.Abstract.NMaxMin.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Natural.Abstract.NMulOrder.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Natural.Abstract.NOrder.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Natural.Abstract.NParity.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Natural.Abstract.NPow.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Natural.Abstract.NProperties.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Natural.Abstract.NSqrt.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Natural.Abstract.NStrongRec.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Natural.Abstract.NSub.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Natural.Binary.NBinary.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.Natural.Peano.NPeano.html /usr/share/doc/packages/coq/stdlib/Coq.Numbers.NumPrelude.html /usr/share/doc/packages/coq/stdlib/Coq.PArith.BinPos.html /usr/share/doc/packages/coq/stdlib/Coq.PArith.BinPosDef.html /usr/share/doc/packages/coq/stdlib/Coq.PArith.PArith.html /usr/share/doc/packages/coq/stdlib/Coq.PArith.POrderedType.html /usr/share/doc/packages/coq/stdlib/Coq.PArith.Pnat.html /usr/share/doc/packages/coq/stdlib/Coq.Program.Basics.html /usr/share/doc/packages/coq/stdlib/Coq.Program.Combinators.html /usr/share/doc/packages/coq/stdlib/Coq.Program.Equality.html /usr/share/doc/packages/coq/stdlib/Coq.Program.Program.html /usr/share/doc/packages/coq/stdlib/Coq.Program.Subset.html /usr/share/doc/packages/coq/stdlib/Coq.Program.Syntax.html /usr/share/doc/packages/coq/stdlib/Coq.Program.Tactics.html /usr/share/doc/packages/coq/stdlib/Coq.Program.Utils.html /usr/share/doc/packages/coq/stdlib/Coq.Program.Wf.html /usr/share/doc/packages/coq/stdlib/Coq.QArith.QArith.html /usr/share/doc/packages/coq/stdlib/Coq.QArith.QArith_base.html /usr/share/doc/packages/coq/stdlib/Coq.QArith.QOrderedType.html /usr/share/doc/packages/coq/stdlib/Coq.QArith.Qabs.html /usr/share/doc/packages/coq/stdlib/Coq.QArith.Qcabs.html /usr/share/doc/packages/coq/stdlib/Coq.QArith.Qcanon.html /usr/share/doc/packages/coq/stdlib/Coq.QArith.Qfield.html /usr/share/doc/packages/coq/stdlib/Coq.QArith.Qminmax.html /usr/share/doc/packages/coq/stdlib/Coq.QArith.Qpower.html /usr/share/doc/packages/coq/stdlib/Coq.QArith.Qreals.html /usr/share/doc/packages/coq/stdlib/Coq.QArith.Qreduction.html /usr/share/doc/packages/coq/stdlib/Coq.QArith.Qring.html /usr/share/doc/packages/coq/stdlib/Coq.QArith.Qround.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Abstract.ConstructiveAbs.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Abstract.ConstructiveLUB.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Abstract.ConstructiveLimits.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Abstract.ConstructiveMinMax.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Abstract.ConstructivePower.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Abstract.ConstructiveReals.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Abstract.ConstructiveRealsMorphisms.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Abstract.ConstructiveSum.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Alembert.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.AltSeries.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.ArithProp.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Binomial.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Cauchy.ConstructiveCauchyAbs.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Cauchy.ConstructiveCauchyReals.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Cauchy.ConstructiveCauchyRealsMult.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Cauchy.ConstructiveExtra.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Cauchy.ConstructiveRcomplete.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Cauchy.PosExtra.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Cauchy.QExtra.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Cauchy_prod.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.ClassicalConstructiveReals.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.ClassicalDedekindReals.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Cos_plus.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Cos_rel.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.DiscrR.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Exp_prop.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Integration.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.MVT.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Machin.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.NewtonInt.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.PSeries_reg.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.PartSum.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.RIneq.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.RList.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.ROrderedType.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.R_Ifp.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.R_sqr.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.R_sqrt.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Ranalysis.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Ranalysis1.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Ranalysis2.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Ranalysis3.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Ranalysis4.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Ranalysis5.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Ranalysis_reg.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Ratan.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Raxioms.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Rbase.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Rbasic_fun.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Rcomplete.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Rdefinitions.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Rderiv.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Reals.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Rfunctions.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Rgeom.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.RiemannInt.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.RiemannInt_SF.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Rlimit.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Rlogic.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Rminmax.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Rpow_def.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Rpower.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Rprod.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Rregisternames.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Rseries.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Rsigma.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Rsqrt_def.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Rtopology.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Rtrigo.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Rtrigo1.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Rtrigo_alt.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Rtrigo_calc.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Rtrigo_def.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Rtrigo_facts.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Rtrigo_fun.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Rtrigo_reg.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Runcountable.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.SeqProp.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.SeqSeries.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.SplitAbsolu.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.SplitRmult.html /usr/share/doc/packages/coq/stdlib/Coq.Reals.Sqrt_reg.html /usr/share/doc/packages/coq/stdlib/Coq.Relations.Operators_Properties.html /usr/share/doc/packages/coq/stdlib/Coq.Relations.Relation_Definitions.html /usr/share/doc/packages/coq/stdlib/Coq.Relations.Relation_Operators.html /usr/share/doc/packages/coq/stdlib/Coq.Relations.Relations.html /usr/share/doc/packages/coq/stdlib/Coq.Setoids.Setoid.html /usr/share/doc/packages/coq/stdlib/Coq.Sets.Classical_sets.html /usr/share/doc/packages/coq/stdlib/Coq.Sets.Constructive_sets.html /usr/share/doc/packages/coq/stdlib/Coq.Sets.Cpo.html /usr/share/doc/packages/coq/stdlib/Coq.Sets.Ensembles.html /usr/share/doc/packages/coq/stdlib/Coq.Sets.Finite_sets.html /usr/share/doc/packages/coq/stdlib/Coq.Sets.Finite_sets_facts.html /usr/share/doc/packages/coq/stdlib/Coq.Sets.Image.html /usr/share/doc/packages/coq/stdlib/Coq.Sets.Infinite_sets.html /usr/share/doc/packages/coq/stdlib/Coq.Sets.Integers.html /usr/share/doc/packages/coq/stdlib/Coq.Sets.Multiset.html /usr/share/doc/packages/coq/stdlib/Coq.Sets.Partial_Order.html /usr/share/doc/packages/coq/stdlib/Coq.Sets.Permut.html /usr/share/doc/packages/coq/stdlib/Coq.Sets.Powerset.html /usr/share/doc/packages/coq/stdlib/Coq.Sets.Powerset_Classical_facts.html /usr/share/doc/packages/coq/stdlib/Coq.Sets.Powerset_facts.html /usr/share/doc/packages/coq/stdlib/Coq.Sets.Relations_1.html /usr/share/doc/packages/coq/stdlib/Coq.Sets.Relations_1_facts.html /usr/share/doc/packages/coq/stdlib/Coq.Sets.Relations_2.html /usr/share/doc/packages/coq/stdlib/Coq.Sets.Relations_2_facts.html /usr/share/doc/packages/coq/stdlib/Coq.Sets.Relations_3.html /usr/share/doc/packages/coq/stdlib/Coq.Sets.Relations_3_facts.html /usr/share/doc/packages/coq/stdlib/Coq.Sets.Uniset.html /usr/share/doc/packages/coq/stdlib/Coq.Sorting.CPermutation.html /usr/share/doc/packages/coq/stdlib/Coq.Sorting.Heap.html /usr/share/doc/packages/coq/stdlib/Coq.Sorting.Mergesort.html /usr/share/doc/packages/coq/stdlib/Coq.Sorting.PermutEq.html /usr/share/doc/packages/coq/stdlib/Coq.Sorting.PermutSetoid.html /usr/share/doc/packages/coq/stdlib/Coq.Sorting.Permutation.html /usr/share/doc/packages/coq/stdlib/Coq.Sorting.Sorted.html /usr/share/doc/packages/coq/stdlib/Coq.Sorting.Sorting.html /usr/share/doc/packages/coq/stdlib/Coq.Strings.Ascii.html /usr/share/doc/packages/coq/stdlib/Coq.Strings.BinaryString.html /usr/share/doc/packages/coq/stdlib/Coq.Strings.Byte.html /usr/share/doc/packages/coq/stdlib/Coq.Strings.ByteVector.html /usr/share/doc/packages/coq/stdlib/Coq.Strings.HexString.html /usr/share/doc/packages/coq/stdlib/Coq.Strings.OctalString.html /usr/share/doc/packages/coq/stdlib/Coq.Strings.String.html /usr/share/doc/packages/coq/stdlib/Coq.Structures.DecidableType.html /usr/share/doc/packages/coq/stdlib/Coq.Structures.DecidableTypeEx.html /usr/share/doc/packages/coq/stdlib/Coq.Structures.Equalities.html /usr/share/doc/packages/coq/stdlib/Coq.Structures.EqualitiesFacts.html /usr/share/doc/packages/coq/stdlib/Coq.Structures.GenericMinMax.html /usr/share/doc/packages/coq/stdlib/Coq.Structures.OrderedType.html /usr/share/doc/packages/coq/stdlib/Coq.Structures.OrderedTypeAlt.html /usr/share/doc/packages/coq/stdlib/Coq.Structures.OrderedTypeEx.html /usr/share/doc/packages/coq/stdlib/Coq.Structures.Orders.html /usr/share/doc/packages/coq/stdlib/Coq.Structures.OrdersAlt.html /usr/share/doc/packages/coq/stdlib/Coq.Structures.OrdersEx.html /usr/share/doc/packages/coq/stdlib/Coq.Structures.OrdersFacts.html /usr/share/doc/packages/coq/stdlib/Coq.Structures.OrdersLists.html /usr/share/doc/packages/coq/stdlib/Coq.Structures.OrdersTac.html /usr/share/doc/packages/coq/stdlib/Coq.Unicode.Utf8.html /usr/share/doc/packages/coq/stdlib/Coq.Unicode.Utf8_core.html /usr/share/doc/packages/coq/stdlib/Coq.Vectors.Fin.html /usr/share/doc/packages/coq/stdlib/Coq.Vectors.Vector.html /usr/share/doc/packages/coq/stdlib/Coq.Vectors.VectorDef.html /usr/share/doc/packages/coq/stdlib/Coq.Vectors.VectorEq.html /usr/share/doc/packages/coq/stdlib/Coq.Vectors.VectorSpec.html /usr/share/doc/packages/coq/stdlib/Coq.Wellfounded.Disjoint_Union.html /usr/share/doc/packages/coq/stdlib/Coq.Wellfounded.Inclusion.html /usr/share/doc/packages/coq/stdlib/Coq.Wellfounded.Inverse_Image.html /usr/share/doc/packages/coq/stdlib/Coq.Wellfounded.Lexicographic_Exponentiation.html /usr/share/doc/packages/coq/stdlib/Coq.Wellfounded.Lexicographic_Product.html /usr/share/doc/packages/coq/stdlib/Coq.Wellfounded.Transitive_Closure.html /usr/share/doc/packages/coq/stdlib/Coq.Wellfounded.Union.html /usr/share/doc/packages/coq/stdlib/Coq.Wellfounded.Well_Ordering.html /usr/share/doc/packages/coq/stdlib/Coq.Wellfounded.Wellfounded.html /usr/share/doc/packages/coq/stdlib/Coq.ZArith.BinInt.html /usr/share/doc/packages/coq/stdlib/Coq.ZArith.BinIntDef.html /usr/share/doc/packages/coq/stdlib/Coq.ZArith.Int.html /usr/share/doc/packages/coq/stdlib/Coq.ZArith.Wf_Z.html /usr/share/doc/packages/coq/stdlib/Coq.ZArith.ZArith.html /usr/share/doc/packages/coq/stdlib/Coq.ZArith.ZArith_base.html /usr/share/doc/packages/coq/stdlib/Coq.ZArith.ZArith_dec.html /usr/share/doc/packages/coq/stdlib/Coq.ZArith.Zabs.html /usr/share/doc/packages/coq/stdlib/Coq.ZArith.Zbool.html /usr/share/doc/packages/coq/stdlib/Coq.ZArith.Zcompare.html /usr/share/doc/packages/coq/stdlib/Coq.ZArith.Zcomplements.html /usr/share/doc/packages/coq/stdlib/Coq.ZArith.Zdigits.html /usr/share/doc/packages/coq/stdlib/Coq.ZArith.Zdiv.html /usr/share/doc/packages/coq/stdlib/Coq.ZArith.Zeuclid.html /usr/share/doc/packages/coq/stdlib/Coq.ZArith.Zeven.html /usr/share/doc/packages/coq/stdlib/Coq.ZArith.Zgcd_alt.html /usr/share/doc/packages/coq/stdlib/Coq.ZArith.Zhints.html /usr/share/doc/packages/coq/stdlib/Coq.ZArith.Zmax.html /usr/share/doc/packages/coq/stdlib/Coq.ZArith.Zmin.html /usr/share/doc/packages/coq/stdlib/Coq.ZArith.Zminmax.html /usr/share/doc/packages/coq/stdlib/Coq.ZArith.Zmisc.html /usr/share/doc/packages/coq/stdlib/Coq.ZArith.Znat.html /usr/share/doc/packages/coq/stdlib/Coq.ZArith.Znumtheory.html /usr/share/doc/packages/coq/stdlib/Coq.ZArith.Zorder.html /usr/share/doc/packages/coq/stdlib/Coq.ZArith.Zpow_alt.html /usr/share/doc/packages/coq/stdlib/Coq.ZArith.Zpow_def.html /usr/share/doc/packages/coq/stdlib/Coq.ZArith.Zpow_facts.html /usr/share/doc/packages/coq/stdlib/Coq.ZArith.Zpower.html /usr/share/doc/packages/coq/stdlib/Coq.ZArith.Zquot.html /usr/share/doc/packages/coq/stdlib/Coq.ZArith.Zwf.html /usr/share/doc/packages/coq/stdlib/Coq.ZArith.auxiliary.html /usr/share/doc/packages/coq/stdlib/Coq.btauto.Algebra.html /usr/share/doc/packages/coq/stdlib/Coq.btauto.Btauto.html /usr/share/doc/packages/coq/stdlib/Coq.btauto.Reflect.html /usr/share/doc/packages/coq/stdlib/Coq.derive.Derive.html /usr/share/doc/packages/coq/stdlib/Coq.extraction.ExtrHaskellBasic.html /usr/share/doc/packages/coq/stdlib/Coq.extraction.ExtrHaskellNatInt.html /usr/share/doc/packages/coq/stdlib/Coq.extraction.ExtrHaskellNatInteger.html /usr/share/doc/packages/coq/stdlib/Coq.extraction.ExtrHaskellNatNum.html /usr/share/doc/packages/coq/stdlib/Coq.extraction.ExtrHaskellString.html /usr/share/doc/packages/coq/stdlib/Coq.extraction.ExtrHaskellZInt.html /usr/share/doc/packages/coq/stdlib/Coq.extraction.ExtrHaskellZInteger.html /usr/share/doc/packages/coq/stdlib/Coq.extraction.ExtrHaskellZNum.html /usr/share/doc/packages/coq/stdlib/Coq.extraction.ExtrOCamlFloats.html /usr/share/doc/packages/coq/stdlib/Coq.extraction.ExtrOCamlInt63.html /usr/share/doc/packages/coq/stdlib/Coq.extraction.ExtrOCamlPArray.html /usr/share/doc/packages/coq/stdlib/Coq.extraction.ExtrOcamlBasic.html /usr/share/doc/packages/coq/stdlib/Coq.extraction.ExtrOcamlBigIntConv.html /usr/share/doc/packages/coq/stdlib/Coq.extraction.ExtrOcamlChar.html /usr/share/doc/packages/coq/stdlib/Coq.extraction.ExtrOcamlIntConv.html /usr/share/doc/packages/coq/stdlib/Coq.extraction.ExtrOcamlNatBigInt.html /usr/share/doc/packages/coq/stdlib/Coq.extraction.ExtrOcamlNatInt.html /usr/share/doc/packages/coq/stdlib/Coq.extraction.ExtrOcamlNativeString.html /usr/share/doc/packages/coq/stdlib/Coq.extraction.ExtrOcamlString.html /usr/share/doc/packages/coq/stdlib/Coq.extraction.ExtrOcamlZBigInt.html /usr/share/doc/packages/coq/stdlib/Coq.extraction.ExtrOcamlZInt.html /usr/share/doc/packages/coq/stdlib/Coq.extraction.Extraction.html /usr/share/doc/packages/coq/stdlib/Coq.funind.FunInd.html /usr/share/doc/packages/coq/stdlib/Coq.funind.Recdef.html /usr/share/doc/packages/coq/stdlib/Coq.micromega.DeclConstant.html /usr/share/doc/packages/coq/stdlib/Coq.micromega.Env.html /usr/share/doc/packages/coq/stdlib/Coq.micromega.EnvRing.html /usr/share/doc/packages/coq/stdlib/Coq.micromega.Fourier.html /usr/share/doc/packages/coq/stdlib/Coq.micromega.Fourier_util.html /usr/share/doc/packages/coq/stdlib/Coq.micromega.Lia.html /usr/share/doc/packages/coq/stdlib/Coq.micromega.Lqa.html /usr/share/doc/packages/coq/stdlib/Coq.micromega.Lra.html /usr/share/doc/packages/coq/stdlib/Coq.micromega.MExtraction.html /usr/share/doc/packages/coq/stdlib/Coq.micromega.OrderedRing.html /usr/share/doc/packages/coq/stdlib/Coq.micromega.Psatz.html /usr/share/doc/packages/coq/stdlib/Coq.micromega.QMicromega.html /usr/share/doc/packages/coq/stdlib/Coq.micromega.RMicromega.html /usr/share/doc/packages/coq/stdlib/Coq.micromega.Refl.html /usr/share/doc/packages/coq/stdlib/Coq.micromega.RingMicromega.html /usr/share/doc/packages/coq/stdlib/Coq.micromega.Tauto.html /usr/share/doc/packages/coq/stdlib/Coq.micromega.VarMap.html /usr/share/doc/packages/coq/stdlib/Coq.micromega.ZArith_hints.html /usr/share/doc/packages/coq/stdlib/Coq.micromega.ZCoeff.html /usr/share/doc/packages/coq/stdlib/Coq.micromega.ZMicromega.html /usr/share/doc/packages/coq/stdlib/Coq.micromega.Zify.html /usr/share/doc/packages/coq/stdlib/Coq.micromega.ZifyBool.html /usr/share/doc/packages/coq/stdlib/Coq.micromega.ZifyClasses.html /usr/share/doc/packages/coq/stdlib/Coq.micromega.ZifyComparison.html /usr/share/doc/packages/coq/stdlib/Coq.micromega.ZifyInst.html /usr/share/doc/packages/coq/stdlib/Coq.micromega.ZifyInt63.html /usr/share/doc/packages/coq/stdlib/Coq.micromega.ZifyPow.html /usr/share/doc/packages/coq/stdlib/Coq.micromega.Ztac.html /usr/share/doc/packages/coq/stdlib/Coq.nsatz.Nsatz.html /usr/share/doc/packages/coq/stdlib/Coq.nsatz.NsatzTactic.html /usr/share/doc/packages/coq/stdlib/Coq.omega.Omega.html /usr/share/doc/packages/coq/stdlib/Coq.omega.OmegaLemmas.html /usr/share/doc/packages/coq/stdlib/Coq.omega.OmegaPlugin.html /usr/share/doc/packages/coq/stdlib/Coq.omega.OmegaTactic.html /usr/share/doc/packages/coq/stdlib/Coq.omega.PreOmega.html /usr/share/doc/packages/coq/stdlib/Coq.rtauto.Bintree.html /usr/share/doc/packages/coq/stdlib/Coq.rtauto.Rtauto.html /usr/share/doc/packages/coq/stdlib/Coq.setoid_ring.Algebra_syntax.html /usr/share/doc/packages/coq/stdlib/Coq.setoid_ring.ArithRing.html /usr/share/doc/packages/coq/stdlib/Coq.setoid_ring.BinList.html /usr/share/doc/packages/coq/stdlib/Coq.setoid_ring.Cring.html /usr/share/doc/packages/coq/stdlib/Coq.setoid_ring.Field.html /usr/share/doc/packages/coq/stdlib/Coq.setoid_ring.Field_tac.html /usr/share/doc/packages/coq/stdlib/Coq.setoid_ring.Field_theory.html /usr/share/doc/packages/coq/stdlib/Coq.setoid_ring.InitialRing.html /usr/share/doc/packages/coq/stdlib/Coq.setoid_ring.Integral_domain.html /usr/share/doc/packages/coq/stdlib/Coq.setoid_ring.NArithRing.html /usr/share/doc/packages/coq/stdlib/Coq.setoid_ring.Ncring.html /usr/share/doc/packages/coq/stdlib/Coq.setoid_ring.Ncring_initial.html /usr/share/doc/packages/coq/stdlib/Coq.setoid_ring.Ncring_polynom.html /usr/share/doc/packages/coq/stdlib/Coq.setoid_ring.Ncring_tac.html /usr/share/doc/packages/coq/stdlib/Coq.setoid_ring.RealField.html /usr/share/doc/packages/coq/stdlib/Coq.setoid_ring.Ring.html /usr/share/doc/packages/coq/stdlib/Coq.setoid_ring.Ring_base.html /usr/share/doc/packages/coq/stdlib/Coq.setoid_ring.Ring_polynom.html /usr/share/doc/packages/coq/stdlib/Coq.setoid_ring.Ring_tac.html /usr/share/doc/packages/coq/stdlib/Coq.setoid_ring.Ring_theory.html /usr/share/doc/packages/coq/stdlib/Coq.setoid_ring.Rings_Q.html /usr/share/doc/packages/coq/stdlib/Coq.setoid_ring.Rings_R.html /usr/share/doc/packages/coq/stdlib/Coq.setoid_ring.Rings_Z.html /usr/share/doc/packages/coq/stdlib/Coq.setoid_ring.ZArithRing.html /usr/share/doc/packages/coq/stdlib/Coq.ssr.ssrbool.html /usr/share/doc/packages/coq/stdlib/Coq.ssr.ssrclasses.html /usr/share/doc/packages/coq/stdlib/Coq.ssr.ssreflect.html /usr/share/doc/packages/coq/stdlib/Coq.ssr.ssrfun.html /usr/share/doc/packages/coq/stdlib/Coq.ssr.ssrsetoid.html /usr/share/doc/packages/coq/stdlib/Coq.ssr.ssrunder.html /usr/share/doc/packages/coq/stdlib/Coq.ssrmatching.ssrmatching.html /usr/share/doc/packages/coq/stdlib/Coq.ssrsearch.ssrsearch.html /usr/share/doc/packages/coq/stdlib/Ltac2.Array.html /usr/share/doc/packages/coq/stdlib/Ltac2.Bool.html /usr/share/doc/packages/coq/stdlib/Ltac2.Char.html /usr/share/doc/packages/coq/stdlib/Ltac2.Constr.html /usr/share/doc/packages/coq/stdlib/Ltac2.Control.html /usr/share/doc/packages/coq/stdlib/Ltac2.Env.html /usr/share/doc/packages/coq/stdlib/Ltac2.Fresh.html /usr/share/doc/packages/coq/stdlib/Ltac2.Ident.html /usr/share/doc/packages/coq/stdlib/Ltac2.Init.html /usr/share/doc/packages/coq/stdlib/Ltac2.Int.html /usr/share/doc/packages/coq/stdlib/Ltac2.List.html /usr/share/doc/packages/coq/stdlib/Ltac2.Ltac1.html /usr/share/doc/packages/coq/stdlib/Ltac2.Ltac2.html /usr/share/doc/packages/coq/stdlib/Ltac2.Message.html /usr/share/doc/packages/coq/stdlib/Ltac2.Notations.html /usr/share/doc/packages/coq/stdlib/Ltac2.Option.html /usr/share/doc/packages/coq/stdlib/Ltac2.Pattern.html /usr/share/doc/packages/coq/stdlib/Ltac2.Std.html /usr/share/doc/packages/coq/stdlib/Ltac2.String.html /usr/share/doc/packages/coq/stdlib/coqdoc.css /usr/share/doc/packages/coq/stdlib/genindex.html /usr/share/doc/packages/coq/stdlib/index.html /usr/share/doc/packages/coq/stdlib/index_abbreviation_*.html /usr/share/doc/packages/coq/stdlib/index_abbreviation_A.html /usr/share/doc/packages/coq/stdlib/index_abbreviation_B.html /usr/share/doc/packages/coq/stdlib/index_abbreviation_C.html /usr/share/doc/packages/coq/stdlib/index_abbreviation_D.html /usr/share/doc/packages/coq/stdlib/index_abbreviation_E.html /usr/share/doc/packages/coq/stdlib/index_abbreviation_F.html /usr/share/doc/packages/coq/stdlib/index_abbreviation_G.html /usr/share/doc/packages/coq/stdlib/index_abbreviation_H.html /usr/share/doc/packages/coq/stdlib/index_abbreviation_I.html /usr/share/doc/packages/coq/stdlib/index_abbreviation_J.html /usr/share/doc/packages/coq/stdlib/index_abbreviation_K.html /usr/share/doc/packages/coq/stdlib/index_abbreviation_L.html /usr/share/doc/packages/coq/stdlib/index_abbreviation_M.html /usr/share/doc/packages/coq/stdlib/index_abbreviation_N.html /usr/share/doc/packages/coq/stdlib/index_abbreviation_O.html /usr/share/doc/packages/coq/stdlib/index_abbreviation_P.html /usr/share/doc/packages/coq/stdlib/index_abbreviation_Q.html /usr/share/doc/packages/coq/stdlib/index_abbreviation_R.html /usr/share/doc/packages/coq/stdlib/index_abbreviation_S.html /usr/share/doc/packages/coq/stdlib/index_abbreviation_T.html /usr/share/doc/packages/coq/stdlib/index_abbreviation_U.html /usr/share/doc/packages/coq/stdlib/index_abbreviation_V.html /usr/share/doc/packages/coq/stdlib/index_abbreviation_W.html /usr/share/doc/packages/coq/stdlib/index_abbreviation_X.html /usr/share/doc/packages/coq/stdlib/index_abbreviation_Y.html /usr/share/doc/packages/coq/stdlib/index_abbreviation_Z.html /usr/share/doc/packages/coq/stdlib/index_abbreviation__.html /usr/share/doc/packages/coq/stdlib/index_axiom_*.html /usr/share/doc/packages/coq/stdlib/index_axiom_A.html /usr/share/doc/packages/coq/stdlib/index_axiom_B.html /usr/share/doc/packages/coq/stdlib/index_axiom_C.html /usr/share/doc/packages/coq/stdlib/index_axiom_D.html /usr/share/doc/packages/coq/stdlib/index_axiom_E.html /usr/share/doc/packages/coq/stdlib/index_axiom_F.html /usr/share/doc/packages/coq/stdlib/index_axiom_G.html /usr/share/doc/packages/coq/stdlib/index_axiom_H.html /usr/share/doc/packages/coq/stdlib/index_axiom_I.html /usr/share/doc/packages/coq/stdlib/index_axiom_J.html /usr/share/doc/packages/coq/stdlib/index_axiom_K.html /usr/share/doc/packages/coq/stdlib/index_axiom_L.html /usr/share/doc/packages/coq/stdlib/index_axiom_M.html /usr/share/doc/packages/coq/stdlib/index_axiom_N.html /usr/share/doc/packages/coq/stdlib/index_axiom_O.html /usr/share/doc/packages/coq/stdlib/index_axiom_P.html /usr/share/doc/packages/coq/stdlib/index_axiom_Q.html /usr/share/doc/packages/coq/stdlib/index_axiom_R.html /usr/share/doc/packages/coq/stdlib/index_axiom_S.html /usr/share/doc/packages/coq/stdlib/index_axiom_T.html /usr/share/doc/packages/coq/stdlib/index_axiom_U.html /usr/share/doc/packages/coq/stdlib/index_axiom_V.html /usr/share/doc/packages/coq/stdlib/index_axiom_W.html /usr/share/doc/packages/coq/stdlib/index_axiom_X.html /usr/share/doc/packages/coq/stdlib/index_axiom_Y.html /usr/share/doc/packages/coq/stdlib/index_axiom_Z.html /usr/share/doc/packages/coq/stdlib/index_axiom__.html /usr/share/doc/packages/coq/stdlib/index_binder_*.html /usr/share/doc/packages/coq/stdlib/index_binder_A.html /usr/share/doc/packages/coq/stdlib/index_binder_B.html /usr/share/doc/packages/coq/stdlib/index_binder_C.html /usr/share/doc/packages/coq/stdlib/index_binder_D.html /usr/share/doc/packages/coq/stdlib/index_binder_E.html /usr/share/doc/packages/coq/stdlib/index_binder_F.html /usr/share/doc/packages/coq/stdlib/index_binder_G.html /usr/share/doc/packages/coq/stdlib/index_binder_H.html /usr/share/doc/packages/coq/stdlib/index_binder_I.html /usr/share/doc/packages/coq/stdlib/index_binder_J.html /usr/share/doc/packages/coq/stdlib/index_binder_K.html /usr/share/doc/packages/coq/stdlib/index_binder_L.html /usr/share/doc/packages/coq/stdlib/index_binder_M.html /usr/share/doc/packages/coq/stdlib/index_binder_N.html /usr/share/doc/packages/coq/stdlib/index_binder_O.html /usr/share/doc/packages/coq/stdlib/index_binder_P.html /usr/share/doc/packages/coq/stdlib/index_binder_Q.html /usr/share/doc/packages/coq/stdlib/index_binder_R.html /usr/share/doc/packages/coq/stdlib/index_binder_S.html /usr/share/doc/packages/coq/stdlib/index_binder_T.html /usr/share/doc/packages/coq/stdlib/index_binder_U.html /usr/share/doc/packages/coq/stdlib/index_binder_V.html /usr/share/doc/packages/coq/stdlib/index_binder_W.html /usr/share/doc/packages/coq/stdlib/index_binder_X.html /usr/share/doc/packages/coq/stdlib/index_binder_Y.html /usr/share/doc/packages/coq/stdlib/index_binder_Z.html /usr/share/doc/packages/coq/stdlib/index_binder__.html /usr/share/doc/packages/coq/stdlib/index_constructor_*.html /usr/share/doc/packages/coq/stdlib/index_constructor_A.html /usr/share/doc/packages/coq/stdlib/index_constructor_B.html /usr/share/doc/packages/coq/stdlib/index_constructor_C.html /usr/share/doc/packages/coq/stdlib/index_constructor_D.html /usr/share/doc/packages/coq/stdlib/index_constructor_E.html /usr/share/doc/packages/coq/stdlib/index_constructor_F.html /usr/share/doc/packages/coq/stdlib/index_constructor_G.html /usr/share/doc/packages/coq/stdlib/index_constructor_H.html /usr/share/doc/packages/coq/stdlib/index_constructor_I.html /usr/share/doc/packages/coq/stdlib/index_constructor_J.html /usr/share/doc/packages/coq/stdlib/index_constructor_K.html /usr/share/doc/packages/coq/stdlib/index_constructor_L.html /usr/share/doc/packages/coq/stdlib/index_constructor_M.html /usr/share/doc/packages/coq/stdlib/index_constructor_N.html /usr/share/doc/packages/coq/stdlib/index_constructor_O.html /usr/share/doc/packages/coq/stdlib/index_constructor_P.html /usr/share/doc/packages/coq/stdlib/index_constructor_Q.html /usr/share/doc/packages/coq/stdlib/index_constructor_R.html /usr/share/doc/packages/coq/stdlib/index_constructor_S.html /usr/share/doc/packages/coq/stdlib/index_constructor_T.html /usr/share/doc/packages/coq/stdlib/index_constructor_U.html /usr/share/doc/packages/coq/stdlib/index_constructor_V.html /usr/share/doc/packages/coq/stdlib/index_constructor_W.html /usr/share/doc/packages/coq/stdlib/index_constructor_X.html /usr/share/doc/packages/coq/stdlib/index_constructor_Y.html /usr/share/doc/packages/coq/stdlib/index_constructor_Z.html /usr/share/doc/packages/coq/stdlib/index_constructor__.html /usr/share/doc/packages/coq/stdlib/index_definition_*.html /usr/share/doc/packages/coq/stdlib/index_definition_A.html /usr/share/doc/packages/coq/stdlib/index_definition_B.html /usr/share/doc/packages/coq/stdlib/index_definition_C.html /usr/share/doc/packages/coq/stdlib/index_definition_D.html /usr/share/doc/packages/coq/stdlib/index_definition_E.html /usr/share/doc/packages/coq/stdlib/index_definition_F.html /usr/share/doc/packages/coq/stdlib/index_definition_G.html /usr/share/doc/packages/coq/stdlib/index_definition_H.html /usr/share/doc/packages/coq/stdlib/index_definition_I.html /usr/share/doc/packages/coq/stdlib/index_definition_J.html /usr/share/doc/packages/coq/stdlib/index_definition_K.html /usr/share/doc/packages/coq/stdlib/index_definition_L.html /usr/share/doc/packages/coq/stdlib/index_definition_M.html /usr/share/doc/packages/coq/stdlib/index_definition_N.html /usr/share/doc/packages/coq/stdlib/index_definition_O.html /usr/share/doc/packages/coq/stdlib/index_definition_P.html /usr/share/doc/packages/coq/stdlib/index_definition_Q.html /usr/share/doc/packages/coq/stdlib/index_definition_R.html /usr/share/doc/packages/coq/stdlib/index_definition_S.html /usr/share/doc/packages/coq/stdlib/index_definition_T.html /usr/share/doc/packages/coq/stdlib/index_definition_U.html /usr/share/doc/packages/coq/stdlib/index_definition_V.html /usr/share/doc/packages/coq/stdlib/index_definition_W.html /usr/share/doc/packages/coq/stdlib/index_definition_X.html /usr/share/doc/packages/coq/stdlib/index_definition_Y.html /usr/share/doc/packages/coq/stdlib/index_definition_Z.html /usr/share/doc/packages/coq/stdlib/index_definition__.html /usr/share/doc/packages/coq/stdlib/index_global_*.html /usr/share/doc/packages/coq/stdlib/index_global_A.html /usr/share/doc/packages/coq/stdlib/index_global_B.html /usr/share/doc/packages/coq/stdlib/index_global_C.html /usr/share/doc/packages/coq/stdlib/index_global_D.html /usr/share/doc/packages/coq/stdlib/index_global_E.html /usr/share/doc/packages/coq/stdlib/index_global_F.html /usr/share/doc/packages/coq/stdlib/index_global_G.html /usr/share/doc/packages/coq/stdlib/index_global_H.html /usr/share/doc/packages/coq/stdlib/index_global_I.html /usr/share/doc/packages/coq/stdlib/index_global_J.html /usr/share/doc/packages/coq/stdlib/index_global_K.html /usr/share/doc/packages/coq/stdlib/index_global_L.html /usr/share/doc/packages/coq/stdlib/index_global_M.html /usr/share/doc/packages/coq/stdlib/index_global_N.html /usr/share/doc/packages/coq/stdlib/index_global_O.html /usr/share/doc/packages/coq/stdlib/index_global_P.html /usr/share/doc/packages/coq/stdlib/index_global_Q.html /usr/share/doc/packages/coq/stdlib/index_global_R.html /usr/share/doc/packages/coq/stdlib/index_global_S.html /usr/share/doc/packages/coq/stdlib/index_global_T.html /usr/share/doc/packages/coq/stdlib/index_global_U.html /usr/share/doc/packages/coq/stdlib/index_global_V.html /usr/share/doc/packages/coq/stdlib/index_global_W.html /usr/share/doc/packages/coq/stdlib/index_global_X.html /usr/share/doc/packages/coq/stdlib/index_global_Y.html /usr/share/doc/packages/coq/stdlib/index_global_Z.html /usr/share/doc/packages/coq/stdlib/index_global__.html /usr/share/doc/packages/coq/stdlib/index_inductive_*.html /usr/share/doc/packages/coq/stdlib/index_inductive_A.html /usr/share/doc/packages/coq/stdlib/index_inductive_B.html /usr/share/doc/packages/coq/stdlib/index_inductive_C.html /usr/share/doc/packages/coq/stdlib/index_inductive_D.html /usr/share/doc/packages/coq/stdlib/index_inductive_E.html /usr/share/doc/packages/coq/stdlib/index_inductive_F.html /usr/share/doc/packages/coq/stdlib/index_inductive_G.html /usr/share/doc/packages/coq/stdlib/index_inductive_H.html /usr/share/doc/packages/coq/stdlib/index_inductive_I.html /usr/share/doc/packages/coq/stdlib/index_inductive_J.html /usr/share/doc/packages/coq/stdlib/index_inductive_K.html /usr/share/doc/packages/coq/stdlib/index_inductive_L.html /usr/share/doc/packages/coq/stdlib/index_inductive_M.html /usr/share/doc/packages/coq/stdlib/index_inductive_N.html /usr/share/doc/packages/coq/stdlib/index_inductive_O.html /usr/share/doc/packages/coq/stdlib/index_inductive_P.html /usr/share/doc/packages/coq/stdlib/index_inductive_Q.html /usr/share/doc/packages/coq/stdlib/index_inductive_R.html /usr/share/doc/packages/coq/stdlib/index_inductive_S.html /usr/share/doc/packages/coq/stdlib/index_inductive_T.html /usr/share/doc/packages/coq/stdlib/index_inductive_U.html /usr/share/doc/packages/coq/stdlib/index_inductive_V.html /usr/share/doc/packages/coq/stdlib/index_inductive_W.html /usr/share/doc/packages/coq/stdlib/index_inductive_X.html /usr/share/doc/packages/coq/stdlib/index_inductive_Y.html /usr/share/doc/packages/coq/stdlib/index_inductive_Z.html /usr/share/doc/packages/coq/stdlib/index_inductive__.html /usr/share/doc/packages/coq/stdlib/index_instance_*.html /usr/share/doc/packages/coq/stdlib/index_instance_A.html /usr/share/doc/packages/coq/stdlib/index_instance_B.html /usr/share/doc/packages/coq/stdlib/index_instance_C.html /usr/share/doc/packages/coq/stdlib/index_instance_D.html /usr/share/doc/packages/coq/stdlib/index_instance_E.html /usr/share/doc/packages/coq/stdlib/index_instance_F.html /usr/share/doc/packages/coq/stdlib/index_instance_G.html /usr/share/doc/packages/coq/stdlib/index_instance_H.html /usr/share/doc/packages/coq/stdlib/index_instance_I.html /usr/share/doc/packages/coq/stdlib/index_instance_J.html /usr/share/doc/packages/coq/stdlib/index_instance_K.html /usr/share/doc/packages/coq/stdlib/index_instance_L.html /usr/share/doc/packages/coq/stdlib/index_instance_M.html /usr/share/doc/packages/coq/stdlib/index_instance_N.html /usr/share/doc/packages/coq/stdlib/index_instance_O.html /usr/share/doc/packages/coq/stdlib/index_instance_P.html /usr/share/doc/packages/coq/stdlib/index_instance_Q.html /usr/share/doc/packages/coq/stdlib/index_instance_R.html /usr/share/doc/packages/coq/stdlib/index_instance_S.html /usr/share/doc/packages/coq/stdlib/index_instance_T.html /usr/share/doc/packages/coq/stdlib/index_instance_U.html /usr/share/doc/packages/coq/stdlib/index_instance_V.html /usr/share/doc/packages/coq/stdlib/index_instance_W.html /usr/share/doc/packages/coq/stdlib/index_instance_X.html /usr/share/doc/packages/coq/stdlib/index_instance_Y.html /usr/share/doc/packages/coq/stdlib/index_instance_Z.html /usr/share/doc/packages/coq/stdlib/index_instance__.html /usr/share/doc/packages/coq/stdlib/index_lemma_*.html /usr/share/doc/packages/coq/stdlib/index_lemma_A.html /usr/share/doc/packages/coq/stdlib/index_lemma_B.html /usr/share/doc/packages/coq/stdlib/index_lemma_C.html /usr/share/doc/packages/coq/stdlib/index_lemma_D.html /usr/share/doc/packages/coq/stdlib/index_lemma_E.html /usr/share/doc/packages/coq/stdlib/index_lemma_F.html /usr/share/doc/packages/coq/stdlib/index_lemma_G.html /usr/share/doc/packages/coq/stdlib/index_lemma_H.html /usr/share/doc/packages/coq/stdlib/index_lemma_I.html /usr/share/doc/packages/coq/stdlib/index_lemma_J.html /usr/share/doc/packages/coq/stdlib/index_lemma_K.html /usr/share/doc/packages/coq/stdlib/index_lemma_L.html /usr/share/doc/packages/coq/stdlib/index_lemma_M.html /usr/share/doc/packages/coq/stdlib/index_lemma_N.html /usr/share/doc/packages/coq/stdlib/index_lemma_O.html /usr/share/doc/packages/coq/stdlib/index_lemma_P.html /usr/share/doc/packages/coq/stdlib/index_lemma_Q.html /usr/share/doc/packages/coq/stdlib/index_lemma_R.html /usr/share/doc/packages/coq/stdlib/index_lemma_S.html /usr/share/doc/packages/coq/stdlib/index_lemma_T.html /usr/share/doc/packages/coq/stdlib/index_lemma_U.html /usr/share/doc/packages/coq/stdlib/index_lemma_V.html /usr/share/doc/packages/coq/stdlib/index_lemma_W.html /usr/share/doc/packages/coq/stdlib/index_lemma_X.html /usr/share/doc/packages/coq/stdlib/index_lemma_Y.html /usr/share/doc/packages/coq/stdlib/index_lemma_Z.html /usr/share/doc/packages/coq/stdlib/index_lemma__.html /usr/share/doc/packages/coq/stdlib/index_library_*.html /usr/share/doc/packages/coq/stdlib/index_library_A.html /usr/share/doc/packages/coq/stdlib/index_library_B.html /usr/share/doc/packages/coq/stdlib/index_library_C.html /usr/share/doc/packages/coq/stdlib/index_library_D.html /usr/share/doc/packages/coq/stdlib/index_library_E.html /usr/share/doc/packages/coq/stdlib/index_library_F.html /usr/share/doc/packages/coq/stdlib/index_library_G.html /usr/share/doc/packages/coq/stdlib/index_library_H.html /usr/share/doc/packages/coq/stdlib/index_library_I.html /usr/share/doc/packages/coq/stdlib/index_library_J.html /usr/share/doc/packages/coq/stdlib/index_library_K.html /usr/share/doc/packages/coq/stdlib/index_library_L.html /usr/share/doc/packages/coq/stdlib/index_library_M.html /usr/share/doc/packages/coq/stdlib/index_library_N.html /usr/share/doc/packages/coq/stdlib/index_library_O.html /usr/share/doc/packages/coq/stdlib/index_library_P.html /usr/share/doc/packages/coq/stdlib/index_library_Q.html /usr/share/doc/packages/coq/stdlib/index_library_R.html /usr/share/doc/packages/coq/stdlib/index_library_S.html /usr/share/doc/packages/coq/stdlib/index_library_T.html /usr/share/doc/packages/coq/stdlib/index_library_U.html /usr/share/doc/packages/coq/stdlib/index_library_V.html /usr/share/doc/packages/coq/stdlib/index_library_W.html /usr/share/doc/packages/coq/stdlib/index_library_X.html /usr/share/doc/packages/coq/stdlib/index_library_Y.html /usr/share/doc/packages/coq/stdlib/index_library_Z.html /usr/share/doc/packages/coq/stdlib/index_library__.html /usr/share/doc/packages/coq/stdlib/index_module_*.html /usr/share/doc/packages/coq/stdlib/index_module_A.html /usr/share/doc/packages/coq/stdlib/index_module_B.html /usr/share/doc/packages/coq/stdlib/index_module_C.html /usr/share/doc/packages/coq/stdlib/index_module_D.html /usr/share/doc/packages/coq/stdlib/index_module_E.html /usr/share/doc/packages/coq/stdlib/index_module_F.html /usr/share/doc/packages/coq/stdlib/index_module_G.html /usr/share/doc/packages/coq/stdlib/index_module_H.html /usr/share/doc/packages/coq/stdlib/index_module_I.html /usr/share/doc/packages/coq/stdlib/index_module_J.html /usr/share/doc/packages/coq/stdlib/index_module_K.html /usr/share/doc/packages/coq/stdlib/index_module_L.html /usr/share/doc/packages/coq/stdlib/index_module_M.html /usr/share/doc/packages/coq/stdlib/index_module_N.html /usr/share/doc/packages/coq/stdlib/index_module_O.html /usr/share/doc/packages/coq/stdlib/index_module_P.html /usr/share/doc/packages/coq/stdlib/index_module_Q.html /usr/share/doc/packages/coq/stdlib/index_module_R.html /usr/share/doc/packages/coq/stdlib/index_module_S.html /usr/share/doc/packages/coq/stdlib/index_module_T.html /usr/share/doc/packages/coq/stdlib/index_module_U.html /usr/share/doc/packages/coq/stdlib/index_module_V.html /usr/share/doc/packages/coq/stdlib/index_module_W.html /usr/share/doc/packages/coq/stdlib/index_module_X.html /usr/share/doc/packages/coq/stdlib/index_module_Y.html /usr/share/doc/packages/coq/stdlib/index_module_Z.html /usr/share/doc/packages/coq/stdlib/index_module__.html /usr/share/doc/packages/coq/stdlib/index_notation_*.html /usr/share/doc/packages/coq/stdlib/index_notation_A.html /usr/share/doc/packages/coq/stdlib/index_notation_B.html /usr/share/doc/packages/coq/stdlib/index_notation_C.html /usr/share/doc/packages/coq/stdlib/index_notation_D.html /usr/share/doc/packages/coq/stdlib/index_notation_E.html /usr/share/doc/packages/coq/stdlib/index_notation_F.html /usr/share/doc/packages/coq/stdlib/index_notation_G.html /usr/share/doc/packages/coq/stdlib/index_notation_H.html /usr/share/doc/packages/coq/stdlib/index_notation_I.html /usr/share/doc/packages/coq/stdlib/index_notation_J.html /usr/share/doc/packages/coq/stdlib/index_notation_K.html /usr/share/doc/packages/coq/stdlib/index_notation_L.html /usr/share/doc/packages/coq/stdlib/index_notation_M.html /usr/share/doc/packages/coq/stdlib/index_notation_N.html /usr/share/doc/packages/coq/stdlib/index_notation_O.html /usr/share/doc/packages/coq/stdlib/index_notation_P.html /usr/share/doc/packages/coq/stdlib/index_notation_Q.html /usr/share/doc/packages/coq/stdlib/index_notation_R.html /usr/share/doc/packages/coq/stdlib/index_notation_S.html /usr/share/doc/packages/coq/stdlib/index_notation_T.html /usr/share/doc/packages/coq/stdlib/index_notation_U.html /usr/share/doc/packages/coq/stdlib/index_notation_V.html /usr/share/doc/packages/coq/stdlib/index_notation_W.html /usr/share/doc/packages/coq/stdlib/index_notation_X.html /usr/share/doc/packages/coq/stdlib/index_notation_Y.html /usr/share/doc/packages/coq/stdlib/index_notation_Z.html /usr/share/doc/packages/coq/stdlib/index_notation__.html /usr/share/doc/packages/coq/stdlib/index_projection_*.html /usr/share/doc/packages/coq/stdlib/index_projection_A.html /usr/share/doc/packages/coq/stdlib/index_projection_B.html /usr/share/doc/packages/coq/stdlib/index_projection_C.html /usr/share/doc/packages/coq/stdlib/index_projection_D.html /usr/share/doc/packages/coq/stdlib/index_projection_E.html /usr/share/doc/packages/coq/stdlib/index_projection_F.html /usr/share/doc/packages/coq/stdlib/index_projection_G.html /usr/share/doc/packages/coq/stdlib/index_projection_H.html /usr/share/doc/packages/coq/stdlib/index_projection_I.html /usr/share/doc/packages/coq/stdlib/index_projection_J.html /usr/share/doc/packages/coq/stdlib/index_projection_K.html /usr/share/doc/packages/coq/stdlib/index_projection_L.html /usr/share/doc/packages/coq/stdlib/index_projection_M.html /usr/share/doc/packages/coq/stdlib/index_projection_N.html /usr/share/doc/packages/coq/stdlib/index_projection_O.html /usr/share/doc/packages/coq/stdlib/index_projection_P.html /usr/share/doc/packages/coq/stdlib/index_projection_Q.html /usr/share/doc/packages/coq/stdlib/index_projection_R.html /usr/share/doc/packages/coq/stdlib/index_projection_S.html /usr/share/doc/packages/coq/stdlib/index_projection_T.html /usr/share/doc/packages/coq/stdlib/index_projection_U.html /usr/share/doc/packages/coq/stdlib/index_projection_V.html /usr/share/doc/packages/coq/stdlib/index_projection_W.html /usr/share/doc/packages/coq/stdlib/index_projection_X.html /usr/share/doc/packages/coq/stdlib/index_projection_Y.html /usr/share/doc/packages/coq/stdlib/index_projection_Z.html /usr/share/doc/packages/coq/stdlib/index_projection__.html /usr/share/doc/packages/coq/stdlib/index_record_*.html /usr/share/doc/packages/coq/stdlib/index_record_A.html /usr/share/doc/packages/coq/stdlib/index_record_B.html /usr/share/doc/packages/coq/stdlib/index_record_C.html /usr/share/doc/packages/coq/stdlib/index_record_D.html /usr/share/doc/packages/coq/stdlib/index_record_E.html /usr/share/doc/packages/coq/stdlib/index_record_F.html /usr/share/doc/packages/coq/stdlib/index_record_G.html /usr/share/doc/packages/coq/stdlib/index_record_H.html /usr/share/doc/packages/coq/stdlib/index_record_I.html /usr/share/doc/packages/coq/stdlib/index_record_J.html /usr/share/doc/packages/coq/stdlib/index_record_K.html /usr/share/doc/packages/coq/stdlib/index_record_L.html /usr/share/doc/packages/coq/stdlib/index_record_M.html /usr/share/doc/packages/coq/stdlib/index_record_N.html /usr/share/doc/packages/coq/stdlib/index_record_O.html /usr/share/doc/packages/coq/stdlib/index_record_P.html /usr/share/doc/packages/coq/stdlib/index_record_Q.html /usr/share/doc/packages/coq/stdlib/index_record_R.html /usr/share/doc/packages/coq/stdlib/index_record_S.html /usr/share/doc/packages/coq/stdlib/index_record_T.html /usr/share/doc/packages/coq/stdlib/index_record_U.html /usr/share/doc/packages/coq/stdlib/index_record_V.html /usr/share/doc/packages/coq/stdlib/index_record_W.html /usr/share/doc/packages/coq/stdlib/index_record_X.html /usr/share/doc/packages/coq/stdlib/index_record_Y.html /usr/share/doc/packages/coq/stdlib/index_record_Z.html /usr/share/doc/packages/coq/stdlib/index_record__.html /usr/share/doc/packages/coq/stdlib/index_section_*.html /usr/share/doc/packages/coq/stdlib/index_section_A.html /usr/share/doc/packages/coq/stdlib/index_section_B.html /usr/share/doc/packages/coq/stdlib/index_section_C.html /usr/share/doc/packages/coq/stdlib/index_section_D.html /usr/share/doc/packages/coq/stdlib/index_section_E.html /usr/share/doc/packages/coq/stdlib/index_section_F.html /usr/share/doc/packages/coq/stdlib/index_section_G.html /usr/share/doc/packages/coq/stdlib/index_section_H.html /usr/share/doc/packages/coq/stdlib/index_section_I.html /usr/share/doc/packages/coq/stdlib/index_section_J.html /usr/share/doc/packages/coq/stdlib/index_section_K.html /usr/share/doc/packages/coq/stdlib/index_section_L.html /usr/share/doc/packages/coq/stdlib/index_section_M.html /usr/share/doc/packages/coq/stdlib/index_section_N.html /usr/share/doc/packages/coq/stdlib/index_section_O.html /usr/share/doc/packages/coq/stdlib/index_section_P.html /usr/share/doc/packages/coq/stdlib/index_section_Q.html /usr/share/doc/packages/coq/stdlib/index_section_R.html /usr/share/doc/packages/coq/stdlib/index_section_S.html /usr/share/doc/packages/coq/stdlib/index_section_T.html /usr/share/doc/packages/coq/stdlib/index_section_U.html /usr/share/doc/packages/coq/stdlib/index_section_V.html /usr/share/doc/packages/coq/stdlib/index_section_W.html /usr/share/doc/packages/coq/stdlib/index_section_X.html /usr/share/doc/packages/coq/stdlib/index_section_Y.html /usr/share/doc/packages/coq/stdlib/index_section_Z.html /usr/share/doc/packages/coq/stdlib/index_section__.html /usr/share/doc/packages/coq/stdlib/index_variable_*.html /usr/share/doc/packages/coq/stdlib/index_variable_A.html /usr/share/doc/packages/coq/stdlib/index_variable_B.html /usr/share/doc/packages/coq/stdlib/index_variable_C.html /usr/share/doc/packages/coq/stdlib/index_variable_D.html /usr/share/doc/packages/coq/stdlib/index_variable_E.html /usr/share/doc/packages/coq/stdlib/index_variable_F.html /usr/share/doc/packages/coq/stdlib/index_variable_G.html /usr/share/doc/packages/coq/stdlib/index_variable_H.html /usr/share/doc/packages/coq/stdlib/index_variable_I.html /usr/share/doc/packages/coq/stdlib/index_variable_J.html /usr/share/doc/packages/coq/stdlib/index_variable_K.html /usr/share/doc/packages/coq/stdlib/index_variable_L.html /usr/share/doc/packages/coq/stdlib/index_variable_M.html /usr/share/doc/packages/coq/stdlib/index_variable_N.html /usr/share/doc/packages/coq/stdlib/index_variable_O.html /usr/share/doc/packages/coq/stdlib/index_variable_P.html /usr/share/doc/packages/coq/stdlib/index_variable_Q.html /usr/share/doc/packages/coq/stdlib/index_variable_R.html /usr/share/doc/packages/coq/stdlib/index_variable_S.html /usr/share/doc/packages/coq/stdlib/index_variable_T.html /usr/share/doc/packages/coq/stdlib/index_variable_U.html /usr/share/doc/packages/coq/stdlib/index_variable_V.html /usr/share/doc/packages/coq/stdlib/index_variable_W.html /usr/share/doc/packages/coq/stdlib/index_variable_X.html /usr/share/doc/packages/coq/stdlib/index_variable_Y.html /usr/share/doc/packages/coq/stdlib/index_variable_Z.html /usr/share/doc/packages/coq/stdlib/index_variable__.html
Generated by rpm2html 1.8.1
Fabrice Bellet, Tue Jul 9 17:26:31 2024