Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: skolemization.pvs   Sprache: PVS

Untersuchungsergebnis.rst Download desHaskell {Haskell[225] BAT[451] Ada[462]}zum Wurzelverzeichnis wechseln

--------------
Recent changes
--------------

.. ifconfig:: not coq_config.is_a_released_version

   .. include:: ../unreleased.rst

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: :n:`under @term do [@tactic | ...]`

    It can take occurrence switches, contextual patterns, and intro patterns:
    :g:`under {2}[in RHS]eq_big => [i|i ?]`
    (`#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.
    The INSTALL file available in the Coq sources has been updated to list
    the new dependencies
    (`#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
continuously 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 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, David A. Dalrymple, Christian
Doczkal, Maxime Dénès, Andres Erbsen, Jim Fehrle, Emilio Jesus Gallego
Arias, Gaëtan Gilbert, Matěj Grabovský, Simon Gregersen, Jason Gross,
Samuel Gruetter, Hugo Herbelin, Jasper Hugunin, Mirai Ikebuchi,
Chantal Keller, Matej Košík, Sam Pablo Kuper, Vincent Laporte, Olivier
Laurent, Larry Darryl Lee Jr, Nick Lewycky, Yao Li, Yishuai Li, Assia
Mahboubi, Simon Marechal, Erik Martin-Dorel, Thierry Martinez,
Guillaume Melquiond, Kayla Ngan, Karl Palmskog, Pierre-Marie Pédrot,
Clément Pit-Claudel, 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,
Xia Li-yao, 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 [email protected] 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).

  - Allow inspecting custom grammar entries by :cmd:`Print Custom Grammar`
    (`#10061 <https://github.com/coq/coq/pull/10061>`_,
    fixes `#9681 <http://github.com/coq/coq/pull/9681>`_,
    by Jasper Hugunin, review by Pierre-Marie Pédrot and Hugo Herbelin).

- 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).

  - Modes are now taken into account by :tacn:`typeclasses eauto` for
    local hypotheses
    (`#9996 <https://github.com/coq/coq/pull/9996>`_,
    fixes `#5752 <https://github.com/coq/coq/issues/5752>`_,
    by Maxime Dénès, review by Pierre-Marie Pédrot).

  - New variant :tacn:`change_no_check` of :tacn:`change`, usable as a
    documented replacement of :tacn:`convert_concl_no_check`
    (`#10012 <https://github.com/coq/coq/pull/10012>`_,
    `#10017 <https://github.com/coq/coq/pull/10017>`_,
    `#10053 <https://github.com/coq/coq/pull/10053>`_, and
    `#10059 <https://github.com/coq/coq/pull/10059>`_,
    by Hugo Herbelin and Paolo G. Giarrusso).

  - The simplified value returned by :tacn:`field_simplify` is not
    always a fraction anymore.  When the denominator is :g:`1`, it
    returns :g:`x` while previously it was returning :g:`x/1`.  This
    change could break codes that were post-processing application of
    :tacn:`field_simplify` to get rid of these :g:`x/1`
    (`#9854 <https://github.com/coq/coq/pull/9854>`_,
    by Laurent Théry,
    with help from Michael Soegtrop, Maxime Dénès, and Vincent Laporte).

- 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).

  - `inE` now expands `y \in r x` when `r` is a `simpl_rel`.
    New `{pred T}` notation for a `pred T` alias in the `pred_sort` coercion
    class, simplified `predType` interface: `pred_class` and `mkPredType`
    deprecated, `{pred T}` and `PredType` should be used instead.
    `if c return t then ...` now expects `c` to be a variable bound in `t`.
    New `nonPropType` interface matching types that do _not_ have sort `Prop`.
    New `relpre R f` definition for the preimage of a relation R under f
    (`#9995 <https://github.com/coq/coq/pull/9995>`_, by Georges Gonthier).

- 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. The ambiguous paths messages have been
    turned to warnings, thus now they could appear in the output of ``coqc``.
    The convertibility checking procedure for coercion paths is complete for
    paths consisting of coercions satisfying the uniform inheritance condition,
    but some coercion paths could be reported as ambiguous even if they are
    convertible with existing ones when they have coercions that don't satisfy
    the uniform inheritance condition
    (`#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).

  - Added :g:`Coq.Structures.EqualitiesFacts.PairUsualDecidableTypeFull`
    (`#9984 <https://github.com/coq/coq/pull/9984>`_,
    by Jean-Christophe Léchenet and Oliver Nash).

- 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).

- Changelog has been moved from a specific file `CHANGES.md` to the
  reference manual; former Credits chapter of the reference manual has
  been split in two parts: a History chapter which was enriched with
  additional historical information about Coq versions 1 to 5, and a
  Changes chapter which was enriched with the content formerly in
  `CHANGES.md` and `COMPATIBILITY`
  (`#9133 <https://github.com/coq/coq/pull/9133>`_,
  `#9668 <https://github.com/coq/coq/pull/9668>`_,
  `#9939 <https://github.com/coq/coq/pull/9939>`_,
  `#9964 <https://github.com/coq/coq/pull/9964>`_,
  and `#10085 <https://github.com/coq/coq/pull/10085>`_,
  by Théo Zimmermann,
  with help and ideas from Emilio Jesús Gallego Arias, Gaëtan
  Gilbert, Clément Pit-Claudel, Matthieu Sozeau, and Enrico Tassi).

Changes in 8.10+beta2
~~~~~~~~~~~~~~~~~~~~~

Many bug fixes and documentation improvements, in particular:

**Tactics**

- Make the :tacn:`discriminate` tactic work together with
  :flag:`Universe Polymorphism` and equality in :g:`Type`. This,
  in particular, makes :tacn:`discriminate` compatible with the HoTT
  library https://github.com/HoTT/HoTT
  (`#10205 <https://github.com/coq/coq/pull/10205>`_,
  by Andreas Lynge, review by Pierre-Marie Pédrot and Matthieu Sozeau).

**SSReflect**

- Make the ``case E: t`` tactic work together with
  :flag:`Universe Polymorphism` and equality in :g:`Type`.
  This makes :tacn:`case <case (ssreflect)>` compatible with the HoTT
  library https://github.com/HoTT/HoTT
  (`#10302 <https://github.com/coq/coq/pull/10302>`_,
  fixes `#10301 <https://github.com/coq/coq/issues/10301>`_,
  by Andreas Lynge, review by Enrico Tassi)
- Make the ``rewrite /t`` tactic work together with
  :flag:`Universe Polymorphism`.
  This makes :tacn:`rewrite <rewrite (ssreflect)>` compatible with the HoTT
  library https://github.com/HoTT/HoTT
  (`#10305 <https://github.com/coq/coq/pull/10305>`_,
  fixes `#9336 <https://github.com/coq/coq/issues/9336>`_,
  by Andreas Lynge, review by Enrico Tassi)

**CoqIDE**

- Fix CoqIDE instability on Windows after the update to gtk3
  (`#10360 <https://github.com/coq/coq/pull/10360>`_, by Michael Soegtrop,
  closes `#9885 <https://github.com/coq/coq/issues/9885>`_).

**Miscellaneous**

- Proof General can now display Coq-generated diffs between proof steps
  in color
  (`#10019 <https://github.com/coq/coq/pull/10019>`_ and
  (in Proof General) `#421 <https://github.com/ProofGeneral/PG/pull/421>`_,
  by Jim Fehrle).

Changes in 8.10+beta3
~~~~~~~~~~~~~~~~~~~~~

**Kernel**

- Fix soundness issue with template polymorphism (`#9294
  <https://github.com/coq/coq/issues/9294>`_).

  Declarations of template-polymorphic inductive types ignored the
  provenance of the universes they were abstracting on and did not
  detect if they should be greater or equal to :math:`\Set` in
  general. Previous universes and universes introduced by the inductive
  definition could have constraints that prevented their instantiation
  with e.g. :math:`\Prop`, resulting in unsound instantiations later. The
  implemented fix only allows abstraction over universes introduced by
  the inductive declaration, and properly records all their constraints
  by making them by default only :math:`>= \Prop`. It is also checked
  that a template polymorphic inductive actually is polymorphic on at
  least one universe.

  This prevents inductive declarations in sections to be universe
  polymorphic over section parameters. For a backward compatible fix,
  simply hoist the inductive definition out of the section.
  An alternative is to declare the inductive as universe-polymorphic and
  cumulative in a universe-polymorphic section: all universes and
  constraints will be properly gathered in this case.
  See :ref:`Template-polymorphism` for a detailed exposition of the
  rules governing template-polymorphic types.

  To help users incrementally fix this issue, a command line option
  `-no-template-check` and a global flag :flag:`Template Check` are
  available to selectively disable the new check. Use at your own risk.

  (`#9918 <https://github.com/coq/coq/pull/9918>`_, by Matthieu Sozeau
  and Maxime Dénès).

**User messages**

- Improve the ambiguous paths warning to indicate which path is ambiguous with
  new one
  (`#10336 <https://github.com/coq/coq/pull/10336>`_,
  closes `#3219 <https://github.com/coq/coq/issues/3219>`_,
  by Kazuhiko Sakaguchi).

**Extraction**

- Fix extraction to OCaml of primitive machine integers;
  see :ref:`primitive-integers`
  (`#10430 <https://github.com/coq/coq/pull/10430>`_,
  fixes `#10361 <https://github.com/coq/coq/issues/10361>`_,
  by Vincent Laporte).
- Fix a printing bug of OCaml extraction on dependent record projections, which
  produced improper `assert false`. This change makes the OCaml extractor
  internally inline record projections by default; thus the monolithic OCaml
  extraction (:cmd:`Extraction` and :cmd:`Recursive Extraction`) does not
  produce record projection constants anymore except for record projections
  explicitly instructed to extract, and records declared in opaque modules
  (`#10577 <https://github.com/coq/coq/pull/10577>`_,
  fixes `#7348 <https://github.com/coq/coq/issues/7348>`_,
  by Kazuhiko Sakaguchi).

**Standard library**

- Added ``splitat`` function and lemmas about ``splitat`` and ``uncons``
  (`#9379 <https://github.com/coq/coq/pull/9379>`_,
  by Yishuai Li, with help of Konstantinos Kallas,
  follow-up of `#8365 <https://github.com/coq/coq/pull/8365>`_,
  which added ``uncons`` in 8.10+beta1).

Changes in 8.10.0
~~~~~~~~~~~~~~~~~

- Micromega tactics (:tacn:`lia`, :tacn:`nia`, etc) are no longer confused by
  primitive projections (`#10806 <https://github.com/coq/coq/pull/10806>`_,
  fixes `#9512 <https://github.com/coq/coq/issues/9512>`_
  by Vincent Laporte).

Changes in 8.10.1
~~~~~~~~~~~~~~~~~

A few bug fixes and documentation improvements, in particular:

**Kernel**

- Fix proof of False when using |SProp| (incorrect De Bruijn handling
  when inferring the relevance mark of a function) (`#10904
  <https://github.com/coq/coq/pull/10904>`_, by Pierre-Marie Pédrot).

**Tactics**

- Fix an anomaly when unsolved evar in :cmd:`Add Ring`
  (`#10891 <https://github.com/coq/coq/pull/10891>`_,
  fixes `#9851 <https://github.com/coq/coq/issues/9851>`_,
  by Gaëtan Gilbert).

**Tactic language**

- Fix Ltac regression in binding free names in uconstr
  (`#10899 <https://github.com/coq/coq/pull/10899>`_,
  fixes `#10894 <https://github.com/coq/coq/issues/10894>`_,
  by Hugo Herbelin).

**CoqIDE**

- Fix handling of unicode input before space
  (`#10852 <https://github.com/coq/coq/pull/10852>`_,
  fixes `#10842 <https://github.com/coq/coq/issues/10842>`_,
  by Arthur Charguéraud).

**Extraction**

- Fix custom extraction of inductives to JSON
  (`#10897 <https://github.com/coq/coq/pull/10897>`_,
  fixes `#4741 <https://github.com/coq/coq/issues/4741>`_,
  by Helge Bahmann).

Version 8.9
-----------

Summary of changes
~~~~~~~~~~~~~~~~~~

|Coq| version 8.9 contains the result of refinements and stabilization
of features and deprecations or removals of deprecated features,
cleanups of the internals of the system and API along with a few new
features. This release includes many user-visible changes, including
deprecations that are documented in the next subsection and new features that
are documented in the reference manual. Here are the most important
changes:

- Kernel: mutually recursive records are now supported, by Pierre-Marie
  Pédrot.

- Notations:

  - Support for autonomous grammars of terms called “custom entries”, by
    Hugo Herbelin (see Section :ref:`custom-entries` of the reference
    manual).

  - Deprecated notations of the standard library will be removed in the
    next version of |Coq|, see the 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
    numeral notations for custom types, by Daniel de Rauglaudre, Pierre
    Letouzey and Jason Gross.

- Tactics: Introduction tactics :tacn:`intro`/:tacn:`intros` on a goal that is an
  existential variable now force a refinement of the goal into a
  dependent product rather than failing, by Hugo Herbelin.

- Decision procedures: deprecation of tactic ``romega`` in favor of
  :tacn:`lia` and removal of ``fourier``, replaced by :tacn:`lra` which
  subsumes it, by Frédéric Besson, Maxime Dénès, Vincent Laporte and
  Laurent Théry.

- Proof language: focusing bracket ``{`` now supports named
  :ref:`goals <curly-braces>`, e.g. ``[x]:{`` will focus
  on a goal (existential variable) named ``x``, by Théo Zimmermann.

- SSReflect: the implementation of delayed clear was simplified by
  Enrico Tassi: the variables are always renamed using inaccessible
  names when the clear switch is processed and finally cleared at the
  end of the intro pattern. In addition to that, the use-and-discard flag
  ``{}`` typical of rewrite rules can now be also applied to views,
  e.g. ``=> {}/v`` applies ``v`` and then clears ``v``. See Section
  :ref:`introduction_ssr`.

- Vernacular:

  - Experimental support for :ref:`attributes <gallina-attributes>` on
    commands, by Vincent Laporte, as in ``#[local] Lemma foo : bar.``
    Tactics and tactic notations now support the ``deprecated``
    attribute.

  - Removed deprecated commands ``Arguments Scope`` and ``Implicit
    Arguments`` in favor of :cmd:`Arguments (scopes)` and
    :cmd:`Arguments (implicits)`, with the help of Jasper Hugunin.

  - New flag :flag:`Uniform Inductive Parameters` by Jasper Hugunin to
    avoid repeating uniform parameters in constructor declarations.

  - New commands :cmd:`Hint Variables` and :cmd:`Hint Constants`, by
    Matthieu Sozeau, for controlling the opacity status of variables and
    constants in hint databases. It is recommended to always use these
    commands after creating a hint database with :cmd:`Create HintDb`.

  - Multiple sections with the same name are now allowed, by Jasper
    Hugunin.

- Library: additions and changes in the ``VectorDef``, ``Ascii``, and
  ``String`` libraries. Syntax notations are now available only when using
  ``Import`` of libraries and not merely ``Require``, by various
  contributors (source of incompatibility, see 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.

- Documentation: we integrated a large number of fixes to the new Sphinx
  documentation by various contributors, coordinated by Clément
  Pit-Claudel and Théo Zimmermann.

- Tools: removed the ``gallina`` utility and the homebrewed ``Emacs`` mode.

- Packaging: as in |Coq| 8.8.2, the Windows installer now includes many
  more external packages that can be individually selected for
  installation, by Michael Soegtrop.

Version 8.9 also comes with a bunch of smaller-scale changes and
improvements regarding the different components of the system.  Most
important ones are documented in the next subsection file.

On the implementation side, the ``dev/doc/changes.md`` file documents
the numerous changes to the implementation and improvements of
interfaces. The file provides guidelines on porting a plugin to the new
version and a plugin development tutorial kept in sync with Coq was
introduced by Yves Bertot http://github.com/ybertot/plugin_tutorials.
The new ``dev/doc/critical-bugs`` file documents the known critical bugs
of |Coq| and affected releases.

The efficiency of the whole system has seen improvements thanks to
contributions from Gaëtan Gilbert, Pierre-Marie Pédrot, and Maxime Dénès.

Maxime Dénès, Emilio Jesús Gallego Arias, Gaëtan Gilbert, Michael
Soegtrop, Théo Zimmermann worked on maintaining and improving the
continuous integration system.

The OPAM repository for |Coq| packages has been maintained by Guillaume
Melquiond, Matthieu Sozeau, Enrico Tassi with contributions from many
users. A list of packages is available at https://coq.inria.fr/opam/www/.

The 54 contributors for this version are Léo Andrès, Rin Arakaki,
Benjamin Barenblat, Langston Barrett, Siddharth Bhat, Martin Bodin,
Simon Boulier, Timothy Bourke, Joachim Breitner, Tej Chajed, Arthur
Charguéraud, Pierre Courtieu, Maxime Dénès, Andres Erbsen, Jim Fehrle,
Julien Forest, Emilio Jesus Gallego Arias, Gaëtan Gilbert, Matěj
Grabovský, Jason Gross, Samuel Gruetter, Armaël Guéneau, Hugo Herbelin,
Jasper Hugunin, Ralf Jung, Sam Pablo Kuper, Ambroise Lafont, Leonidas
Lampropoulos, Vincent Laporte, Peter LeFanu Lumsdaine, Pierre Letouzey,
Jean-Christophe Léchenet, Nick Lewycky, Yishuai Li, Sven M. Hallberg,
Assia Mahboubi, Cyprien Mangin, Guillaume Melquiond, Perry E. Metzger,
Clément Pit-Claudel, Pierre-Marie Pédrot, Daniel R. Grayson, Kazuhiko
Sakaguchi, Michael Soegtrop, Matthieu Sozeau, Paul Steckler, Enrico
Tassi, Laurent Théry, Anton Trunov, whitequark, Théo Winterhalter,
Zeimer, Beta Ziliani, Théo Zimmermann.

Many power users helped to improve the design of the new features via
the issue and pull request system, the |Coq| development mailing list or
the [email protected] mailing list. It would be impossible to mention
exhaustively the names of everybody who to some extent influenced the
development.

Version 8.9 is the fourth release of |Coq| developed on a time-based
development cycle. Its development spanned 7 months from the release of
|Coq| 8.8. The development moved to a decentralized merging process
during this cycle. Guillaume Melquiond was in charge of the release
process and is the maintainer of this release. This release is the
result of ~2,000 commits and ~500 PRs merged, closing 75+ issues.

The |Coq| development team welcomed Vincent Laporte, a new |Coq|
engineer working with Maxime Dénès in the |Coq| consortium.

| Paris, November 2018,
| Matthieu Sozeau for the |Coq| development team
|

Details of changes in 8.9+beta1
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Kernel

- Mutually defined records are now supported.

Notations

- New support for autonomous grammars of terms, called "custom
  entries" (see chapter "Syntax extensions" of the reference manual).

- 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
  contains documentation on its usage in a comment at the top.

Tactics

- Added toplevel goal selector `!` which expects a single focused goal.
  Use with `Set Default Goal Selector` to force focusing before tactics
  are called.

- The undocumented "nameless" forms `fix N`, `cofix` that were
  deprecated in 8.8 have been removed from Ltac's syntax; please use
  `fix ident N/cofix ident` to explicitly name the (co)fixpoint
  hypothesis to be introduced.

- Introduction tactics `intro`/`intros` on a goal that is an
  existential variable now force a refinement of the goal into a
  dependent product rather than failing.

- Support for `fix`/`cofix` added in Ltac `match` and `lazymatch`.

- Ltac backtraces now include trace information about tactics
  called by OCaml-defined tactics.

- Option `Ltac Debug` now applies also to terms built using Ltac functions.

- Deprecated the `Implicit Tactic` family of commands.

- The default program obligation tactic uses a bounded proof search
  instead of an unbounded and potentially non-terminating one now
  (source of incompatibility).

- The `simple apply` tactic now respects the `Opaque` flag when called from
  Ltac (`auto` still does not respect it).

- Tactic `constr_eq` now adds universe constraints needed for the
  identity to the context (it used to ignore them). New tactic
  `constr_eq_strict` checks that the required constraints already hold
  without adding new ones. Preexisting tactic `constr_eq_nounivs` can
  still be used if you really want to ignore universe constraints.

- Tactics and tactic notations now understand the `deprecated` attribute.
- The `fourier` tactic has been removed. Please now use `lra` instead. You
  may need to add `Require Import Lra` to your developments. For compatibility,
  we now define `fourier` as a deprecated alias of `lra`.

- The `romega` tactics have been deprecated; please use `lia` instead.

Focusing

- Focusing bracket `{` now supports named goal selectors,
  e.g. `[x]: {` will focus on a goal (existential variable) named `x`.
  As usual, unfocus with `}` once the sub-goal is fully solved.

Specification language

- A fix to unification (which was sensitive to the ascii name of
  variables) may occasionally change type inference in incompatible
  ways, especially regarding the inference of the return clause of `match`.

Standard Library

- Added `Ascii.eqb` and `String.eqb` and the `=?` notation for them,
  and proved some lemmas about them.  Note that this might cause
  incompatibilities if you have, e.g., `string_scope` and `Z_scope` both
  open with `string_scope` on top, and expect `=?` to refer to `Z.eqb`.
  Solution: wrap `_ =? _` in `(_ =? _)%Z` (or whichever scope you
  want).

- Added `Ndigits.N2Bv_sized`, and proved some lemmas about it.
  Deprecated `Ndigits.N2Bv_gen`.

- The scopes `int_scope` and `uint_scope` have been renamed to
  `dec_int_scope` and `dec_uint_scope`, to clash less with ssreflect
  and other packages.  They are still delimited by `%int` and `%uint`.

- Syntax notations for `string`, `ascii`, `Z`, `positive`, `N`, `R`,
  and `int31` are no longer available merely by :cmd:`Require`\ing the files
  that define the inductives.  You must :cmd:`Import` `Coq.Strings.String.StringSyntax`
  (after `Require` `Coq.Strings.String`), `Coq.Strings.Ascii.AsciiSyntax` (after
  `Require` `Coq.Strings.Ascii`), `Coq.ZArith.BinIntDef`, `Coq.PArith.BinPosDef`,
  `Coq.NArith.BinNatDef`, `Coq.Reals.Rdefinitions`, and
  `Coq.Numbers.Cyclic.Int31.Int31`, respectively, to be able to use
  these notations.  Note that passing `-compat 8.8` or issuing
  `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
  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.
  Note also that this method is not fail-proof; you may have to adjust
  some scopes if you were relying on string notations not being
  available even when `string_scope` was open.)

- Numeral syntax for `nat` is no longer available without loading the
  entire prelude (`Require Import Coq.Init.Prelude`).  This only
  impacts users running Coq without the init library (`-nois` or
  `-noinit`) and also issuing `Require Import Coq.Init.Datatypes`.

Tools

- Coq_makefile lets one override or extend the following variables from
  the command line: `COQFLAGS`, `COQCHKFLAGS`, `COQDOCFLAGS`.
  `COQFLAGS` is now entirely separate from `COQLIBS`, so in custom Makefiles
  `$(COQFLAGS)` should be replaced by `$(COQFLAGS) $(COQLIBS)`.

- Removed the `gallina` utility (extracts specification from Coq vernacular files).
  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.
  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.

Vernacular Commands

- Removed deprecated commands `Arguments Scope` and `Implicit Arguments`
  (not the option). Use the `Arguments` command instead.
- Nested proofs may be enabled through the option `Nested Proofs Allowed`.
  By default, they are disabled and produce an error. The deprecation
  warning which used to occur when using nested proofs has been removed.
- Added option `Uniform Inductive Parameters` which abstracts over parameters
  before typechecking constructors, allowing to write for example
  `Inductive list (A : Type) := nil : list | cons : A -> list -> list.`
- New `Set Hint Variables/Constants Opaque/Transparent` commands for setting
  globally the opacity flag of variables and constants in hint databases,
  overwriting the opacity set of the hint database.
- Added generic syntax for "attributes"as in:
  `#[local] Lemma foo : bar.`
- Added the `Numeral Notation` command for registering decimal numeral
  notations for custom types
- The `Set SsrHave NoTCResolution` command no longer has special global
  scope. If you want the previous behavior, use `Global Set SsrHave
  NoTCResolution`.
- Multiple sections with the same name are allowed.

Coq binaries and process model

- Before 8.9, Coq distributed a single `coqtop` binary and a set of
  dynamically loadable plugins that used to take over the main loop
  for tasks such as IDE language server or parallel proof checking.

  These plugins have been turned into full-fledged binaries so each
  different process has associated a particular binary now, in
  particular `coqidetop` is the CoqIDE language server, and
  `coq{proof,tactic,query}worker` are in charge of task-specific and
  parallel proof checking.

SSReflect

- The implementation of delayed clear switches in intro patterns
  is now simpler to explain:

  1. The immediate effect of a clear switch like `{x}` is to rename the
     variable `x` to `_x_` (i.e. a reserved identifier that cannot be mentioned
     explicitly)
  2. The delayed effect of `{x}` is that `_x_` is cleared at the end of the intro
     pattern
  3. A clear switch immediately before a view application like `{x}/v` is
     translated to `/v{x}`.

  In particular, the third rule lets one write `{x}/v` even if `v` uses the variable `x`:
  indeed the view is executed before the renaming.

- An empty clear switch is now accepted in intro patterns before a
  view application whenever the view is a variable.
  One can now write `{}/v` to mean `{v}/v`.  Remark that `{}/x` is very similar
  to the idiom `{}e` for the rewrite tactic (the equation `e` is used for
  rewriting and then discarded).

Standard Library

- There are now conversions between `string` and `positive`, `Z`,
  `nat`, and `N` in binary, octal, and hex.

Display diffs between proof steps

- `coqtop` and `coqide` can now highlight the differences between proof steps
  in color. This can be enabled from the command line or the
  `Set Diffs "on"/"off"/"removed"` command. Please see the documentation for
  details.  Showing diffs in Proof General requires small changes to PG
  (under discussion).

Notations

- Added `++` infix for `VectorDef.append`.
  Note that this might cause incompatibilities if you have, e.g., `list_scope`
  and `vector_scope` both open with `vector_scope` on top, and expect `++` to
  refer to `app`.
  Solution: wrap `_ ++ _` in `(_ ++ _)%list` (or whichever scope you want).

Changes in 8.8.0
~~~~~~~~~~~~~~~~

Various bug fixes.

Changes in 8.8.1
~~~~~~~~~~~~~~~~

- Some quality-of-life fixes.
- Numerous improvements to the documentation.
- Fix a critical bug related to primitive projections and :tacn:`native_compute`.
- Ship several additional Coq libraries with the Windows installer.

Version 8.8
-----------

Summary of changes
~~~~~~~~~~~~~~~~~~

|Coq| version 8.8 contains the result of refinements and stabilization of
features and deprecations, cleanups of the internals of the system along
with a few new features. The main user visible changes are:

- Kernel: fix a subject reduction failure due to allowing fixpoints
  on non-recursive values, by Matthieu Sozeau.
  Handling of evars in the VM (the kernel still does not accept evars)
  by Pierre-Marie Pédrot.

- Notations: many improvements on recursive notations and support for
  destructuring patterns in the syntax of notations by Hugo Herbelin.

- Proof language: tacticals for profiling, timing and checking success
  or failure of tactics by Jason Gross. The focusing bracket ``{``
  supports single-numbered goal selectors, e.g. ``2:{``, by Théo
  Zimmermann.

- Vernacular: deprecation of commands and more uniform handling of the
  ``Local`` flag, by Vincent Laporte and Maxime Dénès, part of a larger
  attribute system overhaul. Experimental ``Show Extraction`` command by
  Pierre Letouzey. Coercion now accepts ``Prop`` or ``Type`` as a source
  by Arthur Charguéraud. ``Export`` modifier for options allowing to
  export the option to modules that ``Import`` and not only ``Require``
  a module, by Pierre-Marie Pédrot.

- Universes: many user-level and API level enhancements: qualified
  naming and printing, variance annotations for cumulative inductive
  types, more general constraints and enhancements of the minimization
  heuristics, interaction with modules by Gaëtan Gilbert, Pierre-Marie
  Pédrot and Matthieu Sozeau.

- Library: Decimal Numbers library by Pierre Letouzey and various small
  improvements.

- Documentation: a large community effort resulted in the migration
  of the reference manual to the Sphinx documentation tool. The result
  is this manual. The new documentation infrastructure (based on Sphinx)
  is by Clément Pit-Claudel. The migration was coordinated by Maxime Dénès
  and Paul Steckler, with some help of Théo Zimmermann during the
  final integration phase. The 14 people who ported the manual are
  Calvin Beck, Heiko Becker, Yves Bertot, Maxime Dénès, Richard Ford,
  Pierre Letouzey, Assia Mahboubi, Clément Pit-Claudel,
  Laurence Rideau, Matthieu Sozeau, Paul Steckler, Enrico Tassi,
  Laurent Théry, Nikita Zyuzin.

- Tools: experimental ``-mangle-names`` option to ``coqtop``/``coqc`` for
  linting proof scripts, by Jasper Hugunin.

On the implementation side, the ``dev/doc/changes.md`` file
documents the numerous changes to the implementation and improvements of
interfaces. The file provides guidelines on porting a plugin to the new
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 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
Matthieu Sozeau and performance issue tracking by Jason Gross and Paul
Steckler.

The official wiki and the bugtracker of |Coq| migrated to the GitHub
platform, thanks to the work of Pierre Letouzey and Théo
Zimmermann. Gaëtan Gilbert, Emilio Jesús Gallego Arias worked on
maintaining and improving the continuous integration system.

The OPAM repository for |Coq| packages has been maintained by Guillaume
Melquiond, Matthieu Sozeau, Enrico Tassi with contributions from many
users. A list of packages is available at https://coq.inria.fr/opam/www/.

The 44 contributors for this version are Yves Bertot, Joachim Breitner, Tej
Chajed, Arthur Charguéraud, Jacques-Pascal Deplaix, Maxime Dénès, Jim Fehrle,
Julien Forest, Yannick Forster, Gaëtan Gilbert, Jason Gross, Samuel Gruetter,
Thomas Hebb, Hugo Herbelin, Jasper Hugunin, Emilio Jesus Gallego Arias, Ralf
Jung, Johannes Kloos, Matej Košík, Robbert Krebbers, Tony Beta Lambda, Vincent
Laporte, Peter LeFanu Lumsdaine, Pierre Letouzey, Farzon Lotfi, Cyprien Mangin,
Guillaume Melquiond, Raphaël Monat, Carl Patenaude Poulin, Pierre-Marie Pédrot,
Clément Pit-Claudel, Matthew Ryan, Matt Quinn, Sigurd Schneider, Bernhard
Schommer, Michael Soegtrop, Matthieu Sozeau, Arnaud Spiwack, Paul Steckler,
Enrico Tassi, Anton Trunov, Martin Vassor, Vadim Zaliva and Théo Zimmermann.

Version 8.8 is the third release of |Coq| developed on a time-based
development cycle. Its development spanned 6 months from the release of
|Coq| 8.7 and was based on a public roadmap. The development process
was coordinated by Matthieu Sozeau. Maxime Dénès was in charge of the
release process. Théo Zimmermann is the maintainer of this release.

Many power users helped to improve the design of the new features via
the bug tracker, the pull request system, the |Coq| development mailing
list or the [email protected] mailing list. Special thanks to the users who
contributed patches and intensive brain-storming and code reviews,
starting with Jason Gross, Ralf Jung, Robbert Krebbers and Amin Timany.
It would however be impossible to mention exhaustively the names
of everybody who to some extent influenced the development.

The |Coq| consortium, an organization directed towards users and
supporters of the system, is now running and employs Maxime Dénès.
The contacts of the Coq Consortium are Yves Bertot and Maxime Dénès.

| Santiago de Chile, March 2018,
| Matthieu Sozeau for the |Coq| development team
|

Details of changes in 8.8+beta1
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Kernel

- Support for template polymorphism for definitions was removed. May trigger
  more "universe inconsistency" errors in rare occasions.
- Fixpoints are no longer allowed on non-recursive inductive types.

Notations

- Recursive notations with the recursive pattern repeating on the
  right (e.g. "( x ; .. ; y ; z )") now supported.
- Notations with a specific level for the leftmost nonterminal,
  when printing-only, are supported.
- Notations can now refer to the syntactic category of patterns (as in
  "fun 'pat =>" or "match p with pat => ... end"). Two variants are
  available, depending on whether a single variable is considered as a
  pattern or not.
- Recursive notations now support ".." patterns with several
  occurrences of the recursive term or binder, possibly mixing terms
  and binders, possibly in reverse left-to-right order.
"Locate" now working also on notations of the form "x + y" (rather
  than "_ + _").

Specification language

- When printing clauses of a "match", clauses with same right-hand
  side are factorized and the last most factorized clause with no
  variables, if it exists, is turned into a default clause.
  Use "Unset Printing Allow Default Clause" do deactivate printing
  of a default clause.
  Use "Unset Printing Factorizable Match Patterns" to deactivate
  factorization of clauses with same right-hand side.

Tactics

- On Linux, "native_compute" calls can be profiled using the "perf"
  utility. The command "Set NativeCompute Profiling" enables
  profiling, and "Set NativeCompute Profile Filename" customizes
  the profile filename.
- The tactic "omega" is now aware of the bodies of context variables
  such as "x := 5 : Z" (see #1362). This could be disabled via
  Unset Omega UseLocalDefs.
- The tactic "romega" is also aware now of the bodies of context variables.
- The tactic "zify" resp. "omega with N" is now aware of N.pred.
- Tactic "decide equality" now able to manage constructors which
  contain proofs.
- Added tactics reset ltac profile, show ltac profile (and variants)
- Added tactics restart_timer, finish_timing, and time_constr as an
  experimental way of timing Ltac's evaluation phase
- Added tactic optimize_heap, analogous to the Vernacular Optimize
  Heap, which performs a major garbage collection and heap compaction
  in the OCaml run-time system.
- The tactics "dtauto""dintuition""firstorder" now handle inductive types
  with let bindings in the parameters.
- The tactic ``dtauto`` now handles some inductives such as
  ``@sigT A (fun _ => B)`` as non-dependent conjunctions.
- A bug fixed in ``rewrite H in *`` and ``rewrite H in * |-`` may cause a
  few rare incompatibilities (it was unintendedly recursively
  rewriting in the side conditions generated by H).
- Added tactics "assert_succeeds tac" and "assert_fails tac" to ensure
  properties of the execution of a tactic without keeping the effect
  of the execution.
- `vm_compute` now supports existential variables.
- Calls to `shelve` and `give_up` within calls to tactic `refine` now working.
- Deprecated tactic `appcontext` was removed.

Focusing

- Focusing bracket `{` now supports single-numbered goal selector,
  e.g. `2: {` will focus on the second sub-goal. As usual, unfocus
  with `}` once the sub-goal is fully solved.
  The `Focus` and `Unfocus` commands are now deprecated.

Vernacular Commands

- Proofs ending in "Qed exporting ident, .., ident" are not supported
  anymore. Constants generated during `abstract` are kept private to the
  local environment.
- The deprecated Coercion Local, Open Local Scope, Notation Local syntax
  was removed. Use Local as a prefix instead.
- For the Extraction Language command, "OCaml" is spelled correctly.
  The older "Ocaml" is still accepted, but deprecated.
- Using “Require” inside a section is deprecated.
- An experimental command "Show Extraction" allows to extract the content
  of the current ongoing proof (grant wish #4129).
- Coercion now accepts the type of its argument to be "Prop" or "Type".
- The "Export" modifier can now be used when setting and unsetting options, and
  will result in performing the same change when the module corresponding the
  command is imported.
- The `Axiom` command does not automatically declare axioms as instances when
  their type is a class. Previous behavior can be restored using `Set
  Typeclasses Axioms Are Instances`.

Universes

Qualified naming of global universes now works like other namespaced
  objects (e.g. constants), with a separate namespace, inside and across
  module and library boundaries. Global universe names introduced in an
  inductive / constant / Let declaration get qualified with the name of
  the declaration.
- Universe cumulativity for inductive types is now specified as a
  variance for each polymorphic universe. See the reference manual for
  more information.
- Inference of universe constraints with cumulative inductive types
  produces more general constraints. Unsetting new option Cumulativity
  Weak Constraints produces even more general constraints (but may
  produce too many universes to be practical).
- Fix #5726: Notations that start with `Type` now support universe instances
  with `@{u}`.
- `with Definition` now understands universe declarations
  (like `@{u| Set < u}`).

Tools

- Coq can now be run with the option -mangle-names to change the auto-generated
  name scheme. This is intended to function as a linter for developments that
  want to be robust to changes in auto-generated names. This feature is experimental,
  and may change or disappear without warning.
- GeoProof support was removed.

Checker

- The checker now accepts filenames in addition to logical paths.

CoqIDE

- Find and Replace All report the number of occurrences found; Find indicates
  when it wraps.

coqdep

- Learned to read -I, -Q, -R and filenames from _CoqProject files.
  This is used by coq_makefile when generating dependencies for .v
  files (but not other files).

Documentation

- The Coq FAQ, formerly located at https://coq.inria.fr/faq, has been
  moved to the GitHub wiki section of this repository; the main entry
  page is https://github.com/coq/coq/wiki/The-Coq-FAQ.
- Documentation: a large community effort resulted in the migration
  of the reference manual to the Sphinx documentation tool. The result
  is partially integrated in this version.

Standard Library

- New libraries Coq.Init.Decimal, Coq.Numbers.DecimalFacts,
  Coq.Numbers.DecimalNat, Coq.Numbers.DecimalPos,
  Coq.Numbers.DecimalN, Coq.Numbers.DecimalZ,
  Coq.Numbers.DecimalString providing a type of decimal numbers, some
  facts about them, and conversions between decimal numbers and nat,
  positive, N, Z, and string.
- Added [Coq.Strings.String.concat] to concatenate a list of strings
  inserting a separator between each item
- Notation `'` for Zpos in QArith was removed.

- Some deprecated aliases are now emitting warnings when used.

Compatibility support

- Support for compatibility with versions before 8.6 was dropped.

Options

- The following deprecated options have been removed:

  + `Refolding Reduction`
  + `Standard Proposition Elimination`
  + `Dependent Propositions Elimination`
  + `Discriminate Introduction`
  + `Shrink Abstract`
  + `Tactic Pattern Unification`
  + `Intuition Iff Unfolding`
  + `Injection L2R Pattern Order`
  + `Record Elimination Schemes`
  + `Match Strict`
  + `Tactic Compat Context`
  + `Typeclasses Legacy Resolution`
  + `Typeclasses Module Eta`
  + `Typeclass Resolution After Apply`

Details of changes in 8.8.0
~~~~~~~~~~~~~~~~~~~~~~~~~~~

Tools

- Asynchronous proof delegation policy was fixed. Since version 8.7
  Coq was ignoring previous runs and the `-async-proofs-delegation-threshold`
  option did not have the expected behavior.

Tactic language

- The undocumented "nameless" forms `fix N`, `cofix` have been
  deprecated; please use `fix ident N /cofix ident` to explicitly
  name the (co)fixpoint hypothesis to be introduced.

Documentation

- The reference manual is now fully ported to Sphinx.

Other small deprecations and bug fixes.

Details of changes in 8.8.1
~~~~~~~~~~~~~~~~~~~~~~~~~~~

Kernel
--> --------------------

--> maximum size reached

--> --------------------

[ zur Elbe Produktseite wechseln0.304Quellennavigators  ]

                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik