diff options
Diffstat (limited to 'doc')
65 files changed, 686 insertions, 262 deletions
diff --git a/doc/README.md b/doc/README.md index ef3ccc2105..7fa6f5cf3d 100644 --- a/doc/README.md +++ b/doc/README.md @@ -96,7 +96,7 @@ Alternatively, you can use some specific targets: - `make refman-{html,pdf}` to produce only one format of the reference manual -- `make stdlib` +- `make doc-stdlib` to produce all formats of the Coq standard library diff --git a/doc/changelog/01-kernel/11081-native-cleanup.rst b/doc/changelog/01-kernel/11081-native-cleanup.rst deleted file mode 100644 index b3e3a78b96..0000000000 --- a/doc/changelog/01-kernel/11081-native-cleanup.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Changed:** the native compilation (:tacn:`native_compute`) now - creates a directory to contain temporary files instead of putting - them in the root of the system temporary directory. (`#11081 - <https://github.com/coq/coq/pull/11081>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/01-kernel/11361-fix-11360-discharge-template-param-var.rst b/doc/changelog/01-kernel/11361-fix-11360-discharge-template-param-var.rst deleted file mode 100644 index 8c84648aa7..0000000000 --- a/doc/changelog/01-kernel/11361-fix-11360-discharge-template-param-var.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Fixed:** `#11360 <https://github.com/issues/11360>`_ - Broken section closing when a template polymorphic inductive type depends on - a section variable through its parameters (`#11361 - <https://github.com/coq/coq/pull/11361>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/02-specification-language/10202-master+fix8011-stronger-check-on-typability-ltac-env.rst b/doc/changelog/02-specification-language/10202-master+fix8011-stronger-check-on-typability-ltac-env.rst new file mode 100644 index 0000000000..57bce7e4f6 --- /dev/null +++ b/doc/changelog/02-specification-language/10202-master+fix8011-stronger-check-on-typability-ltac-env.rst @@ -0,0 +1,7 @@ +- **Changed:** + Warn when manual implicit arguments are used in unexpected positions + of a term (e.g. in `Check id (forall {x}, x)`) or when a implicit + argument name is shadowed (e.g. in `Check fun f : forall {x:nat} + {x}, nat => f`) + (`#10202 <https://github.com/coq/coq/pull/10202>`_, + by Hugo Herbelin). diff --git a/doc/changelog/02-specification-language/10657-minim-toset-flex.rst b/doc/changelog/02-specification-language/10657-minim-toset-flex.rst deleted file mode 100644 index 8983e162fb..0000000000 --- a/doc/changelog/02-specification-language/10657-minim-toset-flex.rst +++ /dev/null @@ -1,3 +0,0 @@ -- Changed heuristics for universe minimization to :g:`Set`: only - minimize flexible universes (`#10657 <https://github.com/coq/coq/pull/10657>`_, - by Gaëtan Gilbert with help from Maxime Dénès and Matthieu Sozeau). diff --git a/doc/changelog/02-specification-language/11098-master+arguments-supports-anonymous-implicit.rst b/doc/changelog/02-specification-language/11098-master+arguments-supports-anonymous-implicit.rst new file mode 100644 index 0000000000..32526babdb --- /dev/null +++ b/doc/changelog/02-specification-language/11098-master+arguments-supports-anonymous-implicit.rst @@ -0,0 +1,8 @@ +- **Added:** + :cmd:`Arguments <Arguments (implicits)>` now supports setting + implicit an anonymous argument, as e.g. in :g:`Arguments id {A} {_}`. + (`#11098 <https://github.com/coq/coq/pull/11098>`_, + by Hugo Herbelin, fixes `#4696 + <https://github.com/coq/coq/pull/4696>`_, `#5173 + <https://github.com/coq/coq/pull/5173>`_, `#9098 + <https://github.com/coq/coq/pull/9098>`_.). diff --git a/doc/changelog/02-specification-language/11233-master+fix11231-missing-variable-pattern-matching-decompilation.rst b/doc/changelog/02-specification-language/11233-master+fix11231-missing-variable-pattern-matching-decompilation.rst deleted file mode 100644 index 941469d698..0000000000 --- a/doc/changelog/02-specification-language/11233-master+fix11231-missing-variable-pattern-matching-decompilation.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed:** - A dependency was missing when looking for default clauses in the - algorithm for printing pattern matching clauses (`#11233 - <https://github.com/coq/coq/pull/11233>`_, by Hugo Herbelin, fixing - `#11231 <https://github.com/coq/coq/pull/11231>`_, reported by Barry - Jay). diff --git a/doc/changelog/02-specification-language/11235-non_maximal_implicit.rst b/doc/changelog/02-specification-language/11235-non_maximal_implicit.rst new file mode 100644 index 0000000000..d8ff1fec31 --- /dev/null +++ b/doc/changelog/02-specification-language/11235-non_maximal_implicit.rst @@ -0,0 +1,6 @@ +- **Added:** + Syntax for non maximal implicit arguments in definitions and terms using + square brackets. The syntax is ``[x : A]``, ``[x]``, ```[A]`` + to be consistent with the command :cmd:`Arguments (implicits)`. + (`#11235 <https://github.com/coq/coq/pull/11235>`_, + by SimonBoulier). diff --git a/doc/changelog/02-specification-language/11261-master+implicit-type-used-printing.rst b/doc/changelog/02-specification-language/11261-master+implicit-type-used-printing.rst new file mode 100644 index 0000000000..51818c666b --- /dev/null +++ b/doc/changelog/02-specification-language/11261-master+implicit-type-used-printing.rst @@ -0,0 +1,5 @@ +- **Added:** + :cmd:`Implicit Types` are now taken into account for printing. To inhibit it, + unset the :flag:`Printing Use Implicit Types` flag + (`#11261 <https://github.com/coq/coq/pull/11261>`_, + by Hugo Herbelin, granting `#10366 <https://github.com/coq/coq/pull/10366>`_). diff --git a/doc/changelog/02-specification-language/11600-uniform-syntax.rst b/doc/changelog/02-specification-language/11600-uniform-syntax.rst new file mode 100644 index 0000000000..3fa3f80301 --- /dev/null +++ b/doc/changelog/02-specification-language/11600-uniform-syntax.rst @@ -0,0 +1,4 @@ +- **Added:** + New syntax :g:`Inductive Acc A R | x : Prop := ...` to specify which + parameters of an inductive are uniform. + (`#11600 <https://github.com/coq/coq/pull/11600>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/03-notations/10832-master+fix6082-7766-overriding-notation-format.rst b/doc/changelog/03-notations/10832-master+fix6082-7766-overriding-notation-format.rst new file mode 100644 index 0000000000..5393fb3d8c --- /dev/null +++ b/doc/changelog/03-notations/10832-master+fix6082-7766-overriding-notation-format.rst @@ -0,0 +1 @@ +- Different interpretations in different scopes of the same notation string can now be associated to different printing formats; this fixes bug #6092 and #7766 (`#10832 <https://github.com/coq/coq/pull/10832>`_, by Hugo Herbelin). diff --git a/doc/changelog/03-notations/11113-remove-compat.rst b/doc/changelog/03-notations/11113-remove-compat.rst index 8c71d70cda..3bcdd3dd6f 100644 --- a/doc/changelog/03-notations/11113-remove-compat.rst +++ b/doc/changelog/03-notations/11113-remove-compat.rst @@ -1,4 +1,4 @@ -- Removed deprecated ``compat`` modifier of :cmd:`Notation` +- **Removed:** deprecated ``compat`` modifier of :cmd:`Notation` and :cmd:`Infix` commands (`#11113 <https://github.com/coq/coq/pull/11113>`_, by Théo Zimmermann, with help from Jason Gross). diff --git a/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst b/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst new file mode 100644 index 0000000000..d95f554766 --- /dev/null +++ b/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst @@ -0,0 +1,17 @@ +- **Fixed:** Parsing and printing consistently handle inheritance of implicit + arguments in notations. With the exception of notations of + the form :n:`Notation @string := @@qualid` and :n:`Notation @ident := @@qualid` which + inhibit implicit arguments, all notations binding a partially + applied constant, as e.g. in :n:`Notation @string := (@qualid {+ @arg })`, + or :n:`Notation @string := (@@qualid {+ @arg })`, or + :n:`Notation @ident := (@qualid {+ @arg })`, or :n:`Notation @ident + := (@@qualid {+ @arg })`, inherit the remaining implicit arguments + (`#11120 <https://github.com/coq/coq/pull/11120>`_, by Hugo + Herbelin, fixing `#4690 <https://github.com/coq/coq/pull/4690>`_ and + `#11091 <https://github.com/coq/coq/pull/11091>`_). + +- **Changed:** Interpretation scopes are now always inherited in + notations binding a partially applied constant, including for + notations binding an expression of the form :n:`@@qualid`. The latter was + not the case beforehand + (part of `#11120 <https://github.com/coq/coq/pull/11120>`_). diff --git a/doc/changelog/03-notations/11172-master+coercion-notation-interleaved-printing.rst b/doc/changelog/03-notations/11172-master+coercion-notation-interleaved-printing.rst index 8551cf3aac..f377b53ae2 100644 --- a/doc/changelog/03-notations/11172-master+coercion-notation-interleaved-printing.rst +++ b/doc/changelog/03-notations/11172-master+coercion-notation-interleaved-printing.rst @@ -1,2 +1,3 @@ -- The printing algorithm now interleave search for notations and removal of coercions +- **Changed:** + The printing algorithm now interleaves search for notations and removal of coercions (`#11172 <https://github.com/coq/coq/pull/11172>`_, by Hugo Herbelin). diff --git a/doc/changelog/03-notations/11240-rew-dependent.rst b/doc/changelog/03-notations/11240-rew-dependent.rst new file mode 100644 index 0000000000..e9daab0c2c --- /dev/null +++ b/doc/changelog/03-notations/11240-rew-dependent.rst @@ -0,0 +1,5 @@ +- **Added** + Added :g:`rew dependent` notations for the dependent version of + :g:`rew` in :g:`Coq.Init.Logic.EqNotations` to improve the display + and parsing of :g:`match` statements on :g:`Logic.eq` (`#11240 + <https://github.com/coq/coq/pull/11240>`_, by Jason Gross). diff --git a/doc/changelog/03-notations/11276-master+fix10750.rst b/doc/changelog/03-notations/11276-master+fix10750.rst deleted file mode 100644 index a1b8594f5f..0000000000 --- a/doc/changelog/03-notations/11276-master+fix10750.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Fixed:** - :cmd:`Print Visibility` was failing in the presence of only-printing notations - (`#11276 <https://github.com/coq/coq/pull/11276>`_, - by Hugo Herbelin, fixing `#10750 <https://github.com/coq/coq/pull/10750>`_). diff --git a/doc/changelog/03-notations/11311-custom-entries-recursive.rst b/doc/changelog/03-notations/11311-custom-entries-recursive.rst deleted file mode 100644 index ae9888512d..0000000000 --- a/doc/changelog/03-notations/11311-custom-entries-recursive.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** - Recursive notations with custom entries were incorrectly parsing `constr` - instead of custom grammars (`#11311 <https://github.com/coq/coq/pull/11311>`_ - by Maxime Dénès, fixes `#9532 <https://github.com/coq/coq/pull/9532>`_, - `#9490 <https://github.com/coq/coq/pull/9490>`_). diff --git a/doc/changelog/03-notations/11530-master+fix11331-custom-entries-precedence.rst b/doc/changelog/03-notations/11530-master+fix11331-custom-entries-precedence.rst new file mode 100644 index 0000000000..b105928b22 --- /dev/null +++ b/doc/changelog/03-notations/11530-master+fix11331-custom-entries-precedence.rst @@ -0,0 +1,8 @@ +- **Fixed:** + Bugs in dealing with precedences of notations in custom entries + (`#11530 <https://github.com/coq/coq/pull/11530>`_, + by Hugo Herbelin, fixing in particular + `#9517 <https://github.com/coq/coq/pull/9517>`_, + `#9519 <https://github.com/coq/coq/pull/9519>`_, + `#9521 <https://github.com/coq/coq/pull/9521>`_, + `#11331 <https://github.com/coq/coq/pull/11331>`_). diff --git a/doc/changelog/03-notations/11590-master+fix9741-only-printing-does-not-reserve-keyword.rst b/doc/changelog/03-notations/11590-master+fix9741-only-printing-does-not-reserve-keyword.rst new file mode 100644 index 0000000000..1d94cbf21b --- /dev/null +++ b/doc/changelog/03-notations/11590-master+fix9741-only-printing-does-not-reserve-keyword.rst @@ -0,0 +1,4 @@ +- **Fixed:** + Notations in onlyprinting mode do not uselessly reserve parsing keywords + (`#11590 <https://github.com/coq/coq/pull/11590>`_, + by Hugo Herbelin, fixes `#9741 <https://github.com/coq/coq/pull/9741>`_). diff --git a/doc/changelog/04-tactics/10760-more-rapply.rst b/doc/changelog/04-tactics/10760-more-rapply.rst index 2815f8af8a..eeae2ec519 100644 --- a/doc/changelog/04-tactics/10760-more-rapply.rst +++ b/doc/changelog/04-tactics/10760-more-rapply.rst @@ -1,4 +1,5 @@ -- The tactic :tacn:`rapply` in :g:`Coq.Program.Tactics` now handles +- **Changed:** + The tactic :tacn:`rapply` in :g:`Coq.Program.Tactics` now handles arbitrary numbers of underscores and takes in a :g:`uconstr`. In rare cases where users were relying on :tacn:`rapply` inserting exactly 15 underscores and no more, due to the lemma having a diff --git a/doc/changelog/04-tactics/10762-notypeclasses-refine.rst b/doc/changelog/04-tactics/10762-notypeclasses-refine.rst deleted file mode 100644 index 2fef75dc7f..0000000000 --- a/doc/changelog/04-tactics/10762-notypeclasses-refine.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Changed:** - The tactics :tacn:`eapply`, :tacn:`refine` and its variants no - longer allows shelved goals to be solved by typeclass resolution. - (`#10762 <https://github.com/coq/coq/pull/10762>`_, by Matthieu Sozeau). diff --git a/doc/changelog/04-tactics/11023-nativecompute-timing.rst b/doc/changelog/04-tactics/11023-nativecompute-timing.rst new file mode 100644 index 0000000000..2afa3990ac --- /dev/null +++ b/doc/changelog/04-tactics/11023-nativecompute-timing.rst @@ -0,0 +1,7 @@ +- The :flag:`NativeCompute Timing` flag causes calls to + :tacn:`native_compute` (as well as kernel calls to the native + compiler) to emit separate timing information about compilation, + execution, and reification. It replaces the timing information + previously emitted when the `-debug` flag was set, and allows more + fine-grained timing of the native compiler. (`#11023 + <https://github.com/coq/coq/pull/11023>`_, by Jason Gross). diff --git a/doc/changelog/04-tactics/11203-fix-time-printing.rst b/doc/changelog/04-tactics/11203-fix-time-printing.rst deleted file mode 100644 index cdfd2b228e..0000000000 --- a/doc/changelog/04-tactics/11203-fix-time-printing.rst +++ /dev/null @@ -1,4 +0,0 @@ -- The optional string argument to :tacn:`time` is now properly quoted - under :cmd:`Print Ltac` (`#11203 - <https://github.com/coq/coq/pull/11203>`_, fixes `#10971 - <https://github.com/coq/coq/issues/10971>`_, by Jason Gross) diff --git a/doc/changelog/04-tactics/11263-micromega-fix.rst b/doc/changelog/04-tactics/11263-micromega-fix.rst deleted file mode 100644 index ebfb6c19b1..0000000000 --- a/doc/changelog/04-tactics/11263-micromega-fix.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed** - Efficiency regression introduced by PR `#9725 <https://github.com/coq/coq/pull/9725>`_. - (`#11263 <https://github.com/coq/coq/pull/11263>`_, - fixes `#11063 <https://github.com/coq/coq/issues/11063>`_, - and `#11242 <https://github.com/coq/coq/issues/11242>`_, - and `#11270 <https://github.com/coq/coq/issues/11270>`_, by Frédéric Besson). diff --git a/doc/changelog/04-tactics/11337-omega-with-depr.rst b/doc/changelog/04-tactics/11337-omega-with-depr.rst deleted file mode 100644 index 25e929e030..0000000000 --- a/doc/changelog/04-tactics/11337-omega-with-depr.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Deprecated:** - The undocumented ``omega with`` tactic variant has been deprecated, - using ``lia`` is the recommended replacement, tho the old semantics - of ``omega with *`` can be recovered with ``zify; omega`` - (`#11337 <https://github.com/coq/coq/pull/11337>`_, - by Emilio Jesus Gallego Arias). diff --git a/doc/changelog/04-tactics/11474-lia-bug-fix-11436.rst b/doc/changelog/04-tactics/11474-lia-bug-fix-11436.rst new file mode 100644 index 0000000000..2a341261e5 --- /dev/null +++ b/doc/changelog/04-tactics/11474-lia-bug-fix-11436.rst @@ -0,0 +1,9 @@ +- **Added:** + :cmd:`Show Lia Profile` prints some statistics about :tacn:`lia` calls. + (`#11474 <https://github.com/coq/coq/pull/11474>`_, by Frédéric Besson). + +- **Fixed:** + Efficiency regression of ``lia`` + (`#11474 <https://github.com/coq/coq/pull/11474>`_, + fixes `#11436 <https://github.com/coq/coq/issues/11436>`_, + by Frédéric Besson). diff --git a/doc/changelog/05-tactic-language/10343-issue-10342-ltac2-standard-library.rst b/doc/changelog/05-tactic-language/10343-issue-10342-ltac2-standard-library.rst new file mode 100644 index 0000000000..4acc423d10 --- /dev/null +++ b/doc/changelog/05-tactic-language/10343-issue-10342-ltac2-standard-library.rst @@ -0,0 +1,4 @@ +- **Added:** + An array library for ltac2 (OCaml standard library compatible where possible). + (`#10343 <https://github.com/coq/coq/pull/10343>`_, + by Michael Soegtrop). diff --git a/doc/changelog/05-tactic-language/11241-master+bug-cofix-with-8.10.rst b/doc/changelog/05-tactic-language/11241-master+bug-cofix-with-8.10.rst deleted file mode 100644 index 462ba4a7b1..0000000000 --- a/doc/changelog/05-tactic-language/11241-master+bug-cofix-with-8.10.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Fixed:** - Syntax of tactic `cofix ... with ...` was broken from Coq 8.10. - (`#11241 <https://github.com/coq/coq/pull/11241>`_, - by Hugo Herbelin). diff --git a/doc/changelog/07-commands-and-options/11162-local-cs.rst b/doc/changelog/07-commands-and-options/11162-local-cs.rst index 5a69a107cd..638222fbe1 100644 --- a/doc/changelog/07-commands-and-options/11162-local-cs.rst +++ b/doc/changelog/07-commands-and-options/11162-local-cs.rst @@ -1 +1,3 @@ -- Handle the ``#[local]`` attribute in :g:`Canonical Structure` declarations (`#11162 <https://github.com/coq/coq/pull/11162>`_, by Enrico Tassi). +- **Added:** Handle the ``#[local]`` attribute in :g:`Canonical + Structure` declarations (`#11162 + <https://github.com/coq/coq/pull/11162>`_, by Enrico Tassi). diff --git a/doc/changelog/07-commands-and-options/11164-let-cs.rst b/doc/changelog/07-commands-and-options/11164-let-cs.rst index b9ecd140e7..ec34c075ae 100644 --- a/doc/changelog/07-commands-and-options/11164-let-cs.rst +++ b/doc/changelog/07-commands-and-options/11164-let-cs.rst @@ -1 +1,3 @@ -- A section variable introduces with :g:`Let` can be declared as a :g:`Canonical Structure` (`#11164 <https://github.com/coq/coq/pull/11164>`_, by Enrico Tassi). +- **Added:** A section variable introduces with :g:`Let` can be + declared as a :g:`Canonical Structure` (`#11164 + <https://github.com/coq/coq/pull/11164>`_, by Enrico Tassi). diff --git a/doc/changelog/07-commands-and-options/11409-mltop+deprecate_use.rst b/doc/changelog/07-commands-and-options/11409-mltop+deprecate_use.rst new file mode 100644 index 0000000000..db433ad64c --- /dev/null +++ b/doc/changelog/07-commands-and-options/11409-mltop+deprecate_use.rst @@ -0,0 +1,5 @@ +- **Removed:** + The `-load-ml-source` and `-load-ml-object` command line options + have been removed; their use was very limited, you can achieve the same adding + additional object files in the linking step or using a plugin. + (`#11409 <https://github.com/coq/coq/pull/11409>`_, by Emilio Jesus Gallego Arias). diff --git a/doc/changelog/07-commands-and-options/11428-mltop+depr_lowlevel_dynloads.rst b/doc/changelog/07-commands-and-options/11428-mltop+depr_lowlevel_dynloads.rst deleted file mode 100644 index a43e950bff..0000000000 --- a/doc/changelog/07-commands-and-options/11428-mltop+depr_lowlevel_dynloads.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Deprecated:** - The `-load-ml-source` and `-load-ml-object` command line options - have been deprecated; their use was very limited, you can achieve the same adding - additional object files in the linking step or by using a plugin. - (`#11428 <https://github.com/coq/coq/pull/11428>`_, - by Emilio Jesus Gallego Arias). diff --git a/doc/changelog/07-commands-and-options/11617-toplevel+boot.rst b/doc/changelog/07-commands-and-options/11617-toplevel+boot.rst new file mode 100644 index 0000000000..49dd0ee2d8 --- /dev/null +++ b/doc/changelog/07-commands-and-options/11617-toplevel+boot.rst @@ -0,0 +1,5 @@ +- **Added:** + New ``coqc`` / ``coqtop`` option ``-boot`` that will not bind the + `Coq` library prefix by default + (`#11617 <https://github.com/coq/coq/pull/11617>`_, + by Emilio Jesus Gallego Arias). diff --git a/doc/changelog/08-tools/11255-master+fix11254-coqtop-version.rst b/doc/changelog/08-tools/11255-master+fix11254-coqtop-version.rst deleted file mode 100644 index ecc134748d..0000000000 --- a/doc/changelog/08-tools/11255-master+fix11254-coqtop-version.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Fixed:** - ``coqtop --version`` was broken when called in the middle of an installation process - (`#11255 <https://github.com/coq/coq/pull/11255>`_, by Hugo Herbelin, fixing - `#11254 <https://github.com/coq/coq/pull/11254>`_). diff --git a/doc/changelog/08-tools/11280-bugfix-11195-vos-vio-interaction.rst b/doc/changelog/08-tools/11280-bugfix-11195-vos-vio-interaction.rst deleted file mode 100644 index 97f456036d..0000000000 --- a/doc/changelog/08-tools/11280-bugfix-11195-vos-vio-interaction.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Deprecated:** - The ``-quick`` command is renamed to ``-vio``, for consistency with the new ``-vos`` and ``-vok`` flags. Usage of ``-quick`` is now deprecated. - (`#11280 <https://github.com/coq/coq/pull/11280>`_, - by charguer). diff --git a/doc/changelog/08-tools/11302-better-timing-scripts-options.rst b/doc/changelog/08-tools/11302-better-timing-scripts-options.rst new file mode 100644 index 0000000000..3b20bbf75d --- /dev/null +++ b/doc/changelog/08-tools/11302-better-timing-scripts-options.rst @@ -0,0 +1,35 @@ +- **Added:** + The ``make-both-single-timing-files.py`` script now accepts a + ``--fuzz=N`` parameter on the command line which determines how many + characters two lines may be offset in the "before" and "after" + timing logs while still being considered the same line. When + invoking this script via the ``print-pretty-single-time-diff`` + target in a ``Makefile`` made by ``coq_makefile``, you can set this + argument by passing ``TIMING_FUZZ=N`` to ``make`` (`#11302 + <https://github.com/coq/coq/pull/11302>`_, by Jason Gross). + +- **Added:** + The ``make-one-time-file.py`` and ``make-both-time-files.py`` + scripts now accept a ``--real`` parameter on the command line to + print real times rather than user times in the tables. The + ``make-both-single-timing-files.py`` script accepts a ``--user`` + parameter to use user times. When invoking these scripts via the + ``print-pretty-timed`` or ``print-pretty-timed-diff`` or + ``print-pretty-single-time-diff`` targets in a ``Makefile`` made by + ``coq_makefile``, you can set this argument by passing + ``TIMING_REAL=1`` (to pass ``--real``) or ``TIMING_REAL=0`` (to pass + ``--user``) to ``make`` (`#11302 + <https://github.com/coq/coq/pull/11302>`_, by Jason Gross). + +- **Added:** + Coq's build system now supports both ``TIMING_FUZZ``, + ``TIMING_SORT_BY``, and ``TIMING_REAL`` just like a ``Makefile`` + made by ``coq_makefile`` (`#11302 + <https://github.com/coq/coq/pull/11302>`_, by Jason Gross). + +- **Fixed:** + The various timing targets for Coq's standard library now correctly + display and label the "before" and "after" columns, rather than + mixing them up (`#11302 <https://github.com/coq/coq/pull/11302>`_ + fixes `#11301 <https://github.com/coq/coq/issues/11301>`_, by Jason + Gross). diff --git a/doc/changelog/08-tools/11357-master.rst b/doc/changelog/08-tools/11357-master.rst deleted file mode 100644 index 599db5b1da..0000000000 --- a/doc/changelog/08-tools/11357-master.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Fixed:** - ``coq_makefile`` does not break when using the ``CAMLPKGS`` variable - together with an unpacked (``mllib``) plugin. (`#11357 - <https://github.com/coq/coq/pull/11357>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/08-tools/11394-fix-coqdoc-annotations.rst b/doc/changelog/08-tools/11394-fix-coqdoc-annotations.rst deleted file mode 100644 index 10952c6b2c..0000000000 --- a/doc/changelog/08-tools/11394-fix-coqdoc-annotations.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** - ``coqdoc`` with option ``-g`` (Gallina only) now correctly prints - commands with attributes (`#11394 <https://github.com/coq/coq/pull/11394>`_, - fixes `#11353 <https://github.com/coq/coq/issues/11353>`_, - by Karl Palmskog). diff --git a/doc/changelog/08-tools/11523-coqdep+refactor2.rst b/doc/changelog/08-tools/11523-coqdep+refactor2.rst new file mode 100644 index 0000000000..32a4750b73 --- /dev/null +++ b/doc/changelog/08-tools/11523-coqdep+refactor2.rst @@ -0,0 +1,10 @@ +- **Changed:** + Internal options and behavior of ``coqdep`` have changed. ``coqdep`` + no longer works as a replacement for ``ocamldep``, thus ``.ml`` + files are not supported as input. Also, several deprecated options + have been removed: ``-w``, ``-D``, ``-mldep``, ``-prefix``, + ``-slash``, and ``-dumpbox``. Passing ``-boot`` to ``coqdep`` will + not load any path by default now, ``-R/-Q`` should be used instead. + (`#11523 <https://github.com/coq/coq/pull/11523>`_ and + `#11589 <https://github.com/coq/coq/pull/11589>`_, + by Emilio Jesus Gallego Arias). diff --git a/doc/changelog/09-coqide/11400-gtk-ide-completion.rst b/doc/changelog/09-coqide/11400-gtk-ide-completion.rst deleted file mode 100644 index 2dc3992b9c..0000000000 --- a/doc/changelog/09-coqide/11400-gtk-ide-completion.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Changed:** - CoqIDE now uses the GtkSourceView native implementation of - the autocomplete mechanism. - (`#11400 <https://github.com/coq/coq/pull/11400>`_, - by Pierre-Marie Pédrot). diff --git a/doc/changelog/09-coqide/11414-remove-ide-tactic-menu.rst b/doc/changelog/09-coqide/11414-remove-ide-tactic-menu.rst new file mode 100644 index 0000000000..6294cdb24a --- /dev/null +++ b/doc/changelog/09-coqide/11414-remove-ide-tactic-menu.rst @@ -0,0 +1,4 @@ +- **Removed:** + Removed the "Tactic" menu from CoqIDE which had been unmaintained for a number of years + (`#11414 <https://github.com/coq/coq/pull/11414>`_, + by Pierre-Marie Pédrot). diff --git a/doc/changelog/09-coqide/11415-remove-ide-revert-all-buffers.rst b/doc/changelog/09-coqide/11415-remove-ide-revert-all-buffers.rst new file mode 100644 index 0000000000..cb92945b8b --- /dev/null +++ b/doc/changelog/09-coqide/11415-remove-ide-revert-all-buffers.rst @@ -0,0 +1,4 @@ +- **Removed:** + Removed the "Revert all buffers" command from CoqIDE which had been broken for a long time + (`#11415 <https://github.com/coq/coq/pull/11415>`_, + by Pierre-Marie Pédrot). diff --git a/doc/changelog/10-standard-library/11350-list.rst b/doc/changelog/10-standard-library/11350-list.rst new file mode 100644 index 0000000000..52c2517161 --- /dev/null +++ b/doc/changelog/10-standard-library/11350-list.rst @@ -0,0 +1,5 @@ +- **Added:** + ``remove'`` and ``count_occ'`` over lists, + alternatives to ``remove`` and ``count_occ`` based on ``filter`` + (`#11350 <https://github.com/coq/coq/pull/11350>`_, + by Yishuai Li). diff --git a/doc/changelog/10-standard-library/11396-issue_11396_Rlist.rst b/doc/changelog/10-standard-library/11396-issue_11396_Rlist.rst deleted file mode 100644 index 3e1f1e02a4..0000000000 --- a/doc/changelog/10-standard-library/11396-issue_11396_Rlist.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Removed:** - Export of module ``RList`` in ``Ranalysis.v`` and ``Ranalysis_reg.v``. Module ``RList`` is still there but must be imported explicitly where required. - (`#11396 <https://github.com/coq/coq/pull/11396>`_, - by Michael Soegtrop). diff --git a/doc/changelog/10-standard-library/11404-removeRList.rst b/doc/changelog/10-standard-library/11404-removeRList.rst new file mode 100644 index 0000000000..88e22d128c --- /dev/null +++ b/doc/changelog/10-standard-library/11404-removeRList.rst @@ -0,0 +1,15 @@ +- **Removed:** + Type `RList` has been removed. All uses have been replaced by `list R`. + Functions from `RList` named `In`, `Rlength`, `cons_Rlist`, `app_Rlist` + have also been removed as they are essentially the same as `In`, `length`, + `app`, and `map` from `List`, modulo the following changes: + + - `RList.In x (RList.cons a l)` used to be convertible to + `(x = a) \\/ RList.In x l`, + but `List.In x (a :: l)` is convertible to + `(a = x) \\/ List.In l`. + The equality is reversed. + - `app_Rlist` and `List.map` take arguments in different order. + + (`#11404 <https://github.com/coq/coq/pull/11404>`_, + by Yves Bertot). diff --git a/doc/changelog/11-infrastructure-and-dependencies/11227-date.rst b/doc/changelog/11-infrastructure-and-dependencies/11227-date.rst deleted file mode 100644 index 5c08e2b0ea..0000000000 --- a/doc/changelog/11-infrastructure-and-dependencies/11227-date.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - Build date can now be overriden by setting the `SOURCE_DATE_EPOCH` - environment variable - (`#11227 <https://github.com/coq/coq/pull/11227>`_, - by Bernhard M. Wiedemann). diff --git a/doc/changelog/12-misc/11329-master+fix11114-extraction-anomaly-implicit-record.rst b/doc/changelog/12-misc/11329-master+fix11114-extraction-anomaly-implicit-record.rst new file mode 100644 index 0000000000..0a686dd87d --- /dev/null +++ b/doc/changelog/12-misc/11329-master+fix11114-extraction-anomaly-implicit-record.rst @@ -0,0 +1,4 @@ +- **Fixed:** + :cmd:`Extraction Implicit` on the constructor of a record was leading to an anomaly + (`#11329 <https://github.com/coq/coq/pull/11329>`_, + by Hugo Herbelin, fixes `#11114 <https://github.com/coq/coq/pull/11114>`_). diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index cc19c8b6a9..f706633da9 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -35,6 +35,17 @@ tactics for solving arithmetic goals over :math:`\mathbb{Q}`, use the Simplex method for solving linear goals. If it is not set, the decision procedures are using Fourier elimination. +.. opt:: Dump Arith + + This option (unset by default) may be set to a file path where + debug info will be written. + +.. cmd:: Show Lia Profile + + This command prints some statistics about the amount of pivoting + operations needed by :tacn:`lia` and may be useful to detect + inefficiencies (only meaningful if flag :flag:`Simplex` is set). + .. flag:: Lia Cache This flag (set by default) instructs :tacn:`lia` to cache its results in the file `.lia.cache` diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 21000889d3..6d9979a704 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -55,23 +55,23 @@ this version of Coq, it should soon be the case and we already recommend users to switch to :tacn:`lia` in new proof scripts (see also the warning message in the :ref:`corresponding chapter <omega>`). -The ``dev/doc/critical-bugs`` file documents the known critical bugs of |Coq| -and affected releases. See the `Changes in 8.11+beta1`_ section for the -detailed list of changes, including potentially breaking changes marked with -**Changed**. +The ``dev/doc/critical-bugs`` file documents the known critical bugs +of |Coq| and affected releases. See the `Changes in 8.11+beta1`_ +section and following sections for the detailed list of changes, +including potentially breaking changes marked with **Changed**. + +Coq's documentation is available at https://coq.github.io/doc/v8.11/api (documentation of +the ML API), https://coq.github.io/doc/v8.11/refman (reference +manual), and https://coq.github.io/doc/v8.11/stdlib (documentation of +the standard library). Maxime Dénès, Emilio Jesús Gallego Arias, Gaëtan Gilbert, Michael -Soegtrop, Théo Zimmermann worked on maintaining and improving the +Soegtrop and Théo Zimmermann worked on maintaining and improving the continuous integration system and package building infrastructure. -Coq's documentation is available at https://coq.github.io/doc/V8.11+beta1/api (documentation of -the ML API), https://coq.github.io/doc/V8.11+beta1/refman (reference -manual), and https://coq.github.io/doc/V8.11+beta1/stdlib (documentation of -the standard library). - The OPAM repository for |Coq| packages has been maintained by -Karl Palmskog, Matthieu Sozeau, Enrico Tassi with contributions -from many users. A list of packages is available at +Guillaume Claret, Karl Palmskog, Matthieu Sozeau and Enrico Tassi with +contributions from many users. A list of packages is available at https://coq.inria.fr/opam/www/. The 61 contributors to this version are Michael D. Adams, Guillaume @@ -514,6 +514,133 @@ Changes in 8.11+beta1 (`#10471 <https://github.com/coq/coq/pull/10471>`_, by Emilio Jesús Gallego Arias). +Changes in 8.11.0 +~~~~~~~~~~~~~~~~~ + +**Kernel** + +- **Changed:** the native compilation (:tacn:`native_compute`) now + creates a directory to contain temporary files instead of putting + them in the root of the system temporary directory (`#11081 + <https://github.com/coq/coq/pull/11081>`_, by Gaëtan Gilbert). +- **Fixed:** `#11360 <https://github.com/issues/11360>`_. + Broken section closing when a template polymorphic inductive type depends on + a section variable through its parameters (`#11361 + <https://github.com/coq/coq/pull/11361>`_, by Gaëtan Gilbert). +- **Fixed:** The type of :g:`Set+1` would be computed to be itself, + leading to a proof of False (`#11422 + <https://github.com/coq/coq/pull/11422>`_, by Gaëtan Gilbert). + +**Specification language, type inference** + +- **Changed:** Heuristics for universe minimization to :g:`Set`: only + minimize flexible universes (`#10657 <https://github.com/coq/coq/pull/10657>`_, + by Gaëtan Gilbert with help from Maxime Dénès and Matthieu Sozeau). +- **Fixed:** + A dependency was missing when looking for default clauses in the + algorithm for printing pattern matching clauses (`#11233 + <https://github.com/coq/coq/pull/11233>`_, by Hugo Herbelin, fixing + `#11231 <https://github.com/coq/coq/pull/11231>`_, reported by Barry + Jay). + +**Notations** + +- **Fixed:** + :cmd:`Print Visibility` was failing in the presence of only-printing notations + (`#11276 <https://github.com/coq/coq/pull/11276>`_, + by Hugo Herbelin, fixing `#10750 <https://github.com/coq/coq/pull/10750>`_). +- **Fixed:** + Recursive notations with custom entries were incorrectly parsing `constr` + instead of custom grammars (`#11311 <https://github.com/coq/coq/pull/11311>`_ + by Maxime Dénès, fixes `#9532 <https://github.com/coq/coq/pull/9532>`_, + `#9490 <https://github.com/coq/coq/pull/9490>`_). + +**Tactics** + +- **Changed:** + The tactics :tacn:`eapply`, :tacn:`refine` and variants no + longer allow shelved goals to be solved by typeclass resolution + (`#10762 <https://github.com/coq/coq/pull/10762>`_, by Matthieu Sozeau). +- **Fixed:** The optional string argument to :tacn:`time` is now + properly quoted under :cmd:`Print Ltac` (`#11203 + <https://github.com/coq/coq/pull/11203>`_, fixes `#10971 + <https://github.com/coq/coq/issues/10971>`_, by Jason Gross) +- **Fixed:** + Efficiency regression of :tacn:`lia` introduced in 8.10 + by PR `#9725 <https://github.com/coq/coq/pull/9725>`_ + (`#11263 <https://github.com/coq/coq/pull/11263>`_, + fixes `#11063 <https://github.com/coq/coq/issues/11063>`_, + and `#11242 <https://github.com/coq/coq/issues/11242>`_, + and `#11270 <https://github.com/coq/coq/issues/11270>`_, by Frédéric Besson). +- **Deprecated:** + The undocumented ``omega with`` tactic variant has been deprecated. + Using :tacn:`lia` is the recommended replacement, though the old semantics + of ``omega with *`` can be recovered with ``zify; omega`` + (`#11337 <https://github.com/coq/coq/pull/11337>`_, + by Emilio Jesus Gallego Arias). +- **Fixed** + For compatibility reasons, in 8.11, :tacn:`zify` does not support :g:`Z.pow_pos` by default. + It can be enabled by explicitly loading the module :g:`ZifyPow` + (`#11430 <https://github.com/coq/coq/pull/11430>`_ by Frédéric Besson + fixes `#11191 <https://github.com/coq/coq/issues/11191>`_). + +**Tactic language** + +- **Fixed:** + Syntax of tactic `cofix ... with ...` was broken since Coq 8.10 + (`#11241 <https://github.com/coq/coq/pull/11241>`_, + by Hugo Herbelin). + +**Commands and options** + +- **Deprecated:** The `-load-ml-source` and `-load-ml-object` command + line options have been deprecated; their use was very limited, you + can achieve the same by adding object files in the linking step or + by using a plugin (`#11428 + <https://github.com/coq/coq/pull/11428>`_, by Emilio Jesus Gallego + Arias). + +**Tools** + +- **Fixed:** + ``coqtop --version`` was broken when called in the middle of an installation process + (`#11255 <https://github.com/coq/coq/pull/11255>`_, by Hugo Herbelin, fixing + `#11254 <https://github.com/coq/coq/pull/11254>`_). +- **Deprecated:** The ``-quick`` command is renamed to ``-vio``, for + consistency with the new ``-vos`` and ``-vok`` flags. Usage of + ``-quick`` is now deprecated (`#11280 + <https://github.com/coq/coq/pull/11280>`_, by Arthur Charguéraud). +- **Fixed:** + ``coq_makefile`` does not break when using the ``CAMLPKGS`` variable + together with an unpacked (``mllib``) plugin (`#11357 + <https://github.com/coq/coq/pull/11357>`_, by Gaëtan Gilbert). +- **Fixed:** + ``coqdoc`` with option ``-g`` (Gallina only) now correctly prints + commands with attributes (`#11394 <https://github.com/coq/coq/pull/11394>`_, + fixes `#11353 <https://github.com/coq/coq/issues/11353>`_, + by Karl Palmskog). + +**CoqIDE** + +- **Changed:** CoqIDE now uses the GtkSourceView native implementation + of the autocomplete mechanism (`#11400 + <https://github.com/coq/coq/pull/11400>`_, by Pierre-Marie Pédrot). + +**Standard library** + +- **Removed:** Export of module :g:`RList` in :g:`Ranalysis` and + :g:`Ranalysis_reg`. Module :g:`RList` is still there but must be + imported explicitly where required (`#11396 + <https://github.com/coq/coq/pull/11396>`_, by Michael Soegtrop). + +**Infrastructure and dependencies** + +- **Added:** + Build date can now be overridden by setting the `SOURCE_DATE_EPOCH` + environment variable + (`#11227 <https://github.com/coq/coq/pull/11227>`_, + by Bernhard M. Wiedemann). + Version 8.10 ------------ diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index f1dd7479c5..77cb3ecc21 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -108,7 +108,7 @@ master_doc = "index" # General information about the project. project = 'Coq' -copyright = '1999-2019, Inria, CNRS and contributors' +copyright = '1999-2020, Inria, CNRS and contributors' author = 'The Coq Development Team' # The version info for the project you're documenting, acts as replacement for diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 510e271951..9686500a35 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1570,11 +1570,26 @@ inserted. In the second case, the function is considered to be implicitly applied to the implicit arguments it is waiting for: one says that the implicit argument is maximally inserted. -Each implicit argument can be declared to have to be inserted maximally or non -maximally. This can be governed argument per argument by the command -:cmd:`Arguments (implicits)` or globally by the :flag:`Maximal Implicit Insertion` flag. +Each implicit argument can be declared to be inserted maximally or non +maximally. In Coq, maximally-inserted implicit arguments are written between curly braces +"{ }" and non-maximally-inserted implicit arguments are written in square brackets "[ ]". -.. seealso:: :ref:`displaying-implicit-args`. +.. seealso:: :flag:`Maximal Implicit Insertion` + +Trailing Implicit Arguments ++++++++++++++++++++++++++++ + +An implicit argument is considered trailing when all following arguments are declared +implicit. Trailing implicit arguments cannot be declared non maximally inserted, +otherwise they would never be inserted. + +.. exn:: Argument @name is a trailing implicit, so it can't be declared non maximal. Please use %{ %} instead of [ ]. + + For instance: + + .. coqtop:: all fail + + Fail Definition double [n] := n + n. Casual use of implicit arguments @@ -1608,7 +1623,7 @@ Implicit Argument Binders In the first setting, one wants to explicitly give the implicit arguments of a declared object as part of its definition. To do this, one has to surround the bindings of implicit arguments by curly -braces: +braces or square braces: .. coqtop:: all @@ -1624,6 +1639,17 @@ absent in every situation but still be able to specify it if needed: Goal forall A, compose id id = id (A:=A). +For non maximally inserted implicit arguments, use square brackets: + +.. coqtop:: all + + Fixpoint map [A B : Type] (f : A -> B) (l : list A) : list B := + match l with + | nil => nil + | cons a t => cons (f a) (map f t) + end. + + Print Implicit map. The syntax is supported in all top-level definitions: :cmd:`Definition`, :cmd:`Fixpoint`, :cmd:`Lemma` and so on. For (co-)inductive datatype @@ -1643,17 +1669,55 @@ For example: One can always specify the parameter if it is not uniform using the usual implicit arguments disambiguation syntax. +The syntax is also supported in internal binders. For instance, in the +following kinds of expressions, the type of each declaration present +in :token:`binders` can be bracketed to mark the declaration as +implicit: +:n:`fun (@ident:forall @binders, @type) => @term`, +:n:`forall (@ident:forall @binders, @type), @type`, +:n:`let @ident @binders := @term in @term`, +:n:`fix @ident @binders := @term in @term` and +:n:`cofix @ident @binders := @term in @term`. +Here is an example: + +.. coqtop:: all + + Axiom Ax : + forall (f:forall {A} (a:A), A * A), + let g {A} (x y:A) := (x,y) in + f 0 = g 0 0. + +.. warn:: Ignoring implicit binder declaration in unexpected position + + This is triggered when setting an argument implicit in an + expression which does not correspond to the type of an assumption + or to the body of a definition. Here is an example: + + .. coqtop:: all warn + + Definition f := forall {y}, y = 0. + +.. warn:: Making shadowed name of implicit argument accessible by position + + This is triggered when two variables of same name are set implicit + in the same block of binders, in which case the first occurrence is + considered to be unnamed. Here is an example: + + .. coqtop:: all warn + + Check let g {x:nat} (H:x=x) {x} (H:x=x) := x in 0. + Declaring Implicit Arguments ++++++++++++++++++++++++++++ -.. cmd:: Arguments @qualid {* {| [ @ident ] | { @ident } | @ident } } +.. cmd:: Arguments @qualid {* {| [ @name ] | { @name } | @name } } :name: Arguments (implicits) This command is used to set implicit arguments *a posteriori*, - where the list of possibly bracketed :token:`ident` is a prefix of the list of + where the list of possibly bracketed :token:`name` is a prefix of the list of arguments of :token:`qualid` where the ones to be declared implicit are surrounded by square brackets and the ones to be declared as maximally inserted implicits are surrounded by curly braces. @@ -1667,20 +1731,20 @@ Declaring Implicit Arguments This command clears implicit arguments. -.. cmdv:: Global Arguments @qualid {* {| [ @ident ] | { @ident } | @ident } } +.. cmdv:: Global Arguments @qualid {* {| [ @name ] | { @name } | @name } } This command is used to recompute the implicit arguments of :token:`qualid` after ending of the current section if any, enforcing the implicit arguments known from inside the section to be the ones declared by the command. -.. cmdv:: Local Arguments @qualid {* {| [ @ident ] | { @ident } | @ident } } +.. cmdv:: Local Arguments @qualid {* {| [ @name ] | { @name } | @name } } When in a module, tell not to activate the implicit arguments of :token:`qualid` declared by this command to contexts that require the module. -.. cmdv:: {? {| Global | Local } } Arguments @qualid {*, {+ {| [ @ident ] | { @ident } | @ident } } } +.. cmdv:: {? {| Global | Local } } Arguments @qualid {*, {+ {| [ @name ] | { @name } | @name } } } For names of constants, inductive types, constructors, lemmas which can only be applied to a fixed number of @@ -1728,14 +1792,6 @@ Declaring Implicit Arguments To know which are the implicit arguments of an object, use the command :cmd:`Print Implicit` (see :ref:`displaying-implicit-args`). -.. exn:: Argument @ident is a trailing implicit, so it can't be declared non maximal. Please use %{ %} instead of [ ]. - - For instance in - - .. coqtop:: all fail - - Arguments prod _ [_]. - Automatic declaration of implicit arguments ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1811,7 +1867,7 @@ appear strictly in the body of the type, they are implicit. Mode for automatic declaration of implicit arguments -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +++++++++++++++++++++++++++++++++++++++++++++++++++++ .. flag:: Implicit Arguments @@ -1823,7 +1879,7 @@ Mode for automatic declaration of implicit arguments .. _controlling-strict-implicit-args: Controlling strict implicit arguments -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ++++++++++++++++++++++++++++++++++++++ .. flag:: Strict Implicit @@ -1842,7 +1898,7 @@ Controlling strict implicit arguments .. _controlling-contextual-implicit-args: Controlling contextual implicit arguments -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ++++++++++++++++++++++++++++++++++++++++++ .. flag:: Contextual Implicit @@ -1853,7 +1909,7 @@ Controlling contextual implicit arguments .. _controlling-rev-pattern-implicit-args: Controlling reversible-pattern implicit arguments -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ++++++++++++++++++++++++++++++++++++++++++++++++++ .. flag:: Reversible Pattern Implicit @@ -1864,7 +1920,7 @@ Controlling reversible-pattern implicit arguments .. _controlling-insertion-implicit-args: Controlling the insertion of implicit arguments not followed by explicit arguments -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ .. flag:: Maximal Implicit Insertion @@ -1873,6 +1929,28 @@ Controlling the insertion of implicit arguments not followed by explicit argumen function is partially applied and the next argument of the function is an implicit one. +Combining manual declaration and automatic declaration +++++++++++++++++++++++++++++++++++++++++++++++++++++++ + +When some arguments are manually specified implicit with binders in a definition +and the automatic declaration mode in on, the manual implicit arguments are added to the +automatically declared ones. + +In that case, and when the flag :flag:`Maximal Implicit Insertion` is set to off, +some trailing implicit arguments can be inferred to be non maximally inserted. In +this case, they are converted to maximally inserted ones. + +.. example:: + + .. coqtop:: all + + Set Implicit Arguments. + Axiom eq0_le0 : forall (n : nat) (x : n = 0), n <= 0. + Print Implicit eq0_le0. + Axiom eq0_le0' : forall (n : nat) {x : n = 0}, n <= 0. + Print Implicit eq0_le0'. + + .. _explicit-applications: Explicit applications @@ -2130,14 +2208,23 @@ or :g:`m` to the type :g:`nat` of natural numbers). Adds blocks of implicit types with different specifications. +.. flag:: Printing Use Implicit Types + + By default, the type of bound variables is not printed when + the variable name is associated to an implicit type which matches the + actual type of the variable. This feature can be deactivated by + turning this flag off. + .. _implicit-generalization: Implicit generalization ~~~~~~~~~~~~~~~~~~~~~~~ .. index:: `{ } +.. index:: `[ ] .. index:: `( ) .. index:: `{! } +.. index:: `[! ] .. index:: `(! ) Implicit generalization is an automatic elaboration of a statement @@ -2145,11 +2232,12 @@ with free variables into a closed statement where these variables are quantified explicitly. It is activated for a binder by prefixing a \`, and for terms by -surrounding it with \`{ } or \`( ). +surrounding it with \`{ }, or \`[ ] or \`( ). Terms surrounded by \`{ } introduce their free variables as maximally -inserted implicit arguments, and terms surrounded by \`( ) introduce -them as explicit arguments. +inserted implicit arguments, terms surrounded by \`[ ] introduce them as +non maximally inserted implicit arguments and terms surrounded by \`( ) +introduce them as explicit arguments. Generalizing binders always introduce their free variables as maximally inserted implicit arguments. The binder itself introduces diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index d591718b17..7ce4538a4d 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -283,8 +283,10 @@ Binders | ( {+ @name } : @term ) | ( @name {? : @term } := @term ) | %{ {+ @name } {? : @term } %} + | [ {+ @name } {? : @term } ] | `( {+, @typeclass_constraint } ) | `%{ {+, @typeclass_constraint } %} + | `[ {+, @typeclass_constraint } ] | ' @pattern0 | ( @name : @term %| @term ) typeclass_constraint ::= {? ! } @term @@ -1061,6 +1063,18 @@ Parameterized inductive types | cons3 : A -> list3 -> list3. End list3. + For finer control, you can use a ``|`` between the uniform and + the non-uniform parameters: + + .. coqtop:: in reset + + Inductive Acc {A:Type} (R:A->A->Prop) | (x:A) : Prop + := Acc_in : (forall y, R y x -> Acc y) -> Acc x. + + The flag can then be seen as deciding whether the ``|`` is at the + beginning (when the flag is unset) or at the end (when it is set) + of the parameters when not explicitly given. + .. seealso:: Section :ref:`inductive-definitions` and the :tacn:`induction` tactic. diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index ba43128bdc..98d222e317 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -157,8 +157,6 @@ and ``coqtop``, unless stated otherwise: loading the default resource file from the standard configuration directories. :-q: Do not to load the default resource file. -:-load-ml-source *file*: Load the OCaml source file *file*. -:-load-ml-object *file*: Load the OCaml object file *file*. :-l *file*, -load-vernac-source *file*: Load and execute the |Coq| script from *file.v*. :-lv *file*, -load-vernac-source-verbose *file*: Load and execute the diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index e5edd08995..179dff9959 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -255,14 +255,20 @@ file timing data: one, you can pass them via the variable ``TGTS``, e.g., ``make pretty-timed TGTS="a.vo b.vo"``. - .. :: + .. note:: This target requires ``python`` to build the table. .. note:: This target will *append* to the timing log; if you want a - fresh start, you must remove the ``filetime-of-build.log`` or + fresh start, you must remove the file ``time-of-build.log`` or ``run make cleanall``. + .. note:: + By default the table displays user times. If the build log + contains real times (which it does by default), passing + ``TIMING_REAL=1`` to ``make pretty-timed`` will use real times + rather than user times in the table. + .. example:: For example, the output of ``make pretty-timed`` may look like this: @@ -310,6 +316,15 @@ file timing data: (which are frequently noise); lexicographic sorting forces an order on files which take effectively no time to compile. + If you prefer a different sorting order, you can pass + ``TIMING_SORT_BY=absolute`` to sort by the total time taken, or + ``TIMING_SORT_BY=diff`` to sort by the signed difference in + time. + + .. note:: + Just like ``pretty-timed``, this table defaults to using user + times. Pass ``TIMING_REAL=1`` to ``make`` on the command line to show real times instead. + .. example:: For example, the output table from @@ -349,7 +364,7 @@ line timing data: :: - print-pretty-single-time-diff BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing + print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing this target will make a sorted table of the per-line timing differences between the timing logs in the ``BEFORE`` and ``AFTER`` files, display it, and @@ -364,6 +379,28 @@ line timing data: .. note:: This target requires python to build the table. + .. note:: + This target follows the same sorting order as the + ``print-pretty-timed-diff`` target, and supports the same + options for the ``TIMING_SORT_BY`` variable. + + .. note:: + By default, two lines are only considered the same if the + character offsets and initial code strings are identical. Passing + ``TIMING_FUZZ=N`` relaxes this constraint by allowing the + character locations to differ by up to ``N``, as long + as the total number of characters and initial code strings + continue to match. This is useful when there are small changes + to a file, and you want to match later lines that have not + changed even though the character offsets have changed. + + .. note:: + By default the table picks up real times, under the assumption + that when comparing line-by-line, the real time is a more + accurate representation as it includes disk time and time spent + in the native compiler. Passing ``TIMING_REAL=0`` to ``make`` + will use user times rather than real times in the table. + .. example:: For example, running ``print-pretty-single-time-diff`` might give a table like this: @@ -545,7 +582,7 @@ Computing Module dependencies In order to compute module dependencies (to be used by ``make`` or ``dune``), |Coq| provides the ``coqdep`` tool. -``coqdep`` computes inter-module dependencies for |Coq| and |OCaml| +``coqdep`` computes inter-module dependencies for |Coq| programs, and prints the dependencies on the standard output in a format readable by make. When a directory is given as argument, it is recursively looked at. @@ -554,11 +591,6 @@ Dependencies of |Coq| modules are computed by looking at ``Require`` commands (``Require``, ``Require Export``, ``Require Import``), but also at the command ``Declare ML Module``. -Dependencies of |OCaml| modules are computed by looking at -`open` commands and the dot notation *module.value*. However, this is -done approximately and you are advised to use ``ocamldep`` instead for the -|OCaml| module dependencies. - See the man page of ``coqdep`` for more details and options. Both Dune and ``coq_makefile`` use ``coqdep`` to compute the diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index b722b1af74..9362a7729e 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -3,10 +3,6 @@ Ltac2 ===== -.. coqtop:: none - - From Ltac2 Require Import Ltac2. - The Ltac tactic language is probably one of the ingredients of the success of Coq, yet it is at the same time its Achilles' heel. Indeed, Ltac: @@ -88,6 +84,12 @@ which allows to ensure that Ltac2 satisfies the same equations as a generic ML with unspecified effects would do, e.g. function reduction is substitution by a value. +To import Ltac2, use the following command: + +.. coqtop:: in + + From Ltac2 Require Import Ltac2. + Type Syntax ~~~~~~~~~~~ diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 853ddfd6dc..46215f16a6 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -2222,14 +2222,14 @@ tactics to *permute* the subgoals generated by a tactic. If :token:`num`\'s value is :math:`k`, this tactic rotates the :math:`n` subgoals :math:`G_1` , …, :math:`G_n` - in focus. The first subgoal becomes :math:`G_{n + 1 − k}` and the + in focus. Subgoal :math:`G_{n + 1 − k}` becomes the first, and the circular order of subgoals remains unchanged. .. tacn:: first @num last If :token:`num`\'s value is :math:`k`, this tactic rotates the :math:`n` subgoals :math:`G_1` , …, :math:`G_n` - in focus. The first subgoal becomes :math:`G_k` and the circular order + in focus. Subgoal :math:`G_{k + 1 \bmod n}` becomes the first, and the circular order of subgoals remains unchanged. Finally, the tactics ``last`` and ``first`` combine with the branching syntax diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 53cfb973d4..2fa4f1fa42 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -275,7 +275,7 @@ These patterns can be used when the hypothesis is an equality: :n:`or` has multiple constructors (:n:`or_introl` and :n:`or_intror`), while :n:`and` has a single constructor (:n:`conj`) with multiple parameters (:n:`A` and :n:`B`). - These are defined in theories/Init/Logic.v. The "where" clauses define the + These are defined in ``theories/Init/Logic.v``. The "where" clauses define the infix notation for "or" and "and". .. coqdoc:: @@ -3113,6 +3113,12 @@ the conversion in hypotheses :n:`{+ @ident}`. compilation cost is higher, so it is worth using only for intensive computations. + .. flag:: NativeCompute Timing + + This flag causes all calls to the native compiler to print + timing information for the compilation, execution, and + reification phases of native compilation. + .. flag:: NativeCompute Profiling On Linux, if you have the ``perf`` profiler installed, this flag makes diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index dbe714c388..8bfcab0f4e 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -163,6 +163,10 @@ Grammar constr` is at level 100. To avoid ``x : A`` being parsed as a type cast, it is necessary to put ``x`` at a level below 100, typically 99. Hence, a correct definition is the following: +.. coqtop:: none + + Reset Initial. + .. coqtop:: all Notation "{ x : A | P }" := (sig A (fun x => P)) (x at level 99). @@ -350,6 +354,11 @@ Reserving notations This command declares an infix parsing rule without giving its interpretation. + When a format is attached to a reserved notation, it is used by + default by all subsequent interpretations of the corresponding + notation. A specific interpretation can provide its own format + overriding the default format though. + Simultaneous definition of terms and notations ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -408,6 +417,27 @@ identifiers or tokens starting with a single quote are dropped. Locate "exists". Locate "exists _ .. _ , _". +Inheritance of the properties of arguments of constants bound to a notation +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +If the right-hand side of a notation is a partially applied constant, +the notation inherits the implicit arguments (see +:ref:`ImplicitArguments`) and interpretation scopes (see +:ref:`Scopes`) of the constant. For instance: + +.. coqtop:: in reset + + Record R := {dom : Type; op : forall {A}, A -> dom}. + Notation "# x" := (@op x) (at level 8). + +.. coqtop:: all + + Check fun x:R => # x 3. + +As an exception, if the right-hand side is just of the form +:n:`@@qualid`, this conventionally stops the inheritance of implicit +arguments (but not of interpretation scopes). + Notations and binders ~~~~~~~~~~~~~~~~~~~~~ @@ -798,7 +828,13 @@ associated to the custom entry ``expr``. The level can be omitted, as in Notation "[ e ]" := e (e custom expr). -in which case Coq tries to infer it. +in which case Coq infer it. If the sub-expression is at a border of +the notation (as e.g. ``x`` and ``y`` in ``x + y``), the level is +determined by the associativity. If the sub-expression is not at the +border of the notation (as e.g. ``e`` in ``"[ e ]``), the level is +inferred to be the highest level used for the entry. In particular, +this level depends on the highest level existing in the entry at the +time of use of the notation. In the absence of an explicit entry for parsing or printing a sub-expression of a notation in a custom entry, the default is to @@ -1400,6 +1436,12 @@ Abbreviations denoted expression is performed at definition time. Type checking is done only at the time of use of the abbreviation. + Like for notations, if the right-hand side of an abbreviation is a + partially applied constant, the abbreviation inherits the implicit + arguments and interpretation scopes of the constant. As an + exception, if the right-hand side is just of the form :n:`@@qualid`, + this conventionally stops the inheritance of implicit arguments. + .. _numeral-notations: Numeral notations diff --git a/doc/stdlib/dune b/doc/stdlib/dune index 828caecabc..093c7a62b2 100644 --- a/doc/stdlib/dune +++ b/doc/stdlib/dune @@ -5,7 +5,6 @@ (deps make-library-index index-list.html.template hidden-files (source_tree %{project_root}/theories) - (source_tree %{project_root}/plugins) (source_tree %{project_root}/user-contrib)) (action (chdir %{project_root} @@ -17,7 +16,6 @@ (deps ; This will be replaced soon by `theories/**/*.v` soon, thanks to rgrinberg (source_tree %{project_root}/theories) - (source_tree %{project_root}/plugins) (source_tree %{project_root}/user-contrib) (:header %{project_root}/doc/common/styles/html/coqremote/header.html) (:footer %{project_root}/doc/common/styles/html/coqremote/footer.html) @@ -26,7 +24,7 @@ (action (progn (run mkdir -p html) - (bash "%{bin:coqdoc} -q -d html --with-header %{header} --with-footer %{footer} --multi-index --html -g -R %{project_root}/theories Coq -R %{project_root}/plugins Coq -Q %{project_root}/user-contrib/Ltac2 Ltac2 $(find %{project_root}/theories %{project_root}/plugins %{project_root}/user-contrib -name *.v)") + (bash "%{bin:coqdoc} -q -d html --with-header %{header} --with-footer %{footer} --multi-index --html -g -R %{project_root}/theories Coq -Q %{project_root}/user-contrib/Ltac2 Ltac2 $(find %{project_root}/theories %{project_root}/user-contrib -name *.v)") (run mv html/index.html html/genindex.html) (with-stdout-to _index.html diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files index dbc3a42ee9..60d6039b0f 100644 --- a/doc/stdlib/hidden-files +++ b/doc/stdlib/hidden-files @@ -1,90 +1,90 @@ -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/ExtrOcamlChar.v -plugins/extraction/ExtrOCamlInt63.v -plugins/extraction/ExtrOCamlFloats.v -plugins/extraction/ExtrOcamlIntConv.v -plugins/extraction/ExtrOcamlNatBigInt.v -plugins/extraction/ExtrOcamlNatInt.v -plugins/extraction/ExtrOcamlString.v -plugins/extraction/ExtrOcamlNativeString.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/Ztac.v -plugins/micromega/DeclConstant.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/micromega/ZifyInst.v -plugins/micromega/ZifyBool.v -plugins/micromega/ZifyComparison.v -plugins/micromega/ZifyClasses.v -plugins/micromega/Zify.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 -plugins/ssr/ssrunder.v -plugins/ssr/ssrsetoid.v +theories/btauto/Algebra.v +theories/btauto/Btauto.v +theories/btauto/Reflect.v +theories/derive/Derive.v +theories/extraction/ExtrHaskellBasic.v +theories/extraction/ExtrHaskellNatInt.v +theories/extraction/ExtrHaskellNatInteger.v +theories/extraction/ExtrHaskellNatNum.v +theories/extraction/ExtrHaskellString.v +theories/extraction/ExtrHaskellZInt.v +theories/extraction/ExtrHaskellZInteger.v +theories/extraction/ExtrHaskellZNum.v +theories/extraction/ExtrOcamlBasic.v +theories/extraction/ExtrOcamlBigIntConv.v +theories/extraction/ExtrOcamlChar.v +theories/extraction/ExtrOCamlInt63.v +theories/extraction/ExtrOCamlFloats.v +theories/extraction/ExtrOcamlIntConv.v +theories/extraction/ExtrOcamlNatBigInt.v +theories/extraction/ExtrOcamlNatInt.v +theories/extraction/ExtrOcamlString.v +theories/extraction/ExtrOcamlNativeString.v +theories/extraction/ExtrOcamlZBigInt.v +theories/extraction/ExtrOcamlZInt.v +theories/extraction/Extraction.v +theories/funind/FunInd.v +theories/funind/Recdef.v +theories/ltac/Ltac.v +theories/micromega/Ztac.v +theories/micromega/DeclConstant.v +theories/micromega/Env.v +theories/micromega/EnvRing.v +theories/micromega/Fourier.v +theories/micromega/Fourier_util.v +theories/micromega/Lia.v +theories/micromega/Lqa.v +theories/micromega/Lra.v +theories/micromega/MExtraction.v +theories/micromega/OrderedRing.v +theories/micromega/Psatz.v +theories/micromega/QMicromega.v +theories/micromega/RMicromega.v +theories/micromega/Refl.v +theories/micromega/RingMicromega.v +theories/micromega/Tauto.v +theories/micromega/VarMap.v +theories/micromega/ZCoeff.v +theories/micromega/ZMicromega.v +theories/micromega/ZifyInst.v +theories/micromega/ZifyBool.v +theories/micromega/ZifyComparison.v +theories/micromega/ZifyClasses.v +theories/micromega/Zify.v +theories/nsatz/Nsatz.v +theories/omega/Omega.v +theories/omega/OmegaLemmas.v +theories/omega/OmegaPlugin.v +theories/omega/OmegaTactic.v +theories/omega/PreOmega.v +theories/quote/Quote.v +theories/romega/ROmega.v +theories/romega/ReflOmegaCore.v +theories/rtauto/Bintree.v +theories/rtauto/Rtauto.v +theories/setoid_ring/Algebra_syntax.v +theories/setoid_ring/ArithRing.v +theories/setoid_ring/BinList.v +theories/setoid_ring/Cring.v +theories/setoid_ring/Field.v +theories/setoid_ring/Field_tac.v +theories/setoid_ring/Field_theory.v +theories/setoid_ring/InitialRing.v +theories/setoid_ring/Integral_domain.v +theories/setoid_ring/NArithRing.v +theories/setoid_ring/Ncring.v +theories/setoid_ring/Ncring_initial.v +theories/setoid_ring/Ncring_polynom.v +theories/setoid_ring/Ncring_tac.v +theories/setoid_ring/RealField.v +theories/setoid_ring/Ring.v +theories/setoid_ring/Ring_base.v +theories/setoid_ring/Ring_polynom.v +theories/setoid_ring/Ring_tac.v +theories/setoid_ring/Ring_theory.v +theories/setoid_ring/Rings_Q.v +theories/setoid_ring/Rings_R.v +theories/setoid_ring/Rings_Z.v +theories/setoid_ring/ZArithRing.v +theories/ssr/ssrunder.v +theories/ssr/ssrsetoid.v diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 5e13214a1a..51688e2d9e 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -619,11 +619,11 @@ through the <tt>Require Import</tt> command.</p> small scale reflection formalization technique </dt> <dd> - plugins/ssrmatching/ssrmatching.v - plugins/ssr/ssrclasses.v - plugins/ssr/ssreflect.v - plugins/ssr/ssrbool.v - plugins/ssr/ssrfun.v + theories/ssrmatching/ssrmatching.v + theories/ssr/ssrclasses.v + theories/ssr/ssreflect.v + theories/ssr/ssrbool.v + theories/ssr/ssrfun.v </dd> <dt> <b>Ltac2</b>: @@ -664,7 +664,6 @@ through the <tt>Require Import</tt> command.</p> </dt> <dd> theories/Compat/AdmitAxiom.v - theories/Compat/Coq89.v theories/Compat/Coq810.v theories/Compat/Coq811.v theories/Compat/Coq812.v diff --git a/doc/stdlib/make-library-index b/doc/stdlib/make-library-index index 732f15b78a..a51308f153 100755 --- a/doc/stdlib/make-library-index +++ b/doc/stdlib/make-library-index @@ -8,7 +8,7 @@ HIDDEN=$2 cp -f $FILE.template tmp echo -n "Building file index-list.prehtml... " -LIBDIRS=`find theories/* plugins/* user-contrib/* -type d ! -name .coq-native` +LIBDIRS=`find theories/* user-contrib/* -type d ! -name .coq-native` for k in $LIBDIRS; do if [[ $k =~ "user-contrib" ]]; then diff --git a/doc/tools/coqrst/checkdeps.py b/doc/tools/coqrst/checkdeps.py index 91f0a7cb1b..feafcba026 100644 --- a/doc/tools/coqrst/checkdeps.py +++ b/doc/tools/coqrst/checkdeps.py @@ -10,13 +10,20 @@ from __future__ import print_function import sys +missing_deps = [] + def eprint(*args, **kwargs): print(*args, file=sys.stderr, **kwargs) def missing_dep(dep): - eprint('Cannot find %s (needed to build documentation)' % dep) - eprint('You can run `pip3 install %s` to install it.' % dep) - sys.exit(1) + missing_deps.append(dep) + +def report_missing_deps(): + if len(missing_deps) > 0: + deps = " ".join(missing_deps) + eprint('Cannot find package(s) `%s` (needed to build documentation)' % deps) + eprint('You can run `pip3 install %s` to install it/them.' % deps) + sys.exit(1) try: import sphinx_rtd_theme @@ -37,3 +44,10 @@ try: import bs4 except: missing_dep('beautifulsoup4') + +try: + import sphinxcontrib.bibtex +except: + missing_dep('sphinxcontrib-bibtex') + +report_missing_deps() diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 1f9178f4b6..85d86bed62 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -270,7 +270,7 @@ class GallinaObject(PlainObject): :math:`p \ge c \rightarrow p \ge \lceil{c}\rceil`. """ subdomain = "thm" - index_suffix = "(thm)" + index_suffix = "(theorem)" annotation = "Theorem" class VernacObject(NotationObject): @@ -283,7 +283,7 @@ class VernacObject(NotationObject): This command is equivalent to :n:`…`. """ subdomain = "cmd" - index_suffix = "(cmd)" + index_suffix = "(command)" annotation = "Command" def _name_from_signature(self, signature): @@ -306,7 +306,7 @@ class VernacVariantObject(VernacObject): This is equivalent to :n:`Axiom @ident : @term`. """ - index_suffix = "(cmdv)" + index_suffix = "(command variant)" annotation = "Variant" def _name_from_signature(self, signature): @@ -322,7 +322,7 @@ class TacticNotationObject(NotationObject): :token:`expr` is evaluated to ``v`` which must be a tactic value. … """ subdomain = "tacn" - index_suffix = "(tacn)" + index_suffix = "(tactic)" annotation = None class TacticNotationVariantObject(TacticNotationObject): @@ -342,7 +342,7 @@ class TacticNotationVariantObject(TacticNotationObject): The number is the failure level. If no level is specified, it defaults to 0. … """ - index_suffix = "(tacnv)" + index_suffix = "(tactic variant)" annotation = "Variant" class OptionObject(NotationObject): @@ -357,7 +357,7 @@ class OptionObject(NotationObject): application of a tactic. """ subdomain = "opt" - index_suffix = "(opt)" + index_suffix = "(option)" annotation = "Option" def _name_from_signature(self, signature): @@ -534,7 +534,7 @@ class ExceptionObject(NotationObject): Raised if :n:`@tactic` does not fully solve the goal. """ subdomain = "exn" - index_suffix = "(err)" + index_suffix = "(error)" annotation = "Error" # Uses “exn” since “err” already is a CSS class added by “writer_aux”. @@ -557,7 +557,7 @@ class WarningObject(NotationObject): valid coercion paths are ignored. """ subdomain = "warn" - index_suffix = "(warn)" + index_suffix = "(warning)" annotation = "Warning" # Generate names automatically diff --git a/doc/tools/coqrst/notations/sphinx.py b/doc/tools/coqrst/notations/sphinx.py index ab18d136b8..5659a64b84 100644 --- a/doc/tools/coqrst/notations/sphinx.py +++ b/doc/tools/coqrst/notations/sphinx.py @@ -80,9 +80,11 @@ class TacticNotationsToSphinxVisitor(TacticNotationsVisitor): while atom != "": if atom[0] == "'": node += nodes.raw("\\textquotesingle{}", "\\textquotesingle{}", format="latex") + node += nodes.raw("'", "'", format="html") atom = atom[1:] elif atom[0] == "`": node += nodes.raw("\\`{}", "\\`{}", format="latex") + node += nodes.raw("`", "`", format="html") atom = atom[1:] else: index_ap = atom.find("'") |