diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/credits.rst | 189 | ||||
| -rw-r--r-- | doc/sphinx/language/cic.rst | 10 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 5 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 39 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 3 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 4 | ||||
| -rw-r--r-- | doc/stdlib/hidden-files | 78 | ||||
| -rw-r--r-- | doc/stdlib/index-list.html.template | 12 | ||||
| -rwxr-xr-x | doc/stdlib/make-library-index | 25 |
9 files changed, 300 insertions, 65 deletions
diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits.rst index ffdc4f3ec6..909af6e2f2 100644 --- a/doc/sphinx/credits.rst +++ b/doc/sphinx/credits.rst @@ -120,7 +120,7 @@ G. Dowek, allowed hierarchical developments of mathematical theories. This high-level language was called the *Mathematical Vernacular*. Furthermore, an interactive *Theorem Prover* permitted the incremental construction of proof trees in a top-down manner, subgoaling recursively -and backtracking from dead-alleys. The theorem prover executed tactics +and backtracking from dead-ends. The theorem prover executed tactics written in CAML, in the LCF fashion. A basic set of tactics was predefined, which the user could extend by his own specific tactics. This system (Version 4.10) was released in 1989. Then, the system was @@ -557,7 +557,7 @@ Pierre Courtieu, Julien Forest and Yves Bertot added extra support to reason on the inductive structure of recursively defined functions. Jean-Marc Notin significantly contributed to the general maintenance of -the system. He also took care of `coqdoc`. +the system. He also took care of ``coqdoc``. Pierre Castéran contributed to the documentation of (co-)inductive types and suggested improvements to the libraries. @@ -642,7 +642,7 @@ improvements, Jean-Marc Notin provided help in debugging, general maintenance and coqdoc support, Vincent Siles contributed extensions of the Scheme command and of injection. -Bruno Barras implemented the `coqchk` tool: this is a stand-alone +Bruno Barras implemented the ``coqchk`` tool: this is a stand-alone type checker that can be used to certify .vo files. Especially, as this verifier runs in a separate process, it is granted not to be “hijacked” by virtually malicious extensions added to |Coq|. @@ -817,12 +817,12 @@ expressions occurring in the goal by pattern in tactics such as set or destruct. Hugo Herbelin also relied on ideas from Chung-Kil Hur’s Heq plugin to introduce automatic computation of occurrences to generalize when using destruct and induction on types with indices. Stéphane Glondu -introduced new tactics constr\_eq, is\_evar and has\_evar to be used +introduced new tactics :tacn:`constr_eq`, :tacn:`is_evar`, and :tacn:`has_evar`, to be used when writing complex tactics. Enrico Tassi added support to fine-tuning -the behavior of simpl. Enrico Tassi added the ability to specify over +the behavior of :tacn:`simpl`. Enrico Tassi added the ability to specify over which variables of a section a lemma has to be exactly generalized. Pierre Letouzey added a tactic timeout and the interruptibility of -vm\_compute. Bug fixes and miscellaneous improvements of the tactic +:tacn:`vm_compute`. Bug fixes and miscellaneous improvements of the tactic language came from Hugo Herbelin, Pierre Letouzey and Matthieu Sozeau. Regarding decision tactics, Loïc Pottier maintained nsatz, moving in @@ -866,7 +866,7 @@ Pierre Courtieu and Arnaud Spiwack contributed new features for using Coq through Proof General. The Dp plugin has been removed. Use the plugin provided with Why 3 -instead (http://why3.lri.fr). +instead (http://why3.lri.fr/). Under the hood, the |Coq| architecture benefited from improvements in terms of efficiency and robustness, especially regarding universes @@ -982,7 +982,7 @@ working at the IAS in Princeton. The guard condition has been made compliant with extensional equality principles such as propositional extensionality and univalence, thanks to Maxime Dénès and Bruno Barras. To ensure compatibility with the -univalence axiom, a new flag “-indices-matter” has been implemented, +univalence axiom, a new flag ``-indices-matter`` has been implemented, taking into account the universe levels of indices when computing the levels of inductive types. This supports using |Coq| as a tool to explore the relations between homotopy theory and type theory. @@ -997,7 +997,7 @@ and improvements regarding the different components of the system. We shall only list a few of them. Pierre Boutillier developed an improved tactic for simplification of -expressions called cbn. +expressions called :tacn:`cbn`. Maxime Dénès maintained the bytecode-based reduction machine. Pierre Letouzey maintained the extraction mechanism. @@ -1069,7 +1069,7 @@ over 100 contributions integrated. The main user visible changes are: document. - More access to the proof engine features from Ltac: goal management - primitives, range selectors and a ``typeclasses eauto`` engine handling + primitives, range selectors and a :tacn:`typeclasses eauto` engine handling multiple goals and multiple successes, by Cyprien Mangin, Matthieu Sozeau and Arnaud Spiwack. @@ -1199,25 +1199,25 @@ Credits: version 8.7 and cleanups of the internals of the system along with a few new features. The main user visible changes are: -- New tactics: variants of tactics supporting existential variables eassert, - eenough, etc... by Hugo Herbelin. Tactics extensionality in H and - inversion_sigma by Jason Gross, specialize with ... accepting partial bindings +- New tactics: variants of tactics supporting existential variables :tacn:`eassert`, + :tacn:`eenough`, etc... by Hugo Herbelin. Tactics ``extensionality in H`` and + :tacn:`inversion_sigma` by Jason Gross, ``specialize with ...`` accepting partial bindings by Pierre Courtieu. -- Cumulative Polymorphic Inductive Types, allowing cumulativity of universes to +- ``Cumulative Polymorphic Inductive`` types, allowing cumulativity of universes to go through applied inductive types, by Amin Timany and Matthieu Sozeau. - Integration of the SSReflect plugin and its documentation in the reference manual, by Enrico Tassi, Assia Mahboubi and Maxime Dénès. -- The coq_makefile tool was completely redesigned to improve its maintainability - and the extensibility of generated Makefiles, and to make `_CoqProject` files +- The ``coq_makefile`` tool was completely redesigned to improve its maintainability + and the extensibility of generated Makefiles, and to make ``_CoqProject`` files more palatable to IDEs by Enrico Tassi. |Coq| 8.7 involved a large amount of work on cleaning and speeding up the code base, notably the work of Pierre-Marie Pédrot on making the tactic-level system insensitive to existential variable expansion, providing a safer API to plugin -writers and making the code more robust. The `dev/doc/changes.txt` file +writers and making the code more robust. The ``dev/doc/changes.txt`` file documents the numerous changes to the implementation and improvements of interfaces. An effort to provide an official, streamlined API to plugin writers is in progress, thanks to the work of Matej Košík. @@ -1238,8 +1238,8 @@ The BigN, BigZ, BigQ libraries are no longer part of the |Coq| standard library, they are now provided by a separate repository https://github.com/coq/bignums, maintained by Pierre Letouzey. -In the Reals library, `IZR` has been changed to produce a compact representation -of integers and real constants are now represented using `IZR` (work by +In the Reals library, ``IZR`` has been changed to produce a compact representation +of integers and real constants are now represented using ``IZR`` (work by Guillaume Melquiond). Standard library additions and improvements by Jason Gross, Pierre Letouzey and @@ -1346,7 +1346,7 @@ with a few new features. The main user visible changes are: Laurence Rideau, Matthieu Sozeau, Paul Steckler, Enrico Tassi, Laurent Théry, Nikita Zyuzin. -- Tools: experimental ``-mangle-names`` option to coqtop/coqc for +- Tools: experimental ``-mangle-names`` option to ``coqtop``/``coqc`` for linting proof scripts, by Jasper Hugunin. On the implementation side, the ``dev/doc/changes.md`` file @@ -1370,7 +1370,7 @@ maintaining and improving the continuous integration system. The OPAM repository for |Coq| packages has been maintained by Guillaume Melquiond, Matthieu Sozeau, Enrico Tassi with contributions from many -users. A list of packages is available at https://coq.inria.fr/opam/www. +users. A list of packages is available at https://coq.inria.fr/opam/www/. The 44 contributors for this version are Yves Bertot, Joachim Breitner, Tej Chajed, Arthur Charguéraud, Jacques-Pascal Deplaix, Maxime Dénès, Jim Fehrle, @@ -1404,3 +1404,150 @@ The contacts of the Coq Consortium are Yves Bertot and Maxime Dénès. | Santiago de Chile, March 2018, | Matthieu Sozeau for the |Coq| development team | + +Credits: version 8.9 +-------------------- + +|Coq| version 8.9 contains the result of refinements and stabilization +of features and deprecations or removals of deprecated features, +cleanups of the internals of the system and API along with a few new +features. This release includes many user-visible changes, including +deprecations that are documented in ``CHANGES.md`` and new features that +are documented in the reference manual. Here are the most important +changes: + +- Kernel: mutually recursive records are now supported, by Pierre-Marie + Pédrot. + +- Notations: + + - Support for autonomous grammars of terms called “custom entries”, by + Hugo Herbelin (see Section :ref:`custom-entries` of the reference + manual). + + - Deprecated notations of the standard library will be removed in the + next version of |Coq|, see the ``CHANGES.md`` file for a script to + ease porting, by Jason Gross and Jean-Christophe Léchenet. + + - Added the :cmd:`Numeral Notation` command for registering decimal + numeral notations for custom types, by Daniel de Rauglaudre, Pierre + Letouzey and Jason Gross. + +- Tactics: Introduction tactics :tacn:`intro`/:tacn:`intros` on a goal that is an + existential variable now force a refinement of the goal into a + dependent product rather than failing, by Hugo Herbelin. + +- Decision procedures: deprecation of tactic ``romega`` in favor of + :tacn:`lia` and removal of ``fourier``, replaced by :tacn:`lra` which + subsumes it, by Frédéric Besson, Maxime Dénès, Vincent Laporte and + Laurent Théry. + +- Proof language: focusing bracket ``{`` now supports named + :ref:`goals <curly-braces>`, e.g. ``[x]:{`` will focus + on a goal (existential variable) named ``x``, by Théo Zimmermann. + +- SSReflect: the implementation of delayed clear was simplified by + Enrico Tassi: 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 + :ref:`introduction_ssr`. + +- Vernacular: + + - Experimental support for :ref:`attributes <gallina-attributes>` on + commands, by Vincent Laporte, 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 :cmd:`Arguments`, with the help of Jasper + Hugunin. + + - New flag :flag:`Uniform Inductive Parameters` by Jasper Hugunin to + avoid repeating uniform parameters in constructor declarations. + + - New commands :cmd:`Hint Variables` and :cmd:`Hint Constants`, by + Matthieu Sozeau, for controlling the opacity status of variables and + constants in hint databases. It is recommended to always use these + commands after creating a hint databse with :cmd:`Create HintDb`. + + - Multiple sections with the same name are now allowed, by Jasper + Hugunin. + +- 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``, by various + contributors (source of incompatibility, see ``CHANGES.md`` for details). + +- Toplevels: ``coqtop`` and ``coqide`` can now display diffs between proof + steps in color, using the :opt:`Diffs` option, by Jim Fehrle. + +- Documentation: we integrated a large number of fixes to the new Sphinx + documentation by various contributors, coordinated by Clément + Pit-Claudel and Théo Zimmermann. + +- Tools: removed the ``gallina`` utility and the homebrewed ``Emacs`` mode. + +- Packaging: as in |Coq| 8.8.2, the Windows installer now includes many + more external packages that can be individually selected for + installation, by Michael Soegtrop. + +Version 8.9 also comes with a bunch of smaller-scale changes and +improvements regarding the different components of the system. Most +important ones are documented in the ``CHANGES.md`` file. + +On the implementation side, the ``dev/doc/changes.md`` file documents +the numerous changes to the implementation and improvements of +interfaces. The file provides guidelines on porting a plugin to the new +version and a plugin development tutorial kept in sync with Coq was +introduced by Yves Bertot http://github.com/ybertot/plugin_tutorials. +The new ``dev/doc/critical-bugs`` file documents the known critical bugs +of |Coq| and affected releases. + +The efficiency of the whole system has seen improvements thanks to +contributions from Gaëtan Gilbert, Pierre-Marie Pédrot, and Maxime Dénès. + +Maxime Dénès, Emilio Jesús Gallego Arias, Gaëtan Gilbert, Michael +Soegtrop, Théo Zimmermann worked on maintaining and improving the +continuous integration system. + +The OPAM repository for |Coq| packages has been maintained by Guillaume +Melquiond, Matthieu Sozeau, Enrico Tassi with contributions from many +users. A list of packages is available at https://coq.inria.fr/opam/www/. + +The 54 contributors for this version are Léo Andrès, Rin Arakaki, +Benjamin Barenblat, Langston Barrett, Siddharth Bhat, Martin Bodin, +Simon Boulier, Timothy Bourke, Joachim Breitner, Tej Chajed, Arthur +Charguéraud, Pierre Courtieu, Maxime Dénès, Andres Erbsen, Jim Fehrle, +Julien Forest, Emilio Jesus Gallego Arias, Gaëtan Gilbert, Matěj +Grabovský, Jason Gross, Samuel Gruetter, Armaël Guéneau, Hugo Herbelin, +Jasper Hugunin, Ralf Jung, Sam Pablo Kuper, Ambroise Lafont, Leonidas +Lampropoulos, Vincent Laporte, Peter LeFanu Lumsdaine, Pierre Letouzey, +Jean-Christophe Léchenet, Nick Lewycky, Yishuai Li, Sven M. Hallberg, +Assia Mahboubi, Cyprien Mangin, Guillaume Melquiond, Perry E. Metzger, +Clément Pit-Claudel, Pierre-Marie Pédrot, Daniel R. Grayson, Kazuhiko +Sakaguchi, Michael Soegtrop, Matthieu Sozeau, Paul Steckler, Enrico +Tassi, Laurent Théry, Anton Trunov, whitequark, Théo Winterhalter, +Zeimer, Beta Ziliani, Théo Zimmermann. + +Many power users helped to improve the design of the new features via +the issue and pull request system, the |Coq| development mailing list or +the coq-club@inria.fr mailing list. It would be impossible to mention +exhaustively the names of everybody who to some extent influenced the +development. + +Version 8.9 is the fourth release of |Coq| developed on a time-based +development cycle. Its development spanned 7 months from the release of +|Coq| 8.8. The development moved to a decentralized merging process +during this cycle. Guillaume Melquiond was in charge of the release +process and is the maintainer of this release. This release is the +result of ~2,000 commits and ~500 PRs merged, closing 75+ issues. + +The |Coq| development team welcomed Vincent Laporte, a new |Coq| +engineer working with Maxime Dénès in the |Coq| consortium. + +| Paris, November 2018, +| Matthieu Sozeau for the |Coq| development team +| diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 381f8bb661..cc5d9d6205 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -533,10 +533,10 @@ Convertibility Let us write :math:`E[Γ] ⊢ t \triangleright u` for the contextual closure of the relation :math:`t` reduces to :math:`u` in the global environment :math:`E` and local context :math:`Γ` with one of the previous -reductions β, ι, δ or ζ. +reductions β, δ, ι or ζ. We say that two terms :math:`t_1` and :math:`t_2` are -*βιδζη-convertible*, or simply *convertible*, or *equivalent*, in the +*βδιζη-convertible*, or simply *convertible*, or *equivalent*, in the global environment :math:`E` and local context :math:`Γ` iff there exist terms :math:`u_1` and :math:`u_2` such that :math:`E[Γ] ⊢ t_1 \triangleright … \triangleright u_1` and :math:`E[Γ] ⊢ t_2 \triangleright … \triangleright u_2` and either :math:`u_1` and @@ -678,7 +678,7 @@ form*. There are several ways (or strategies) to apply the reduction rules. Among them, we have to mention the *head reduction* which will play an important role (see Chapter :ref:`tactics`). Any term :math:`t` can be written as :math:`λ x_1 :T_1 . … λ x_k :T_k . (t_0~t_1 … t_n )` where :math:`t_0` is not an -application. We say then that :math:`t~0` is the *head of* :math:`t`. If we assume +application. We say then that :math:`t_0` is the *head of* :math:`t`. If we assume that :math:`t_0` is :math:`λ x:T. u_0` then one step of β-head reduction of :math:`t` is: .. math:: @@ -771,8 +771,8 @@ the sort of the inductive type t (not to be confused with :math:`\Sort` which is \odd&:&\nat → \Prop \end{array}\right]} {\left[\begin{array}{rcl} \evenO &:& \even~0\\ - \evenS &:& \forall n, \odd~n -> \even~(\kw{S}~n)\\ - \oddS &:& \forall n, \even~n -> \odd~(\kw{S}~n) + \evenS &:& \forall n, \odd~n → \even~(\kw{S}~n)\\ + \oddS &:& \forall n, \even~n → \odd~(\kw{S}~n) \end{array}\right]} which corresponds to the result of the |Coq| declaration: diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index c802f44ac1..741f9fe5b0 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -144,8 +144,9 @@ list of assertion commands is given in :ref:`Assertions`. The command the proof is a subset of the declared one. The set of declared variables is closed under type dependency. For - example if ``T`` is variable and a is a variable of type ``T``, the commands - ``Proof using a`` and ``Proof using T a`` are actually equivalent. + example, if ``T`` is a variable and ``a`` is a variable of type + ``T``, then the commands ``Proof using a`` and ``Proof using T a`` + are equivalent. .. cmdv:: Proof using {+ @ident } with @tactic diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 52609546d5..3ca0ffe678 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -916,11 +916,8 @@ but also folds ``x`` in the goal. .. coqtop:: reset From Coq Require Import ssreflect. - Set Implicit Arguments. - Unset Strict Implicit. - Unset Printing Implicit Defensive. - .. coqtop:: all undo + .. coqtop:: all Lemma test x t (Hx : x = 3) : x + t = 4. set z := 3 in Hx. @@ -929,6 +926,10 @@ If the localization also mentions the goal, then the result is the following one .. example:: + .. coqtop:: reset + + From Coq Require Import ssreflect. + .. coqtop:: all Lemma test x t (Hx : x = 3) : x + t = 4. @@ -2485,8 +2486,7 @@ destruction of existential assumptions like in the tactic: .. coqtop:: all Lemma test : True. - have [x Px]: exists x : nat, x > 0. - Focus 2. + have [x Px]: exists x : nat, x > 0; last first. An alternative use of the ``have`` tactic is to provide the explicit proof term for the intermediate lemma, using tactics of the form: @@ -2564,8 +2564,7 @@ copying the goal itself. .. coqtop:: all Lemma test : True. - have suff H : 2 + 2 = 3. - Focus 2. + have suff H : 2 + 2 = 3; last first. Note that H is introduced in the second goal. @@ -2852,8 +2851,7 @@ pattern will be used to process its instance. .. coqtop:: all Lemma simple n (ngt0 : 0 < n ) : P n. - gen have ltnV, /andP[nge0 neq0] : n ngt0 / (0 <= n) && (n != 0). - Focus 2. + gen have ltnV, /andP[nge0 neq0] : n ngt0 / (0 <= n) && (n != 0); last first. .. _advanced_generalization_ssr: @@ -3556,6 +3554,7 @@ corresponding new goals will be generated. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. + Set Warnings "-notation-overridden". .. coqtop:: all @@ -3756,9 +3755,10 @@ which the function is supplied: :name: congr This tactic: -+ checks that the goal is a Leibniz equality -+ matches both sides of this equality with “term applied to some arguments”, inferring the right number of arguments from the goal and the type of term. This may expand some definitions or fixpoints. -+ generates the subgoals corresponding to pairwise equalities of the arguments present in the goal. + + + checks that the goal is a Leibniz equality; + + matches both sides of this equality with “term applied to some arguments”, inferring the right number of arguments from the goal and the type of term. This may expand some definitions or fixpoints; + + generates the subgoals corresponding to pairwise equalities of the arguments present in the goal. The goal can be a non dependent product ``P -> Q``. In that case, the system asserts the equation ``P = Q``, uses it to solve the goal, and @@ -4918,7 +4918,7 @@ which produces the converse implication. In both cases, the two first Prop arguments are implicit. If ``term`` is an instance of the ``reflect`` predicate, then ``A`` will be one -of the defined view hints for the ``reflec``t predicate, which are by +of the defined view hints for the ``reflect`` predicate, which are by default the ones present in the file ``ssrbool.v``. These hints are not only used for choosing the appropriate direction of the translation, but they also allow complex transformation, involving negations. @@ -4933,9 +4933,9 @@ but they also allow complex transformation, involving negations. Unset Printing Implicit Defensive. Section Test. - .. coqtop:: in + .. coqtop:: all - Lemma introN : forall (P : Prop) (b : bool), reflect P b -> ~ P -> ~~b. + Check introN. .. coqtop:: all @@ -4945,12 +4945,11 @@ but they also allow complex transformation, involving negations. In fact this last script does not exactly use the hint ``introN``, but the more general hint: - .. coqtop:: in + .. coqtop:: all - Lemma introNTF : forall (P : Prop) (b c : bool), - reflect P b -> (if c then ~ P else P) -> ~~ b = c. + Check introNTF. - The lemma ` `introN`` is an instantiation of introNF using c := true. + The lemma ``introN`` is an instantiation of ``introNF`` using ``c := true``. Note that views, being part of :token:`i_pattern`, can be used to interpret assertions too. For example the following script asserts ``a && b`` but diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 26f4ec6242..457f9b2efa 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -2226,6 +2226,7 @@ and an explanation of the underlying technique. :n:`inversion @ident using @ident`. .. tacv:: inversion_sigma + :name: inversion_sigma This tactic turns equalities of dependent pairs (e.g., :g:`existT P x p = existT P y q`, frequently left over by inversion on @@ -2369,7 +2370,7 @@ and an explanation of the underlying technique. assumption. Qed. -.. tacn:: fix ident num +.. tacn:: fix @ident @num :name: fix This tactic is a primitive tactic to start a proof by induction. In diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 705d67e6c6..2214cbfb34 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -692,6 +692,8 @@ side. E.g.: Notation "'apply_id' f a1 .. an" := (.. (f a1) .. an) (at level 10, f ident, a1, an at level 9). +.. _custom-entries: + Custom entries ~~~~~~~~~~~~~~ @@ -1372,11 +1374,11 @@ Abbreviations denoted expression is performed at definition time. Type checking is done only at the time of use of the abbreviation. - Numeral notations ----------------- .. cmd:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope. + :name: Numeral Notation This command allows the user to customize the way numeral literals are parsed and printed. diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files index 8b13789179..b58148ffff 100644 --- a/doc/stdlib/hidden-files +++ b/doc/stdlib/hidden-files @@ -1 +1,77 @@ - +plugins/btauto/Algebra.v +plugins/btauto/Btauto.v +plugins/btauto/Reflect.v +plugins/derive/Derive.v +plugins/extraction/ExtrHaskellBasic.v +plugins/extraction/ExtrHaskellNatInt.v +plugins/extraction/ExtrHaskellNatInteger.v +plugins/extraction/ExtrHaskellNatNum.v +plugins/extraction/ExtrHaskellString.v +plugins/extraction/ExtrHaskellZInt.v +plugins/extraction/ExtrHaskellZInteger.v +plugins/extraction/ExtrHaskellZNum.v +plugins/extraction/ExtrOcamlBasic.v +plugins/extraction/ExtrOcamlBigIntConv.v +plugins/extraction/ExtrOcamlIntConv.v +plugins/extraction/ExtrOcamlNatBigInt.v +plugins/extraction/ExtrOcamlNatInt.v +plugins/extraction/ExtrOcamlString.v +plugins/extraction/ExtrOcamlZBigInt.v +plugins/extraction/ExtrOcamlZInt.v +plugins/extraction/Extraction.v +plugins/funind/FunInd.v +plugins/funind/Recdef.v +plugins/ltac/Ltac.v +plugins/micromega/Env.v +plugins/micromega/EnvRing.v +plugins/micromega/Fourier.v +plugins/micromega/Fourier_util.v +plugins/micromega/Lia.v +plugins/micromega/Lqa.v +plugins/micromega/Lra.v +plugins/micromega/MExtraction.v +plugins/micromega/OrderedRing.v +plugins/micromega/Psatz.v +plugins/micromega/QMicromega.v +plugins/micromega/RMicromega.v +plugins/micromega/Refl.v +plugins/micromega/RingMicromega.v +plugins/micromega/Tauto.v +plugins/micromega/VarMap.v +plugins/micromega/ZCoeff.v +plugins/micromega/ZMicromega.v +plugins/nsatz/Nsatz.v +plugins/omega/Omega.v +plugins/omega/OmegaLemmas.v +plugins/omega/OmegaPlugin.v +plugins/omega/OmegaTactic.v +plugins/omega/PreOmega.v +plugins/quote/Quote.v +plugins/romega/ROmega.v +plugins/romega/ReflOmegaCore.v +plugins/rtauto/Bintree.v +plugins/rtauto/Rtauto.v +plugins/setoid_ring/Algebra_syntax.v +plugins/setoid_ring/ArithRing.v +plugins/setoid_ring/BinList.v +plugins/setoid_ring/Cring.v +plugins/setoid_ring/Field.v +plugins/setoid_ring/Field_tac.v +plugins/setoid_ring/Field_theory.v +plugins/setoid_ring/InitialRing.v +plugins/setoid_ring/Integral_domain.v +plugins/setoid_ring/NArithRing.v +plugins/setoid_ring/Ncring.v +plugins/setoid_ring/Ncring_initial.v +plugins/setoid_ring/Ncring_polynom.v +plugins/setoid_ring/Ncring_tac.v +plugins/setoid_ring/RealField.v +plugins/setoid_ring/Ring.v +plugins/setoid_ring/Ring_base.v +plugins/setoid_ring/Ring_polynom.v +plugins/setoid_ring/Ring_tac.v +plugins/setoid_ring/Ring_theory.v +plugins/setoid_ring/Rings_Q.v +plugins/setoid_ring/Rings_R.v +plugins/setoid_ring/Rings_Z.v +plugins/setoid_ring/ZArithRing.v diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 4cbf75b715..64164cc56f 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -502,6 +502,7 @@ through the <tt>Require Import</tt> command.</p> theories/Strings/BinaryString.v theories/Strings/HexString.v theories/Strings/OctalString.v + theories/Strings/ByteVector.v </dd> <dt> <b>Reals</b>: @@ -587,6 +588,17 @@ through the <tt>Require Import</tt> command.</p> theories/Program/Combinators.v </dd> + <dt> <b>SSReflect</b>: + Base libraries for the SSReflect proof language and the + small scale reflection formalization technique + </dt> + <dd> + plugins/ssrmatching/ssrmatching.v + plugins/ssr/ssreflect.v + plugins/ssr/ssrbool.v + plugins/ssr/ssrfun.v + </dd> + <dt> <b>Unicode</b>: Unicode-based notations </dt> diff --git a/doc/stdlib/make-library-index b/doc/stdlib/make-library-index index 43802efa0a..bea6f24098 100755 --- a/doc/stdlib/make-library-index +++ b/doc/stdlib/make-library-index @@ -8,35 +8,32 @@ HIDDEN=$2 cp -f $FILE.template tmp echo -n "Building file index-list.prehtml... " -#LIBDIRS="Init Logic Structures Bool Arith PArith NArith ZArith QArith Relations Sets Classes Setoids Lists Vectors Sorting Wellfounded MSets FSets Reals Program Numbers Numbers/Natural/Abstract Numbers/Natural/Peano Numbers/Natural/Binary Numbers/Natural/BigN Numbers/Natural/SpecViaZ Numbers/Integer/Abstract Numbers/Integer/NatPairs Numbers/Integer/Binary Numbers/Integer/SpecViaZ Numbers/Integer/BigZ Numbers/NatInt Numbers/Cyclic/Abstract Numbers/Cyclic/Int31 Numbers/Cyclic/ZModulo Numbers/Cyclic/DoubleCyclic Numbers/Rational/BigQ Numbers/Rational/SpecViaQ Strings" -LIBDIRS=`find theories/* -type d ! -name .coq-native | sed -e "s:^theories/::"` +LIBDIRS=`find theories/* plugins/* -type d ! -name .coq-native` for k in $LIBDIRS; do - i=theories/$k - d=`basename $i` - ls $i | grep -q \.v'$' + d=`basename $k` + ls $k | grep -q \.v'$' if [ $? = 0 ]; then - for j in $i/*.v; do + for j in $k/*.v; do b=`basename $j .v` rm -f tmp2 - grep -q theories/$k/$b.v tmp + grep -q $k/$b.v tmp a=$? - grep -q theories/$k/$b.v $HIDDEN + grep -q $k/$b.v $HIDDEN h=$? if [ $a = 0 ]; then if [ $h = 0 ]; then - echo Error: $FILE and $HIDDEN both mention theories/$k/$b.v; exit 1 + echo Error: $FILE and $HIDDEN both mention $k/$b.v; exit 1 else - p=`echo $k | sed 's:/:.:g'` - sed -e "s:theories/$k/$b.v:<a href=\"Coq.$p.$b.html\">$b</a>:g" tmp > tmp2 + p=`echo $k | sed 's:^[^/]*/::' | sed 's:/:.:g'` + sed -e "s:$k/$b.v:<a href=\"Coq.$p.$b.html\">$b</a>:g" tmp > tmp2 mv -f tmp2 tmp fi else if [ $h = 0 ]; then - echo Error: theories/$k/$b.v is missing in the template file - exit 1 + echo Warning: $k/$b.v will be hidden from the index else - echo Error: none of $FILE and $HIDDEN mention theories/$k/$b.v + echo Error: none of $FILE and $HIDDEN mention $k/$b.v exit 1 fi |