diff options
| author | Théo Zimmermann | 2019-12-02 08:43:38 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-12-02 08:58:28 +0100 |
| commit | 68bdefae23d4175b523f4857faab254d9902083c (patch) | |
| tree | 3a51f9f4451744eff49f684928bf14e7be755459 | |
| parent | a03543efc3ab66a846f392ea87897f7354c5a547 (diff) | |
Highlight refine attribute for Instance.
| -rw-r--r-- | doc/sphinx/changes.rst | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index f221f0ed7d..47899ea1ed 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -32,6 +32,8 @@ The main changes brought by |Coq| version 8.11 are: dependencies. - New :g:`Arguments` annotation for `bidirectional type inference`__ configuration for reference (e.g. constants, inductive) applications. +- New `refine attribute`__ for :cmd:`Instance` can be used instead of + the removed ``Refine Instance Mode``. - Generalization of the :g:`under` and :g:`over` tactics__ of SSReflect to arbitrary relations. - `Revision`__ of the :g:`Coq.Reals` library, its axiomatisation and @@ -44,6 +46,7 @@ __ 811UnsafeFlags_ __ 811ExportBug_ __ 811vos_ __ 811BidirArguments_ +__ 811RefineInstance_ __ 811SSRUnderOver_ __ 811Reals_ @@ -194,6 +197,9 @@ Changes in 8.11+beta1 :cmd:`Arguments <Arguments (implicits)>` command instead of the human-targeted prose used in previous Coq versions. (`#10985 <https://github.com/coq/coq/pull/10985>`_, by Gaëtan Gilbert). + + .. _811RefineInstance: + - **Added:** ``#[refine]`` attribute for :cmd:`Instance`, a more predictable version of the old ``Refine Instance Mode`` which unconditionally opens a proof (`#10996 |