Credits for 8.10

2 files changed, 448 insertions, 0 deletions

diff --git a/CHANGES.md b/CHANGES.md
index 51583639ca..5a91bc2428 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -113,6 +113,7 @@ Plugins
 Tactics
 
 - Removed the deprecated `romega` tactics.
+
 - 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:
   `Ltac foo := idtac. Section S. Ltac foo := fail. End S.`
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index 57b9e45342..10cbbcfcaa 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -2,6 +2,453 @@
 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 `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. This release includes
+many user-visible changes, including deprecations that are documented in
+the following section, 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 UInt63(link), by Maxime Dénès, Benjamin Grégoire and Vincent
+    Laporte. See Section :ref:`primitive-integers`.
+
+  - The :math:`\SProp` sort of definitionally proof-irrelevant propositions was
+    introduced by Gaëtan Gilbert. :math:`\SProp` allows to mark proof
+    terms as irrelevant for conversion, and is treated like `Prop`
+    during extraction. It is enabled using the `-allow-sprop`
+    command-line flag. See Section :ref:`sprop`.
+
+  - The unfolding heuristic in termination checking was made more complete
+    by Enrico Tassi, allowing more constants to be unfolded to discover
+    valid recursive calls.
+
+- Universes:
+
+  - Added :cmd:`Print Universes Subgraph` variant of :cmd:`Print Universes` and
+    private universes for opaque polymorphic constants, by Gaëtan Gilbert.
+
+- Notations:
+
+  - New command :cmd:`String Notation` to register string syntax for custom
+    inductive types, by Jason Gross.
+
+  - Numeral Notations now parse decimal constants, by Pierre Roux.
+
+- Ltac:
+
+  - Ltac backtraces can be turned on using the :opt:`Ltac Backtrace` option,
+    by Pierre-Marie Pédrot.
+
+
+- The tactics :tac:`lia`, :tac:`nia`, :tac:`lra`, :tac:`nra` are now using a novel
+  Simplex-based proof engine, by Fréderic Besson.
+
+- SSReflect has new intro patterns and a consistent clear discipline, by
+  Enrico Tassi.
+
+- :cmd:`Combined Scheme` now works when inductive schemes are generated in sort
+  `Type`, by Théo Winterhalter.
+
+- A new registration mechanism for reference from ML code to Coq
+  constructs has been added, by Emilio Jesús Gallego Arias.
+
+- CoqIDE:
+
+  - Migrated to gtk+3 and lablgtk3 by Hugo Herbelin and Jacques Garrigue.
+
+  - Supports smart input for Unicode characters by Arthur Charguéraud.
+
+- Infrastructure:
+
+  - Coq 8.10 requires OCaml >= 4.05.0, bumped from 4.02.3 See the
+    `INSTALL` file for more information on dependencies.
+
+  - Coq now supports building with Dune, in addition to the traditional
+    Makefile which is scheduled for deprecation, by Emilio Jesús Gallego
+    Arias and 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.
+
+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 Laport is the release manager and maintainer of this
+release. This release is the result of ??? commits and ??? PRs
+merged, closing ??? issues.
+
+| Santiago de Chile, April 2019,
+| Matthieu Sozeau for the |Coq| development team
+|
+
+Details of changes
+~~~~~~~~~~~~~~~~~~
+
+OCaml and dependencies
+
+- 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.
+
+  The Coq developers would like to thank Daniel de Rauglaudre for many
+  years of continued support.
+
+Coqide
+
+- CoqIDE now depends on gtk+3 and lablgtk3, rather than gtk+2 and lablgtk2.
+
+- CoqIDE now properly sets the module name for a given file based on
+  its path, see `-topfile` change entry for more details.
+
+Coqtop
+
+- 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. (@ejgallego #9095)
+
+- 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.
+
+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 (PR #8215).
+
+- A few improvements in inference of the return clause of `match` can
+  exceptionally introduce incompatibilities (PR #262). This can be
+  solved by writing an explicit `return` clause, sometimes even simply
+  an explicit `return _` clause.
+
+- Using non-projection values with the projection syntax is not
+  allowed. For instance "0.(S)" is not a valid way to write "S 0".
+  Projections from non-primitive (emulated) records are allowed with
+  warning "nonprimitive-projection-syntax".
+
+Kernel
+
+- Added primitive integers
+
+- Unfolding heuristic in termination checking made more complete.
+  In particular Coq is now more aggressive in unfolding constants
+  when it looks for a iota redex. Performance regression may occur
+  in Fixpoint declarations without an explicit {struct} annotation,
+  since guessing the decreasing argument can now be more expensive.
+  (PR #9602)
+
+Notations
+
+- New command `Declare Scope` to explicitly declare a scope name
+  before any use of it. Implicit declaration of a scope at the time of
+  `Bind Scope`, `Delimit Scope`, `Undelimit Scope`, or `Notation` is
+  deprecated.
+
+- New command `String Notation` to register string syntax for custom
+  inductive types.
+
+- Numeral notations now parse decimal constants such as 1.02e+01 or
+  10.2. Parsers added for Q and R. This should be considered as an
+  experimental feature currently.
+  Note: in -- the rare -- case when such numeral notations were used
+  in a development along with Q or R, they may have to be removed or
+  deconflicted through explicit scope annotations (1.23%Q,
+  45.6%R,...).
+
+- Various bugs have been fixed (e.g. PR #9214 on removing spurious
+  parentheses on abbreviations shortening a strict prefix of an application).
+
+- Numeral Notations now support inductive types in the input to
+  printing functions (e.g., numeral notations can be defined for terms
+  containing things like `@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
+  `Nat.gcd x y = 1` will no longer fail to parse due to containing the
+  constant `Nat.gcd` in the parameter-argument of `eq_refl`).  See
+  #9840 for more details.
+
+- Deprecated compatibility notations have actually been removed.  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
+  contains documentation on its usage in a comment at the top.
+
+Plugins
+
+- The quote plugin (https://coq.inria.fr/distrib/V8.8.1/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.
+
+Tactics
+
+- Removed the deprecated `romega` tactics.
+- 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:
+  `Ltac foo := idtac. Section S. Ltac foo := fail. End S.`
+
+- The tactics 'lia','nia','lra','nra' are now using a novel
+  Simplex-based proof engine. In case of regression, 'Unset Simplex'
+  to get the venerable Fourier-based engine.
+
+- Names of existential variables occurring in Ltac functions
+  (e.g. `?[n]` or `?n` in terms - not in patterns) are now interpreted
+  the same way as other variable names occurring in Ltac functions.
+
+- 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.
+
+- 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 `lia`, `nia`, `romega`, 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.
+
+- Ltac backtraces can be turned on using the "Ltac Backtrace" option.
+
+- The syntax of the `autoapply` tactic was fixed to conform with preexisting
+  documentation: it now takes a `with` clause instead of a `using` clause.
+
+
+
+Vernacular commands
+
+- `Combined Scheme` can now work when inductive schemes are generated in sort
+  `Type`. It used to be limited to sort `Prop`.
+
+- Binders for an `Instance` now act more like binders for a `Theorem`.
+  Names may not be repeated, and may not overlap with section variable names.
+
+- Removed the deprecated `Implicit Tactic` family of commands.
+
+- The `Automatic Introduction` option has been removed and is now the
+  default.
+
+- `Arguments` now accepts names for arguments provided with `extra_scopes`.
+
+- The naming scheme for anonymous binders in a `Theorem` has changed to
+  avoid conflicts with explicitly named binders.
+
+- Computation of implicit arguments now properly handles local definitions in the
+  binders for an `Instance`, and can be mixed with implicit binders `{x : T}`.
+
+- `Declare Instance` now requires an instance name.
+
+- Option `Refine Instance Mode` has been turned off by default, meaning that
+  `Instance` no longer opens a proof when a body is provided.
+
+- `Instance`, when no body is provided, now always opens a proof. This is a
+   breaking change, as instance of `Instance foo : C.` where `C` is a trivial
+   class will have to be changed into `Instance foo : C := {}.` or
+   `Instance foo : C. Proof. Qed.`.
+
+- Option `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.
+
+- The algorithm computing implicit arguments now behaves uniformly for primitive
+  projection and application nodes (bug #9508).
+
+- `Hypotheses` and `Variables` can now take implicit binders inside sections.
+
+- Removed deprecated option `Automatic Coercions Import`.
+
+- The `Show Script` command has been deprecated.
+
+- Option `Refine Instance Mode` has been deprecated and will be removed in
+  the next version.
+
+- `Coercion` does not warn ambiguous paths which are obviously convertible with
+  existing ones.
+
+- A new flag `Fast Name Printing` has been introduced. It changes the
+  algorithm used for allocating bound variable names for a faster but less
+  clever one.
+
+Tools
+
+- 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`.
+
+- CoqIDE now supports input for Unicode characters. For example, typing
+  "\alpha" then the "Shift+Space" will insert the greek letter alpha.
+  In fact, typing the prefix string "\a" is sufficient.
+  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, with the requirement is that keys must begin with a
+  backslash and contain no space character. Bindings may be assigned custom
+  priorities, so that prefixes resolve to the most convenient bindings.
+  The documentation pages for CoqIDE provides further details.
+
+- 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.
+
+Standard Library
+
+- 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`.
+
+- Added `Bvector.BVeq` that decides whether two `Bvector`s are equal.
+
+- Added notations for `BVxor`, `BVand`, `BVor`, `BVeq` and `BVneg`.
+
+- Added `ByteVector` type that can convert to and from [string].
+
+- 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.
+
+- Added `Coq.Structures.OrderedTypeEx.String_as_OT` to make strings an
+  ordered type (using lexical order).
+
+- The `Coq.Numbers.Cyclic.Int31` library is deprecated.
+
+- Added lemmas about `Z.testbit`, `Z.ones`, and `Z.modulo`.
+
+- Moved the `auto` hints of the `FSet` library into a new
+  `fset` database.
+
+Universes
+
+- Added `Print Universes Subgraph` variant of `Print Universes`.
+  Try for instance `Print Universes Subgraph(sigT2.u1 sigT_of_sigT2.u1 projT3_eq.u1 eq_sigT2_rect.u1).`
+
+- Added private universes for opaque polymorphic constants, see doc
+  for the "Private Polymorphic Universes" option (and Unset it to get
+  the previous behaviour).
+
+SProp
+
+- Added a universe "SProp" for definitionally proof irrelevant
+  propositions. Use with -allow-sprop. See manual for details.
+
+Inductives
+
+- 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.
+
+Funind
+
+- Inductive types declared by Funind will never be template polymorphic.
+
+Misc
+
+- Option "Typeclasses Axioms Are Instances" is deprecated. Use Declare Instance for axioms which should be instances.
+
+- Removed option "Printing Primitive Projection Compatibility"
+
+SSReflect
+
+- New intro patterns:
+  - temporary introduction: `=> +`
+  - block introduction: `=> [^ prefix ] [^~ suffix ]`
+  - fast introduction: `=> >`
+  - tactics as views: `=> /ltac:mytac`
+  - replace hypothesis: `=> {}H`
+  See the reference manual for the actual documentation.
+
+- 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}`
+
+Diffs
+
+- Some error messages that show problems with a pair of non-matching values will now
+  highlight the differences.
+
 Version 8.9
 -----------