aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
diff options
context:
space:
mode:
Diffstat (limited to 'doc/sphinx')
-rw-r--r--doc/sphinx/addendum/sprop.rst8
-rw-r--r--doc/sphinx/addendum/type-classes.rst24
-rw-r--r--doc/sphinx/changes.rst568
-rw-r--r--doc/sphinx/language/gallina-extensions.rst1
-rw-r--r--doc/sphinx/practical-tools/coqide.rst2
-rw-r--r--doc/sphinx/practical-tools/utilities.rst4
-rw-r--r--doc/sphinx/proof-engine/ssreflect-proof-language.rst281
-rw-r--r--doc/sphinx/proof-engine/tactics.rst86
-rw-r--r--doc/sphinx/user-extensions/syntax-extensions.rst63
9 files changed, 939 insertions, 98 deletions
diff --git a/doc/sphinx/addendum/sprop.rst b/doc/sphinx/addendum/sprop.rst
index c0c8c2d79c..8935ba27e3 100644
--- a/doc/sphinx/addendum/sprop.rst
+++ b/doc/sphinx/addendum/sprop.rst
@@ -10,9 +10,9 @@ SProp (proof irrelevant propositions)
This section describes the extension of |Coq| with definitionally
proof irrelevant propositions (types in the sort :math:`\SProp`, also
known as strict propositions). To use :math:`\SProp` you must pass
-``-allow-sprop`` to the |Coq| program or use :opt:`Allow StrictProp`.
+``-allow-sprop`` to the |Coq| program or use :flag:`Allow StrictProp`.
-.. opt:: Allow StrictProp
+.. flag:: Allow StrictProp
:name: Allow StrictProp
Allows using :math:`\SProp` when set and forbids it when unset. The
@@ -201,10 +201,10 @@ This means that some errors will be delayed until ``Qed``:
Abort.
-.. opt:: Elaboration StrictProp Cumulativity
+.. flag:: Elaboration StrictProp Cumulativity
:name: Elaboration StrictProp Cumulativity
- Unset this option (it's on by default) to be strict with regard to
+ Unset this flag (it is on by default) to be strict with regard to
:math:`\SProp` cumulativity during elaboration.
The implementation of proof irrelevance uses inferred "relevance"
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index b069cf27f4..77a6ee79cc 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -405,6 +405,8 @@ few other commands related to typeclasses.
resolution with the local hypotheses use full conversion during
unification.
+ + When considering local hypotheses, we use the union of all the modes
+ declared in the given databases.
.. cmdv:: typeclasses eauto @num
@@ -433,22 +435,26 @@ few other commands related to typeclasses.
.. _TypeclassesTransparent:
-Typeclasses Transparent, Typclasses Opaque
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Typeclasses Transparent, Typeclasses Opaque
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
.. cmd:: Typeclasses Transparent {+ @ident}
This command makes the identifiers transparent during typeclass
resolution.
+ Shortcut for :n:`Hint Transparent {+ @ident } : typeclass_instances`.
.. cmd:: Typeclasses Opaque {+ @ident}
- Make the identifiers opaque for typeclass search. It is useful when some
- constants prevent some unifications and make resolution fail. It is also
- useful to declare constants which should never be unfolded during
- proof-search, like fixpoints or anything which does not look like an
- abbreviation. This can additionally speed up proof search as the typeclass
- map can be indexed by such rigid constants (see
+ Make the identifiers opaque for typeclass search.
+ Shortcut for :n:`Hint Opaque {+ @ident } : typeclass_instances`.
+
+ It is useful when some constants prevent some unifications and make
+ resolution fail. It is also useful to declare constants which
+ should never be unfolded during proof-search, like fixpoints or
+ anything which does not look like an abbreviation. This can
+ additionally speed up proof search as the typeclass map can be
+ indexed by such rigid constants (see
:ref:`thehintsdatabasesforautoandeauto`).
By default, all constants and local variables are considered transparent. One
@@ -458,8 +464,6 @@ type, like:
.. coqdoc::
Definition relation A := A -> A -> Prop.
-This is equivalent to ``Hint Transparent, Opaque ident : typeclass_instances``.
-
Settings
~~~~~~~~
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index 57b9e45342..1c4c748295 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -2,6 +2,540 @@
Recent changes
--------------
+Version 8.10
+------------
+
+Summary of changes
+~~~~~~~~~~~~~~~~~~
+
+|Coq| version 8.10 contains two major new features: support for a native
+fixed-precision integer type and a new sort :math:`\SProp` of strict
+propositions. It is also the result of refinements and stabilization of
+previous features, deprecations or removals of deprecated features,
+cleanups of the internals of the system and API, and many documentation improvements.
+This release includes many user-visible changes, including deprecations that are
+documented in the next subsection, and new features that are documented in the
+reference manual. Here are the most important user-visible changes:
+
+- Kernel:
+
+ - A notion of primitive object was added to the calculus. Its first
+ instance is primitive cyclic unsigned integers, axiomatized in
+ module :g:`UInt63`. See Section :ref:`primitive-integers`.
+ The `Coq.Numbers.Cyclic.Int31` library is deprecated
+ (`#6914 <https://github.com/coq/coq/pull/6914>`_, by Maxime Dénès,
+ Benjamin Grégoire and Vincent Laporte,
+ with help and reviews from many others).
+
+ - The :math:`\SProp` sort of definitionally proof-irrelevant propositions was
+ introduced. :math:`\SProp` allows to mark proof
+ terms as irrelevant for conversion, and is treated like :math:`\Prop`
+ during extraction. It is enabled using the `-allow-sprop`
+ command-line flag or the :flag:`Allow StrictProp` flag.
+ See Chapter :ref:`sprop`
+ (`#8817 <https://github.com/coq/coq/pull/8817>`_, by Gaëtan Gilbert).
+
+ - The unfolding heuristic in termination checking was made more
+ complete, allowing more constants to be unfolded to discover valid
+ recursive calls. Performance regression may occur in Fixpoint
+ declarations without an explicit ``{struct}`` annotation, since
+ guessing the decreasing argument can now be more expensive
+ (`#9602 <https://github.com/coq/coq/pull/9602>`_, by Enrico Tassi).
+
+- Universes:
+
+ - Added :cmd:`Print Universes Subgraph` variant of :cmd:`Print Universes`.
+ Try for instance
+ :g:`Print Universes Subgraph(sigT2.u1 sigT_of_sigT2.u1 projT3_eq.u1).`
+ (`#8451 <https://github.com/coq/coq/pull/8451>`_, by Gaëtan Gilbert).
+
+ - Added private universes for opaque polymorphic constants, see the
+ documentation for the :flag:`Private Polymorphic Universes` flag,
+ and unset it to get the previous behaviour
+ (`#8850 <https://github.com/coq/coq/pull/8850>`_, by Gaëtan Gilbert).
+
+- Notations:
+
+ - New command :cmd:`String Notation` to register string syntax for custom
+ inductive types
+ (`#8965 <https://github.com/coq/coq/pull/8965>`_, by Jason Gross).
+
+ - Experimental: :ref:`Numeral Notations <numeral-notations>` now parse decimal
+ constants such as ``1.02e+01`` or ``10.2``. Parsers added for :g:`Q` and :g:`R`.
+ In the rare case when such numeral notations were used
+ in a development along with :g:`Q` or :g:`R`, they may have to be removed or
+ disambiguated through explicit scope annotations
+ (`#8764 <https://github.com/coq/coq/pull/8764>`_, by Pierre Roux).
+
+- Ltac backtraces can be turned on using the :flag:`Ltac Backtrace`
+ flag, which is off by default
+ (`#9142 <https://github.com/coq/coq/pull/9142>`_,
+ fixes `#7769 <https://github.com/coq/coq/issues/7769>`_
+ and `#7385 <https://github.com/coq/coq/issues/7385>`_,
+ by Pierre-Marie Pédrot).
+
+- The tactics :tacn:`lia`, :tacn:`nia`, :tacn:`lra`, :tacn:`nra` are now using a novel
+ Simplex-based proof engine. In case of regression, unset :flag:`Simplex`
+ to get the venerable Fourier-based engine
+ (`#8457 <https://github.com/coq/coq/pull/8457>`_, by Fréderic Besson).
+
+- SSReflect:
+
+ - New intro patterns:
+
+ - temporary introduction: `=> +`
+ - block introduction: `=> [^ prefix ] [^~ suffix ]`
+ - fast introduction: `=> >`
+ - tactics as views: `=> /ltac:mytac`
+ - replace hypothesis: `=> {}H`
+
+ See Section :ref:`introduction_ssr`
+ (`#6705 <https://github.com/coq/coq/pull/6705>`_, by Enrico Tassi,
+ with help from Maxime Dénès,
+ ideas coming from various users).
+
+ - New tactic :tacn:`under` to rewrite under binders, given an
+ extensionality lemma:
+
+ - interactive mode: :n:`under @term`, associated terminator: :tacn:`over`
+ - one-liner mode: `under @term do [@tactic | ...]`
+
+ It can take occurrence switches, contextual patterns, and intro patterns:
+ :g:`under {2}[in RHS]eq_big => [i|i ?] do ...`
+ (`#9651 <https://github.com/coq/coq/pull/9651>`_,
+ by Erik Martin-Dorel and Enrico Tassi).
+
+- :cmd:`Combined Scheme` now works when inductive schemes are generated in sort
+ :math:`\Type`. It used to be limited to sort `Prop`
+ (`#7634 <https://github.com/coq/coq/pull/7634>`_, by Théo Winterhalter).
+
+- A new registration mechanism for reference from ML code to Coq
+ constructs has been added
+ (`#186 <https://github.com/coq/coq/pull/186>`_,
+ by Emilio Jesús Gallego Arias, Maxime Dénès and Vincent Laporte).
+
+- CoqIDE:
+
+ - CoqIDE now depends on gtk+3 and lablgtk3 instead of gtk+2 and lablgtk2
+ (`#9279 <https://github.com/coq/coq/pull/9279>`_,
+ by Hugo Herbelin, with help from Jacques Garrigue,
+ Emilio Jesús Gallego Arias, Michael Sogetrop and Vincent Laporte).
+
+ - Smart input for Unicode characters. For example, typing
+ ``\alpha`` then ``Shift+Space`` will insert the greek letter alpha.
+ A larger number of default bindings are provided, following the latex
+ naming convention. Bindings can be customized, either globally, or on a
+ per-project basis. See Section :ref:`coqide-unicode` for details
+ (`#8560 <https://github.com/coq/coq/pull/8560>`_, by Arthur Charguéraud).
+
+- Infrastructure and dependencies:
+
+ - Coq 8.10 requires OCaml >= 4.05.0, bumped from 4.02.3 See the
+ `INSTALL` file for more information on dependencies
+ (`#7522 <https://github.com/coq/coq/pull/7522>`_, by Emilio Jesús Gallego Arías).
+
+ - Coq 8.10 doesn't need Camlp5 to build anymore. It now includes a
+ fork of the core parsing library that Coq uses, which is a small
+ subset of the whole Camlp5 distribution. In particular, this subset
+ doesn't depend on the OCaml AST, allowing easier compilation and
+ testing on experimental OCaml versions. Coq also ships a new parser
+ `coqpp` that plugin authors must switch to
+ (`#7902 <https://github.com/coq/coq/pull/7902>`_,
+ `#7979 <https://github.com/coq/coq/pull/7979>`_,
+ `#8161 <https://github.com/coq/coq/pull/8161>`_,
+ `#8667 <https://github.com/coq/coq/pull/8667>`_,
+ and `#8945 <https://github.com/coq/coq/pull/8945>`_,
+ by Pierre-Marie Pédrot and Emilio Jesús Gallego Arias).
+
+ The Coq developers would like to thank Daniel de Rauglaudre for many
+ years of continued support.
+
+ - Coq now supports building with Dune, in addition to the traditional
+ Makefile which is scheduled for deprecation
+ (`#6857 <https://github.com/coq/coq/pull/6857>`_,
+ by Emilio Jesús Gallego Arias, with help from Rudi Grinberg).
+
+ Experimental support for building Coq projects has been integrated
+ in Dune at the same time, providing an `improved experience
+ <https://coq.discourse.group/t/a-guide-to-building-your-coq-libraries-and-plugins-with-dune/>`_
+ for plugin developers. We thank the Dune team for their work
+ supporting Coq.
+
+Version 8.10 also comes with a bunch of smaller-scale changes and
+improvements regarding the different components of the system, including
+many additions to the standard library (see the next subsection for details).
+
+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 originally made by Yves Bertot
+is now in `doc/plugin_tutorial`. The ``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 and package building infrastructure.
+Coq is now continuously tested against OCaml trunk, in addition to the
+oldest supported and latest OCaml releases.
+
+Coq's documentation for the development branch is now deployed
+continously at https://coq.github.io/doc/master/api (documentation of
+the ML API), https://coq.github.io/doc/master/refman (reference
+manual), and https://coq.github.io/doc/master/stdlib (documentation of
+the standard library). Similar links exist for the `v8.10` branch.
+
+The OPAM repository for |Coq| packages has been maintained by Guillaume
+Melquiond, Matthieu Sozeau, Enrico Tassi (who migrated it to opam 2)
+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 David A. Dalrymple, Tanaka
+Akira, Benjamin Barenblat, Yves Bertot, Frédéric Besson, Lasse
+Blaauwbroek, Martin Bodin, Joachim Breitner, Tej Chajed, Frédéric
+Chapoton, Arthur Charguéraud, Cyril Cohen, Lukasz Czajka, Christian
+Doczkal, Maxime Dénès, Andres Erbsen, Jim Fehrle, Gaëtan Gilbert, Matěj
+Grabovský, Simon Gregersen, Jason Gross, Samuel Gruetter, Hugo Herbelin,
+Jasper Hugunin, Mirai Ikebuchi, Emilio Jesus Gallego Arias, Chantal
+Keller, Matej Košík, Vincent Laporte, Olivier Laurent, Larry Darryl Lee
+Jr, Pierre Letouzey, Nick Lewycky, Yao Li, Yishuai Li, Xia Li-yao, Assia
+Mahboubi, Simon Marechal, Erik Martin-Dorel, Thierry Martinez, Guillaume
+Melquiond, Kayla Ngan, Sam Pablo Kuper, Karl Palmskog, Clément
+Pit-Claudel, Pierre-Marie Pédrot, Pierre Roux, Kazuhiko Sakaguchi, Ryan
+Scott, Vincent Semeria, Gan Shen, Michael Soegtrop, Matthieu Sozeau,
+Enrico Tassi, Laurent Théry, Kamil Trzciński, whitequark, Théo
+Winterhalter, Beta Ziliani and 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,
+the coq-club@inria.fr mailing list or the new Discourse forum. It would
+be impossible to mention exhaustively the names of everybody who to some
+extent influenced the development.
+
+Version 8.10 is the fifth release of |Coq| developed on a time-based
+development cycle. Its development spanned 6 months from the release of
+|Coq| 8.9. Vincent Laporte is the release manager and maintainer of this
+release. This release is the result of ~2500 commits and ~650 PRs merged,
+closing 150+ issues.
+
+| Santiago de Chile, April 2019,
+| Matthieu Sozeau for the |Coq| development team
+|
+
+Other changes in 8.10+beta1
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+- Command-line tools and options:
+
+ - The use of `coqtop` as a compiler has been deprecated, in favor of
+ `coqc`. Consequently option `-compile` will stop to be accepted in
+ the next release. `coqtop` is now reserved to interactive
+ use
+ (`#9095 <https://github.com/coq/coq/pull/9095>`_,
+ by Emilio Jesús Gallego Arias).
+
+ - New option ``-topfile filename``, which will set the current module name
+ (*à la* ``-top``) based on the filename passed, taking into account the
+ proper ``-R``/``-Q`` options. For example, given ``-R Foo foolib`` using
+ ``-topfile foolib/bar.v`` will set the module name to ``Foo.Bar``.
+ CoqIDE now properly sets the module name for a given file based on
+ its path
+ (`#8991 <https://github.com/coq/coq/pull/8991>`_,
+ closes `#8989 <https://github.com/coq/coq/issues/8989>`_,
+ by Gaëtan Gilbert).
+
+ - Experimental: Coq flags and options can now be set on the
+ command-line, e.g. ``-set "Universe Polymorphism=true"``
+ (`#9876 <https://github.com/coq/coq/pull/9876>`_, by Gaëtan Gilbert).
+
+ - The `-native-compiler` flag of `coqc` and `coqtop` now takes an
+ argument which can have three values:
+
+ - `no` disables native_compute
+ - `yes` enables native_compute and precompiles `.v` files to
+ native code
+ - `ondemand` enables native_compute but compiles code only when
+ `native_compute` is called
+
+ The default value is `ondemand`. Note that this flag now has
+ priority over the configure flag of the same name.
+
+ A new `-bytecode-compiler` flag for `coqc` and `coqtop` controls
+ whether conversion can use the VM. The default value is `yes`.
+
+ (`#8870 <https://github.com/coq/coq/pull/8870>`_, by Maxime Dénès)
+
+ - The pretty timing diff scripts (flag `TIMING=1` to a
+ `coq_makefile`\-made `Makefile`, also
+ `tools/make-both-single-timing-files.py`,
+ `tools/make-both-time-files.py`, and `tools/make-one-time-file.py`)
+ now correctly support non-UTF-8 characters in the output of
+ `coqc` / `make` as well as printing to stdout, on both python2 and
+ python3
+ (`#9872 <https://github.com/coq/coq/pull/9872>`_,
+ closes `#9767 <https://github.com/coq/coq/issues/9767>`_
+ and `#9705 <https://github.com/coq/coq/issues/9705>`_,
+ by Jason Gross)
+
+ - coq_makefile's install target now errors if any file to install is missing
+ (`#9906 <https://github.com/coq/coq/pull/9906>`_, by Gaëtan Gilbert).
+
+ - Preferences from ``coqide.keys`` are no longer overridden by
+ modifiers preferences in ``coqiderc``
+ (`#10014 <https://github.com/coq/coq/pull/10014>`_, by Hugo Herbelin).
+
+- Specification language, type inference:
+
+ - Fixing a missing check in interpreting instances of existential
+ variables that are bound to local definitions. Might exceptionally
+ induce an overhead if the cost of checking the conversion of the
+ corresponding definitions is additionally high
+ (`#8217 <https://github.com/coq/coq/pull/8217>`_,
+ closes `#8215 <https://github.com/coq/coq/issues/8215>`_,
+ by Hugo Herbelin).
+
+ - A few improvements in inference of the return clause of `match` that
+ can exceptionally introduce incompatibilities. This can be
+ solved by writing an explicit `return` clause, sometimes even simply
+ an explicit `return _` clause
+ (`#262 <https://github.com/coq/coq/pull/262>`_, by Hugo Herbelin).
+
+ - Using non-projection values with the projection syntax is not
+ allowed. For instance :g:`0.(S)` is not a valid way to write :g:`S 0`.
+ Projections from non-primitive (emulated) records are allowed with
+ warning "nonprimitive-projection-syntax"
+ (`#8829 <https://github.com/coq/coq/pull/8829>`_, by Gaëtan Gilbert).
+
+ - An option and attributes to control the automatic decision to declare
+ an inductive type as template polymorphic were added. Warning
+ "auto-template" (off by default) can trigger when an inductive is
+ automatically declared template polymorphic without the attribute.
+
+ Inductive types declared by Funind will never be template polymorphic.
+
+ (`#8488 <https://github.com/coq/coq/pull/8488>`_, by Gaëtan Gilbert)
+
+- Notations:
+
+ - New command :cmd:`Declare Scope` to explicitly declare a scope name
+ before any use of it. Implicit declaration of a scope at the time of
+ :cmd:`Bind Scope`, :cmd:`Delimit Scope`, :cmd:`Undelimit Scope`,
+ or :cmd:`Notation` is deprecated
+ (`#7135 <https://github.com/coq/coq/pull/7135>`_, by Hugo Herbelin).
+
+ - Various bugs have been fixed (e.g. `#9214
+ <https://github.com/coq/coq/pull/9214>`_ on removing spurious
+ parentheses on abbreviations shortening a strict prefix of an
+ application, by Hugo Herbelin).
+
+ - :cmd:`Numeral Notation` now support inductive types in the input to
+ printing functions (e.g., numeral notations can be defined for terms
+ containing things like :g:`@cons nat O O`), and parsing functions now
+ fully normalize terms including parameters of constructors (so that,
+ e.g., a numeral notation whose parsing function outputs a proof of
+ :g:`Nat.gcd x y = 1` will no longer fail to parse due to containing the
+ constant :g:`Nat.gcd` in the parameter-argument of :g:`eq_refl`)
+ (`#9874 <https://github.com/coq/coq/pull/9840>`_,
+ closes `#9840 <https://github.com/coq/coq/issues/9840>`_
+ and `#9844 <https://github.com/coq/coq/issues/9844>`_,
+ by Jason Gross).
+
+ - Deprecated compatibility notations have actually been
+ removed. Uses of these notations are generally easy to fix thanks
+ to the hint contained in the deprecation warning emitted by Coq
+ 8.8 and 8.9. For projects that require more than a handful of
+ such fixes, there is `a script
+ <https://gist.github.com/JasonGross/9770653967de3679d131c59d42de6d17#file-replace-notations-py>`_
+ that will do it automatically, using the output of ``coqc``
+ (`#8638 <https://github.com/coq/coq/pull/8638>`_, by Jason Gross).
+
+- The `quote plugin
+ <https://coq.inria.fr/distrib/V8.9.0/refman/proof-engine/detailed-tactic-examples.html#quote>`_
+ was removed. If some users are interested in maintaining this plugin
+ externally, the Coq development team can provide assistance for
+ extracting the plugin and setting up a new repository
+ (`#7894 <https://github.com/coq/coq/pull/7894>`_, by Maxime Dénès).
+
+- Ltac:
+
+ - Tactic names are no longer allowed to clash, even if they are not defined in
+ the same section. For example, the following is no longer accepted:
+ :g:`Ltac foo := idtac. Section S. Ltac foo := fail. End S.`
+ (`#8555 <https://github.com/coq/coq/pull/8555>`_, by Maxime Dénès).
+
+ - Names of existential variables occurring in Ltac functions
+ (e.g. :g:`?[n]` or :g:`?n` in terms - not in patterns) are now interpreted
+ the same way as other variable names occurring in Ltac functions
+ (`#7309 <https://github.com/coq/coq/pull/7309>`_, by Hugo Herbelin).
+
+- Tactics:
+
+ - Removed the deprecated `romega` tactic
+ (`#8419 <https://github.com/coq/coq/pull/8419>`_,
+ by Maxime Dénès and Vincent Laporte).
+
+ - Hint declaration and removal should now specify a database (e.g. `Hint Resolve
+ foo : database`). When the database name is omitted, the hint is added to the
+ `core` database (as previously), but a deprecation warning is emitted
+ (`#8987 <https://github.com/coq/coq/pull/8987>`_, by Maxime Dénès).
+
+ - There are now tactics in `PreOmega.v` called
+ `Z.div_mod_to_equations`, `Z.quot_rem_to_equations`, and
+ `Z.to_euclidean_division_equations` (which combines the `div_mod`
+ and `quot_rem` variants) which allow :tacn:`lia`, :tacn:`nia`, etc to
+ support `Z.div` and `Z.modulo` (`Z.quot` and `Z.rem`, respectively),
+ by posing the specifying equation for `Z.div` and `Z.modulo` before
+ replacing them with atoms
+ (`#8062 <https://github.com/coq/coq/pull/8062>`_, by Jason Gross).
+
+ - The syntax of the :tacn:`autoapply` tactic was fixed to conform with preexisting
+ documentation: it now takes a `with` clause instead of a `using` clause
+ (`#9524 <https://github.com/coq/coq/pull/9524>`_,
+ closes `#7632 <https://github.com/coq/coq/issues/7632>`_,
+ by Théo Zimmermann).
+
+ - SSReflect clear discipline made consistent across the entire proof language.
+ Whenever a clear switch `{x..}` comes immediately before an existing proof
+ context entry (used as a view, as a rewrite rule or as name for a new
+ context entry) then such entry is cleared too.
+
+ E.g. The following sentences are elaborated as follows (when H is an existing
+ proof context entry):
+
+ - `=> {x..} H` -> `=> {x..H} H`
+ - `=> {x..} /H` -> `=> /v {x..H}`
+ - `rewrite {x..} H` -> `rewrite E {x..H}`
+
+ (`#9341 <https://github.com/coq/coq/pull/9341>`_, by Enrico Tassi).
+
+- Vernacular commands:
+
+ - Binders for an :cmd:`Instance` now act more like binders for a :cmd:`Theorem`.
+ Names may not be repeated, and may not overlap with section variable names
+ (`#8820 <https://github.com/coq/coq/pull/8820>`_,
+ closes `#8791 <https://github.com/coq/coq/issues/8791>`_,
+ by Jasper Hugunin).
+
+ - Removed the deprecated `Implicit Tactic` family of commands
+ (`#8779 <https://github.com/coq/coq/pull/8779>`_, by Pierre-Marie Pédrot).
+
+ - The `Automatic Introduction` option has been removed and is now the
+ default
+ (`#9001 <https://github.com/coq/coq/pull/9001>`_,
+ by Emilio Jesús Gallego Arias).
+
+ - `Arguments` now accepts names for arguments provided with `extra_scopes`
+ (`#9117 <https://github.com/coq/coq/pull/9117>`_, by Maxime Dénès).
+
+ - The naming scheme for anonymous binders in a `Theorem` has changed to
+ avoid conflicts with explicitly named binders
+ (`#9160 <https://github.com/coq/coq/pull/9160>`_,
+ closes `#8819 <https://github.com/coq/coq/issues/8819>`_,
+ by Jasper Hugunin).
+
+ - Computation of implicit arguments now properly handles local definitions in the
+ binders for an `Instance`, and can be mixed with implicit binders `{x : T}`
+ (`#9307 <https://github.com/coq/coq/pull/9307>`_,
+ closes `#9300 <https://github.com/coq/coq/issues/9300>`_,
+ by Jasper Hugunin).
+
+ - :cmd:`Declare Instance` now requires an instance name.
+
+ The flag :flag:`Refine Instance Mode` has been turned off by default,
+ meaning that :cmd:`Instance` no longer opens a proof when a body is
+ provided. The flag has been deprecated and will be removed in the next
+ version.
+
+ (`#9270 <https://github.com/coq/coq/pull/9270>`_,
+ and `#9825 <https://github.com/coq/coq/pull/9825>`_,
+ by Maxime Dénès)
+
+ - Command :cmd:`Instance`, when no body is provided, now always opens
+ a proof. This is a breaking change, as instance of :n:`Instance
+ @ident__1 : @ident__2.` where :n:`@ident__2` is a trivial class will
+ have to be changed into :n:`Instance @ident__1 : @ident__2 := {}.`
+ or :n:`Instance @ident__1 : @ident__2. Proof. Qed.`
+ (`#9274 <https://github.com/coq/coq/pull/9274>`_, by Maxime Dénès).
+
+ - The flag :flag:`Program Mode` now means that the `Program` attribute is enabled
+ for all commands that support it. In particular, it does not have any effect
+ on tactics anymore. May cause some incompatibilities
+ (`#9410 <https://github.com/coq/coq/pull/9410>`_, by Maxime Dénès).
+
+ - The algorithm computing implicit arguments now behaves uniformly for primitive
+ projection and application nodes
+ (`#9509 <https://github.com/coq/coq/pull/9509>`_,
+ closes `#9508 <https://github.com/coq/coq/issues/9508>`_,
+ by Pierre-Marie Pédrot).
+
+ - :cmd:`Hypotheses` and :cmd:`Variables` can now take implicit
+ binders inside sections
+ (`#9364 <https://github.com/coq/coq/pull/9364>`_,
+ closes `#9363 <https://github.com/coq/coq/issues/9363>`_,
+ by Jasper Hugunin).
+
+ - Removed deprecated option `Automatic Coercions Import`
+ (`#8094 <https://github.com/coq/coq/pull/8094>`_, by Maxime Dénès).
+
+ - The ``Show Script`` command has been deprecated
+ (`#9829 <https://github.com/coq/coq/pull/9829>`_, by Vincent Laporte).
+
+ - :cmd:`Coercion` does not warn ambiguous paths which are obviously
+ convertible with existing ones
+ (`#9743 <https://github.com/coq/coq/pull/9743>`_,
+ closes `#3219 <https://github.com/coq/coq/issues/3219>`_,
+ by Kazuhiko Sakaguchi).
+
+ - A new flag :flag:`Fast Name Printing` has been introduced. It changes the
+ algorithm used for allocating bound variable names for a faster but less
+ clever one
+ (`#9078 <https://github.com/coq/coq/pull/9078>`_, by Pierre-Marie Pédrot).
+
+ - Option ``Typeclasses Axioms Are Instances`` (compatibility option
+ introduced in the previous version) is deprecated. Use :cmd:`Declare
+ Instance` for axioms which should be instances
+ (`#8920 <https://github.com/coq/coq/pull/8920>`_, by Gaëtan Gilbert).
+
+ - Removed option `Printing Primitive Projection Compatibility`
+ (`#9306 <https://github.com/coq/coq/pull/9306>`_, by Gaëtan Gilbert).
+
+- Standard Library:
+
+ - Added `Bvector.BVeq` that decides whether two `Bvector`\s are equal.
+ Added notations for `BVxor`, `BVand`, `BVor`, `BVeq` and `BVneg`
+ (`#8171 <https://github.com/coq/coq/pull/8171>`_, by Yishuai Li).
+
+ - Added `ByteVector` type that can convert to and from `string`
+ (`#8365 <https://github.com/coq/coq/pull/8365>`_, by Yishuai Li).
+
+ - Added lemmas about monotonicity of `N.double` and `N.succ_double`, and about
+ the upper bound of number represented by a vector.
+ Allowed implicit vector length argument in `Ndigits.Bv2N`
+ (`#8815 <https://github.com/coq/coq/pull/8815>`_, by Yishuai Li).
+
+ - The prelude used to be automatically Exported and is now only
+ Imported. This should be relevant only when importing files which
+ don't use `-noinit` into files which do
+ (`#9013 <https://github.com/coq/coq/pull/9013>`_, by Gaëtan Gilert).
+
+ - Added `Coq.Structures.OrderedTypeEx.String_as_OT` to make strings an
+ ordered type, using lexical order
+ (`#7221 <https://github.com/coq/coq/pull/7221>`_, by Li Yao).
+
+ - Added lemmas about `Z.testbit`, `Z.ones`, and `Z.modulo`
+ (`#9425 <https://github.com/coq/coq/pull/9425>`_, by Andres Erbsen).
+
+ - Moved the `auto` hints of the `FSet` library into a new
+ `fset` database
+ (`#9725 <https://github.com/coq/coq/pull/9725>`_, by Frédéric Besson).
+
+- Some error messages that show problems with a pair of non-matching
+ values will now highlight the differences
+ (`#8669 <https://github.com/coq/coq/pull/8669>`_, by Jim Fehrle).
+
+
Version 8.9
-----------
@@ -12,7 +546,7 @@ Summary of changes
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
+deprecations that are documented in the next subsection and new features that
are documented in the reference manual. Here are the most important
changes:
@@ -26,7 +560,7 @@ changes:
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
+ next version of |Coq|, see the next subsection for a script to
ease porting, by Jason Gross and Jean-Christophe Léchenet.
- Added the :cmd:`Numeral Notation` command for registering decimal
@@ -79,7 +613,7 @@ changes:
- 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).
+ contributors (source of incompatibility, see the next subsection for details).
- Toplevels: ``coqtop`` and ``coqide`` can now display diffs between proof
steps in color, using the :opt:`Diffs` option, by Jim Fehrle.
@@ -96,7 +630,7 @@ changes:
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.
+important ones are documented in the next subsection file.
On the implementation side, the ``dev/doc/changes.md`` file documents
the numerous changes to the implementation and improvements of
@@ -152,8 +686,8 @@ engineer working with Maxime Dénès in the |Coq| consortium.
| Matthieu Sozeau for the |Coq| development team
|
-Details of changes
-~~~~~~~~~~~~~~~~~~
+Details of changes in 8.9+beta1
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Kernel
@@ -167,16 +701,12 @@ Notations
- Deprecated compatibility notations will actually be removed in the
next version of Coq. Uses of these notations are generally easy to
fix thanks to the hint contained in the deprecation warnings. For
- projects that require more than a handful of such fixes, there is [a
- script](https://gist.github.com/JasonGross/9770653967de3679d131c59d42de6d17#file-replace-notations-py)
- that will do it automatically, using the output of coqc. The script
+ projects that require more than a handful of such fixes, there is `a
+ script
+ <https://gist.github.com/JasonGross/9770653967de3679d131c59d42de6d17#file-replace-notations-py>`_
+ that will do it automatically, using the output of ``coqc``. The script
contains documentation on its usage in a comment at the top.
-- When several notations are available for the same expression,
- priority is given to latest notations defined in the scopes being
- opened, in order, rather than to the latest notations defined
- independently of whether they are in an opened scope or not.
-
Tactics
- Added toplevel goal selector `!` which expects a single focused goal.
@@ -260,7 +790,7 @@ Standard Library
`Require Import Coq.Compat.Coq88` will make these notations
available. Users wishing to port their developments automatically
may download `fix.py` from
- <https://gist.github.com/JasonGross/5d4558edf8f5c2c548a3d96c17820169>
+ https://gist.github.com/JasonGross/5d4558edf8f5c2c548a3d96c17820169
and run a command like `while true; do make -Okj 2>&1 |
/path/to/fix.py; done` and get a cup of coffee. (This command must
be manually interrupted once the build finishes all the way though.
@@ -284,8 +814,8 @@ Tools
If you would like to maintain this tool externally, please contact us.
- Removed the Emacs modes distributed with Coq. You are advised to
- use [Proof-General](https://proofgeneral.github.io/) (and optionally
- [Company-Coq](https://github.com/cpitclaudel/company-coq)) instead.
+ use `Proof-General <https://proofgeneral.github.io/>`_ (and optionally
+ `Company-Coq <https://github.com/cpitclaudel/company-coq>`_) instead.
If your use case is not covered by these alternative Emacs modes,
please open an issue. We can help set up external maintenance as part
of Proof-General, or independently as part of coq-community.
@@ -428,7 +958,7 @@ version.
Version 8.8 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.
+Most important ones are documented in the next subsection file.
The efficiency of the whole system has seen improvements thanks to
contributions from Gaëtan Gilbert, Pierre-Marie Pédrot, Maxime Dénès and
@@ -788,7 +1318,7 @@ 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
-others, documented in the ``CHANGES.md`` file.
+others, documented in the next subsection file.
The mathematical proof language/declarative mode plugin was removed from the
archive.
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 695dea222f..5308330820 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -2244,6 +2244,7 @@ Printing universes
unspecified if `string` doesn’t end in ``.dot`` or ``.gv``.
.. cmdv:: Print Universes Subgraph(@names)
+ :name: Print Universes Subgraph
Prints the graph restricted to the requested names (adjusting
constraints to preserve the implied transitive constraints between
diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst
index 97d86943fb..6cbd00f45d 100644
--- a/doc/sphinx/practical-tools/coqide.rst
+++ b/doc/sphinx/practical-tools/coqide.rst
@@ -252,6 +252,8 @@ use antialiased fonts or not, by setting the environment variable
`GDK_USE_XFT` to 1 or 0 respectively.
+.. _coqide-unicode:
+
Bindings for input of Unicode symbols
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst
index 8346b72cb9..35231610fe 100644
--- a/doc/sphinx/practical-tools/utilities.rst
+++ b/doc/sphinx/practical-tools/utilities.rst
@@ -144,6 +144,10 @@ Here we describe only few of them.
:CAMLFLAGS:
can be used to specify additional flags to the |OCaml|
compiler, like ``-bin-annot`` or ``-w``....
+:OCAMLWARN:
+ it contains a default of ``-warn-error +a-3``, useful to modify
+ this setting; beware this is not recommended for projects in
+ Coq's CI.
:COQC, COQDEP, COQDOC:
can be set in order to use alternative binaries
(e.g. wrappers)
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index b240cef40c..4e40df6f94 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -1737,9 +1737,8 @@ Intro patterns
for each :token:`ident`. Its type has to be fixed later on by using the
``abstract`` tactic. Before then the type displayed is ``<hidden>``.
-
Note that |SSR| does not support the syntax ``(ipat, …, ipat)`` for
-destructing intro-patterns.
+destructing intro patterns.
Clear switch
````````````
@@ -3626,7 +3625,7 @@ corresponding new goals will be generated.
As in :ref:`apply_ssr`, the ``ssrautoprop`` tactic is used to try to
solve the existential variable.
- .. coqtop:: all
+ .. coqtop:: all abort
Lemma test (x : 'I_2) y (H : y < 2) : Some x = insub 2 y.
rewrite insubT.
@@ -3637,6 +3636,272 @@ rewriting rule is stated using Leibniz equality (as opposed to setoid
relations). It will be extended to other rewriting relations in the
future.
+.. _under_ssr:
+
+Rewriting under binders
+~~~~~~~~~~~~~~~~~~~~~~~
+
+Goals involving objects defined with higher-order functions often
+require "rewriting under binders". While setoid rewriting is a
+possible approach in this case, it is common to use regular rewriting
+along with dedicated extensionality lemmas. This may cause some
+practical issues during the development of the corresponding scripts,
+notably as we might be forced to provide the rewrite tactic with
+complete terms, as shown by the simple example below.
+
+.. example::
+
+ .. coqtop:: reset none
+
+ From Coq Require Import ssreflect.
+ Set Implicit Arguments.
+ Unset Strict Implicit.
+ Unset Printing Implicit Defensive.
+
+ .. coqtop:: in
+
+ Axiom subnn : forall n : nat, n - n = 0.
+ Parameter map : (nat -> nat) -> list nat -> list nat.
+ Parameter sumlist : list nat -> nat.
+ Axiom eq_map :
+ forall F1 F2 : nat -> nat,
+ (forall n : nat, F1 n = F2 n) ->
+ forall l : list nat, map F1 l = map F2 l.
+
+ .. coqtop:: all
+
+ Lemma example_map l : sumlist (map (fun m => m - m) l) = 0.
+
+ In this context, one cannot directly use ``eq_map``:
+
+ .. coqtop:: all fail
+
+ rewrite eq_map.
+
+ as we need to explicitly provide the non-inferable argument ``F2``,
+ which corresponds here to the term we want to obtain *after* the
+ rewriting step. In order to perform the rewrite step one has to
+ provide the term by hand as follows:
+
+ .. coqtop:: all abort
+
+ rewrite (@eq_map _ (fun _ : nat => 0)).
+ by move=> m; rewrite subnn.
+
+ The :tacn:`under` tactic lets one perform the same operation in a more
+ convenient way:
+
+ .. coqtop:: all abort
+
+ Lemma example_map l : sumlist (map (fun m => m - m) l) = 0.
+ under eq_map => m do rewrite subnn.
+
+
+The under tactic
+````````````````
+
+The convenience :tacn:`under` tactic supports the following syntax:
+
+.. tacn:: under {? @r_prefix } @term {? => {+ @i_item}} {? do ( @tactic | [ {*| @tactic } ] ) }
+ :name: under
+
+ Operate under the context proved to be extensional by
+ lemma :token:`term`.
+
+ .. exn:: Incorrect number of tactics (expected N tactics, was given M).
+
+ This error can occur when using the version with a ``do`` clause.
+
+ The multiplier part of :token:`r_prefix` is not supported.
+
+We distinguish two modes,
+:ref:`interactive mode <under_interactive>` without a ``do`` clause, and
+:ref:`one-liner mode <under_one_liner>` with a ``do`` clause,
+which are explained in more detail below.
+
+.. _under_interactive:
+
+Interactive mode
+````````````````
+
+Let us redo the running example in interactive mode.
+
+.. example::
+
+ .. coqtop:: all abort
+
+ Lemma example_map l : sumlist (map (fun m => m - m) l) = 0.
+ under eq_map => m.
+ rewrite subnn.
+ over.
+
+The execution of the Ltac expression:
+
+:n:`under @term => [ @i_item__1 | … | @i_item__n ].`
+
+involves the following steps:
+
+1. It performs a :n:`rewrite @term`
+ without failing like in the first example with ``rewrite eq_map.``,
+ but creating evars (see :tacn:`evar`). If :n:`term` is prefixed by
+ a pattern or an occurrence selector, then the modifiers are honoured.
+
+2. As a n-branches intro pattern is provided :tacn:`under` checks that
+ n+1 subgoals have been created. The last one is the main subgoal,
+ while the other ones correspond to premises of the rewrite rule (such as
+ ``forall n, F1 n = F2 n`` for ``eq_map``).
+
+3. If so :tacn:`under` puts these n goals in head normal form (using
+ the defective form of the tactic :tacn:`move`), then executes
+ the corresponding intro pattern :n:`@ipat__i` in each goal.
+
+4. Then :tacn:`under` checks that the first n subgoals
+ are (quantified) equalities or double implications between a
+ term and an evar (e.g. ``m - m = ?F2 m`` in the running example).
+
+5. If so :tacn:`under` protects these n goals against an
+ accidental instantiation of the evar.
+ These protected goals are displayed using the ``Under[ … ]``
+ notation (e.g. ``Under[ m - m ]`` in the running example).
+
+6. The expression inside the ``Under[ … ]`` notation can be
+ proved equivalent to the desired expression
+ by using a regular :tacn:`rewrite` tactic.
+
+7. Interactive editing of the first n goals has to be signalled by
+ using the :tacn:`over` tactic or rewrite rule (see below).
+
+8. Finally, a post-processing step is performed in the main goal
+ to keep the name(s) for the bound variables chosen by the user in
+ the intro pattern for the first branch.
+
+.. _over_ssr:
+
+The over tactic
++++++++++++++++
+
+Two equivalent facilities (a terminator and a lemma) are provided to
+close intermediate subgoals generated by :tacn:`under` (i.e. goals
+displayed as ``Under[ … ]``):
+
+.. tacn:: over
+ :name: over
+
+ This terminator tactic allows one to close goals of the form
+ ``'Under[ … ]``.
+
+.. tacv:: by rewrite over
+
+ This is a variant of :tacn:`over` in order to close ``Under[ … ]``
+ goals, relying on the ``over`` rewrite rule.
+
+.. _under_one_liner:
+
+One-liner mode
+``````````````
+
+The Ltac expression:
+
+:n:`under @term => [ @i_item__1 | … | @i_item__n ] do [ @tac__1 | … | @tac__n ].`
+
+can be seen as a shorter form for the following expression:
+
+:n:`(under @term) => [ @i_item__1 | … | @i_item__n | ]; [ @tac__1; over | … | @tac__n; over | cbv beta iota ].`
+
+Notes:
+
++ The ``beta-iota`` reduction here is useful to get rid of the beta
+ redexes that could be introduced after the substitution of the evars
+ by the :tacn:`under` tactic.
+
++ Note that the provided tactics can as well
+ involve other :tacn:`under` tactics. See below for a typical example
+ involving the `bigop` theory from the Mathematical Components library.
+
++ If there is only one tactic, the brackets can be omitted, e.g.:
+ :n:`under @term => i do @tac.` and that shorter form should be
+ preferred.
+
++ If the ``do`` clause is provided and the intro pattern is omitted,
+ then the default :token:`i_item` ``*`` is applied to each branch.
+ E.g., the Ltac expression:
+ :n:`under @term do [ @tac__1 | … | @tac__n ]` is equivalent to:
+ :n:`under @term => [ * | … | * ] do [ @tac__1 | … | @tac__n ]`
+ (and it can be noted here that the :tacn:`under` tactic performs a
+ ``move.`` before processing the intro patterns ``=> [ * | … | * ]``).
+
+.. example::
+
+ .. coqtop:: reset none
+
+ From Coq Require Import ssreflect.
+ Set Implicit Arguments.
+ Unset Strict Implicit.
+ Unset Printing Implicit Defensive.
+
+ Coercion is_true : bool >-> Sortclass.
+
+ Reserved Notation "\big [ op / idx ]_ ( m <= i < n | P ) F"
+ (at level 36, F at level 36, op, idx at level 10, m, i, n at level 50,
+ format "'[' \big [ op / idx ]_ ( m <= i < n | P ) F ']'").
+ Variant bigbody (R I : Type) : Type :=
+ BigBody : forall (_ : I) (_ : forall (_ : R) (_ : R), R) (_ : bool) (_ : R), bigbody R I.
+
+ Parameter bigop :
+ forall (R I : Type) (_ : R) (_ : list I) (_ : forall _ : I, bigbody R I), R.
+
+ Axiom eq_bigr_ :
+ forall (R : Type) (idx : R) (op : forall (_ : R) (_ : R), R) (I : Type)
+ (r : list I) (P : I -> bool) (F1 F2 : I -> R),
+ (forall x : I, is_true (P x) -> F1 x = F2 x) ->
+ bigop idx r (fun i : I => BigBody i op (P i) (F1 i)) =
+ bigop idx r (fun i : I => BigBody i op (P i) (F2 i)).
+
+ Axiom eq_big_ :
+ forall (R : Type) (idx : R) (op : R -> R -> R) (I : Type) (r : list I)
+ (P1 P2 : I -> bool) (F1 F2 : I -> R),
+ (forall x : I, P1 x = P2 x) ->
+ (forall i : I, is_true (P1 i) -> F1 i = F2 i) ->
+ bigop idx r (fun i : I => BigBody i op (P1 i) (F1 i)) =
+ bigop idx r (fun i : I => BigBody i op (P2 i) (F2 i)).
+
+ Reserved Notation "\sum_ ( m <= i < n | P ) F"
+ (at level 41, F at level 41, i, m, n at level 50,
+ format "'[' \sum_ ( m <= i < n | P ) '/ ' F ']'").
+
+ Parameter index_iota : nat -> nat -> list nat.
+
+ Notation "\big [ op / idx ]_ ( m <= i < n | P ) F" :=
+ (bigop idx (index_iota m n) (fun i : nat => BigBody i op P%bool F)).
+
+ Notation "\sum_ ( m <= i < n | P ) F" :=
+ (\big[plus/O]_(m <= i < n | P%bool) F%nat).
+
+ Notation eq_bigr := (fun n m => eq_bigr_ 0 plus (index_iota n m)).
+ Notation eq_big := (fun n m => eq_big_ 0 plus (index_iota n m)).
+
+ Parameter odd : nat -> bool.
+ Parameter prime : nat -> bool.
+
+ .. coqtop:: in
+
+ Parameter addnC : forall m n : nat, m + n = n + m.
+ Parameter muln1 : forall n : nat, n * 1 = n.
+
+ .. coqtop:: all
+
+ Check eq_bigr.
+ Check eq_big.
+
+ Lemma test_big_nested (m n : nat) :
+ \sum_(0 <= a < m | prime a) \sum_(0 <= j < n | odd (j * 1)) (a + j) =
+ \sum_(0 <= i < m | prime i) \sum_(0 <= j < n | odd j) (j + i).
+ under eq_bigr => i prime_i do
+ under eq_big => [ j | j odd_j ] do
+ [ rewrite (muln1 j) | rewrite (addnC i j) ].
+
+ Remark how the final goal uses the name ``i`` (the name given in the
+ intro pattern) rather than ``a`` in the binder of the first summation.
.. _locking_ssr:
@@ -5373,7 +5638,15 @@ respectively.
.. tacn:: rewrite {+ @r_step }
- rewrite (see :ref:`rewriting_ssr`)
+ rewrite (see :ref:`rewriting_ssr`)
+
+.. tacn:: under {? @r_prefix } @term {? => {+ @i_item}} {? do ( @tactic | [ {*| @tactic } ] )}
+
+ under (see :ref:`under_ssr`)
+
+.. tacn:: over
+
+ over (see :ref:`over_ssr`)
.. tacn:: have {* @i_item } {? @i_pattern } {? @s_item %| {+ @ssr_binder } } {? : @term } := @term
have {* @i_item } {? @i_pattern } {? @s_item %| {+ @ssr_binder } } : @term {? by @tactic }
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index e6922408aa..1f339e7761 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -4724,6 +4724,12 @@ Non-logical tactics
from the shelf into focus, by appending them to the end of the current
list of focused goals.
+.. tacn:: unshelve @tactic
+ :name: unshelve
+
+ Performs :n:`@tactic`, then unshelves existential variables added to the
+ shelf by the execution of :n:`@tactic`, prepending them to the current goal.
+
.. tacn:: give_up
:name: give_up
@@ -4805,3 +4811,83 @@ references to automatically generated names.
:name: Mangle Names Prefix
Specifies the prefix to use when generating names.
+
+Performance-oriented tactic variants
+------------------------------------
+
+.. tacn:: change_no_check @term
+ :name: change_no_check
+
+ For advanced usage. Similar to :n:`change @term`, but as an optimization,
+ it skips checking that :n:`@term` is convertible to the goal.
+
+ Recall that the Coq kernel typechecks proofs again when they are concluded to
+ ensure safety. Hence, using :tacn:`change` checks convertibility twice
+ overall, while :tacn:`change_no_check` can produce ill-typed terms,
+ but checks convertibility only once.
+ Hence, :tacn:`change_no_check` can be useful to speed up certain proof
+ scripts, especially if one knows by construction that the argument is
+ indeed convertible to the goal.
+
+ In the following example, :tacn:`change_no_check` replaces :g:`False` by
+ :g:`True`, but :g:`Qed` then rejects the proof, ensuring consistency.
+
+ .. example::
+
+ .. coqtop:: all abort
+
+ Goal False.
+ change_no_check True.
+ exact I.
+ Fail Qed.
+
+ .. tacv:: convert_concl_no_check @term
+ :name: convert_concl_no_check
+
+ Deprecated old name for :tacn:`change_no_check`. Does not support any of its
+ variants.
+
+.. tacn:: exact_no_check @term
+ :name: exact_no_check
+
+ For advanced usage. Similar to :n:`exact @term`, but as an optimization,
+ it skips checking that :n:`@term` has the goal's type, relying on the kernel
+ check instead. See :tacn:`change_no_check` for more explanations.
+
+ .. example::
+
+ .. coqtop:: all abort
+
+ Goal False.
+ exact_no_check I.
+ Fail Qed.
+
+ .. tacv:: vm_cast_no_check @term
+ :name: vm_cast_no_check
+
+ For advanced usage. Similar to :n:`exact_no_check @term`, but additionally
+ instructs the kernel to use :tacn:`vm_compute` to compare the
+ goal's type with the :n:`@term`'s type.
+
+ .. example::
+
+ .. coqtop:: all abort
+
+ Goal False.
+ vm_cast_no_check I.
+ Fail Qed.
+
+ .. tacv:: native_cast_no_check @term
+ :name: native_cast_no_check
+
+ for advanced usage. similar to :n:`exact_no_check @term`, but additionally
+ instructs the kernel to use :tacn:`native_compute` to compare the goal's
+ type with the :n:`@term`'s type.
+
+ .. example::
+
+ .. coqtop:: all abort
+
+ Goal False.
+ native_cast_no_check I.
+ Fail Qed.
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 63df3d37bf..ac079ea7d5 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1040,8 +1040,6 @@ interpreted in the scope stack extended with the scope bound tokey.
To remove a delimiting key of a scope, use the command
:n:`Undelimit Scope @scope`
-.. _ArgumentScopes:
-
Binding arguments of a constant to an interpretation scope
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
@@ -1311,65 +1309,6 @@ Displaying information about scopes
It also displays the delimiting key if any and the class to which the
scope is bound, if any.
-Impact of scopes on printing
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-When several notations are available for printing the same expression,
-Coq will use the following rules for printing priorities:
-
-- If two notations are available in different scopes which are open,
- the notation in the more recently opened scope takes precedence.
-
-- If two notations are available in the same scope, the more recently
- defined (or imported) notation takes precedence.
-
-- Abbreviations and lonely notations, both of which have no scope,
- take precedence over a notation in an open scope if and only if the
- abbreviation or lonely notation was defined (or imported) more
- recently than when the corresponding scope was open. They take
- precedence over any notation not in an open scope, whether this scope
- has a delimiter or not.
-
-- A scope is *active* for printing a term either because it was opened
- with :cmd:`Open Scope`, or the term is the immediate argument of a
- constant which temporarily opens a scope for this argument (see
- :ref:`Arguments <ArgumentScopes>`) in which case this temporary
- scope is the most recent open one.
-
-- In case no abbreviation, nor lonely notation, nor notation in an
- explicitly open scope, nor notation in a temporarily open scope of
- arguments, has been found, notations in those closed scopes which
- have a delimiter are considered, giving priority to the most
- recently defined (or imported) ones. The corresponding delimiter is
- inserted, making the corresponding scope the most recent explicitly
- open scope for all subterms of the current term. As an exception to
- the insertion of the corresponding delimiter, when an expression is
- statically known to be in a position expecting a type and the
- notation is from scope ``type_scope``, and the latter is closed, the
- delimiter is not inserted. This is because expressions statically
- known to be in a position expecting a type are by default
- interpreted with `type_scope` temporarily activated. Expressions
- statically known to be in a position expecting a type typically
- include being on the right-hand side of `:`, `<:`, `<<:` and after
- the comma in a `forall` expression.
-
-- As a refinement of the previous rule, in the case of applied global
- references, notations in a non-opened scope with delimiter
- specifically defined for this applied global reference take priority
- over notations in a non-opened scope with delimiter for generic
- applications. For instance, in the presence of ``Notation "f ( x
- )" := (f x) (at level 10, format "f ( x )") : app_scope`` and
- ``Notation "x '.+1'" := (S x) (at level 10, format "x '.+1'") :
- mynat_scope.`` and both of ``app_scope`` and ``mynat_scope`` being
- bound to a delimiter *and* both not opened, the latter, more
- specific notation will always take precedence over the first, more
- generic one.
-
-- A scope can be closed by using :cmd:`Close Scope` and its delimiter
- removed by using :cmd:`Undelimit Scope`. To remove automatic
- temporary opening of scopes for arguments of a constant, use
- :ref:`Arguments <ArgumentScopes>`.
-
.. _Abbreviations:
Abbreviations
@@ -1437,6 +1376,8 @@ Abbreviations
denoted expression is performed at definition time. Type checking is
done only at the time of use of the abbreviation.
+.. _numeral-notations:
+
Numeral notations
-----------------
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 04:25:49 +0000