diff options
Diffstat (limited to 'doc')
6 files changed, 62 insertions, 5 deletions
diff --git a/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst b/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst new file mode 100644 index 0000000000..d95f554766 --- /dev/null +++ b/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst @@ -0,0 +1,17 @@ +- **Fixed:** Parsing and printing consistently handle inheritance of implicit + arguments in notations. With the exception of notations of + the form :n:`Notation @string := @@qualid` and :n:`Notation @ident := @@qualid` which + inhibit implicit arguments, all notations binding a partially + applied constant, as e.g. in :n:`Notation @string := (@qualid {+ @arg })`, + or :n:`Notation @string := (@@qualid {+ @arg })`, or + :n:`Notation @ident := (@qualid {+ @arg })`, or :n:`Notation @ident + := (@@qualid {+ @arg })`, inherit the remaining implicit arguments + (`#11120 <https://github.com/coq/coq/pull/11120>`_, by Hugo + Herbelin, fixing `#4690 <https://github.com/coq/coq/pull/4690>`_ and + `#11091 <https://github.com/coq/coq/pull/11091>`_). + +- **Changed:** Interpretation scopes are now always inherited in + notations binding a partially applied constant, including for + notations binding an expression of the form :n:`@@qualid`. The latter was + not the case beforehand + (part of `#11120 <https://github.com/coq/coq/pull/11120>`_). diff --git a/doc/changelog/07-commands-and-options/11663-remove-polymorphic-unqualified.rst b/doc/changelog/07-commands-and-options/11663-remove-polymorphic-unqualified.rst new file mode 100644 index 0000000000..1f8dcd3992 --- /dev/null +++ b/doc/changelog/07-commands-and-options/11663-remove-polymorphic-unqualified.rst @@ -0,0 +1,5 @@ +- **Removed:** + Unqualified ``polymorphic``, ``monomorphic``, ``template``, + ``notemplate`` attributes (they were deprecated since Coq 8.10). + Use them as sub-attributes of the ``universes`` attribute (`#11663 + <https://github.com/coq/coq/pull/11663>`_, by Théo Zimmermann). diff --git a/doc/changelog/10-standard-library/11686-fix-int-notations.rst b/doc/changelog/10-standard-library/11686-fix-int-notations.rst new file mode 100644 index 0000000000..cc820c5a25 --- /dev/null +++ b/doc/changelog/10-standard-library/11686-fix-int-notations.rst @@ -0,0 +1,6 @@ +- **Changed:** + Notations :n:`[|@term|]` and :n:`[||@term||]` for morphisms from 63-bit + integers to :g:`Z` and :g:`zn2z int` have been removed in favor of + :n:`φ(@term)` and :n:`Φ(@term)` respectively. These notations were + breaking Ltac parsing. (`#11686 <https://github.com/coq/coq/pull/11686>`_, + by Maxime Dénès). diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index f1dd7479c5..77cb3ecc21 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -108,7 +108,7 @@ master_doc = "index" # General information about the project. project = 'Coq' -copyright = '1999-2019, Inria, CNRS and contributors' +copyright = '1999-2020, Inria, CNRS and contributors' author = 'The Coq Development Team' # The version info for the project you're documenting, acts as replacement for diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index b722b1af74..9362a7729e 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -3,10 +3,6 @@ Ltac2 ===== -.. coqtop:: none - - From Ltac2 Require Import Ltac2. - The Ltac tactic language is probably one of the ingredients of the success of Coq, yet it is at the same time its Achilles' heel. Indeed, Ltac: @@ -88,6 +84,12 @@ which allows to ensure that Ltac2 satisfies the same equations as a generic ML with unspecified effects would do, e.g. function reduction is substitution by a value. +To import Ltac2, use the following command: + +.. coqtop:: in + + From Ltac2 Require Import Ltac2. + Type Syntax ~~~~~~~~~~~ diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 22754e57d4..c568f13c12 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -422,6 +422,27 @@ identifiers or tokens starting with a single quote are dropped. Locate "exists". Locate "exists _ .. _ , _". +Inheritance of the properties of arguments of constants bound to a notation +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +If the right-hand side of a notation is a partially applied constant, +the notation inherits the implicit arguments (see +:ref:`ImplicitArguments`) and interpretation scopes (see +:ref:`Scopes`) of the constant. For instance: + +.. coqtop:: in reset + + Record R := {dom : Type; op : forall {A}, A -> dom}. + Notation "# x" := (@op x) (at level 8). + +.. coqtop:: all + + Check fun x:R => # x 3. + +As an exception, if the right-hand side is just of the form +:n:`@@qualid`, this conventionally stops the inheritance of implicit +arguments (but not of interpretation scopes). + Notations and binders ~~~~~~~~~~~~~~~~~~~~~ @@ -1420,6 +1441,12 @@ Abbreviations denoted expression is performed at definition time. Type checking is done only at the time of use of the abbreviation. + Like for notations, if the right-hand side of an abbreviation is a + partially applied constant, the abbreviation inherits the implicit + arguments and interpretation scopes of the constant. As an + exception, if the right-hand side is just of the form :n:`@@qualid`, + this conventionally stops the inheritance of implicit arguments. + .. _numeral-notations: Numeral notations |