From b531ef305a0dad301629cf9a51a1a4f0ff925297 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 23 Jun 2020 22:51:23 +0200
Subject: [declare] Allow custom typing flags when declaring constants.

We use the new `Declare.Info` structure to uniformly add properties to
the handling of constants. In this case, per-constant typing flags.

The internal code may want to see some further refactoring, including
pushing the flags down to `Safe_typing.add_constant` , but the changes
in the interface should be definitive.

This will allow #12539 and #9004 using attributes.
---
 doc/changelog/12-misc/12586-declare+typing_flags.rst | 5 +++++
 1 file changed, 5 insertions(+)
 create mode 100644 doc/changelog/12-misc/12586-declare+typing_flags.rst

(limited to 'doc')

diff --git a/doc/changelog/12-misc/12586-declare+typing_flags.rst b/doc/changelog/12-misc/12586-declare+typing_flags.rst
new file mode 100644
index 0000000000..001cd600b0
--- /dev/null
+++ b/doc/changelog/12-misc/12586-declare+typing_flags.rst
@@ -0,0 +1,5 @@
+- **Added:**
+  Typing flags can now be specified per-constant, this does allow
+  to fine-grain specify them from plugins or attributes.
+  (`#12586 <https://github.com/coq/coq/pull/12586>`_,
+  by Emilio Jesus Gallego Arias).
-- 
cgit v1.2.3


From 14150241cfd016c7f64974cc5c58bb116689f3c1 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 2 Jul 2020 18:17:24 +0200
Subject: [vernac] Allow to control typing flags with attributes.

The syntax is the one of boolean attributes, that is to say
`#[typing($flag={yes,no}]` where `$flag` is one of `guarded`,
`universes`, `positive`.

We had to instrument the pretyper in a few places, it is interesting
that it is doing so many checks.
---
 .../12-misc/12586-declare+typing_flags.rst         |  5 +++--
 doc/sphinx/language/core/inductive.rst             | 26 +++++++++-------------
 doc/sphinx/proof-engine/vernacular-commands.rst    | 15 +++++++++++++
 3 files changed, 29 insertions(+), 17 deletions(-)

(limited to 'doc')

diff --git a/doc/changelog/12-misc/12586-declare+typing_flags.rst b/doc/changelog/12-misc/12586-declare+typing_flags.rst
index 001cd600b0..bd4e6f401d 100644
--- a/doc/changelog/12-misc/12586-declare+typing_flags.rst
+++ b/doc/changelog/12-misc/12586-declare+typing_flags.rst
@@ -1,5 +1,6 @@
 - **Added:**
-  Typing flags can now be specified per-constant, this does allow
-  to fine-grain specify them from plugins or attributes.
+  Typing flags can now be specified per-constant / inductive, this
+  allows to fine-grain specify them from plugins or attributes. See
+  the reference manual for details on attribute syntax.
   (`#12586 <https://github.com/coq/coq/pull/12586>`_,
   by Emilio Jesus Gallego Arias).
diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst
index 9fda2ab1fa..f277997094 100644
--- a/doc/sphinx/language/core/inductive.rst
+++ b/doc/sphinx/language/core/inductive.rst
@@ -31,8 +31,8 @@ Inductive types
    proposition).
 
    This command supports the :attr:`universes(polymorphic)`,
-   :attr:`universes(template)`, :attr:`universes(cumulative)`, and
-   :attr:`private(matching)` attributes.
+   :attr:`universes(template)`, :attr:`universes(cumulative)`,
+   :attr:`typing(positive)`, and :attr:`private(matching)` attributes.
 
    Mutually inductive types can be defined by including multiple :n:`@inductive_definition`\s.
    The :n:`@ident`\s are simultaneously added to the environment before the types of constructors are checked.
@@ -49,10 +49,12 @@ Inductive types
 
    .. exn:: Non strictly positive occurrence of @ident in @type.
 
-      The types of the constructors have to satisfy a *positivity condition*
-      (see Section :ref:`positivity`). This condition ensures the soundness of
-      the inductive definition. The positivity checking can be disabled using
-      the :flag:`Positivity Checking` flag (see :ref:`controlling-typing-flags`).
+      The types of the constructors have to satisfy a *positivity
+      condition* (see Section :ref:`positivity`). This condition
+      ensures the soundness of the inductive definition. The
+      positivity checking can be disabled using the :flag:`Positivity
+      Checking` flag or the :attr:`typing(positive)` attribute (see
+      :ref:`controlling-typing-flags`).
 
    .. exn:: The conclusion of @type is not valid; it must be built from @ident.
 
@@ -848,9 +850,7 @@ between universes for inductive types in the Type hierarchy.
 
    .. coqtop:: none
 
-      Unset Positivity Checking.
-      Inductive I : Prop := not_I_I (not_I : I -> False) : I.
-      Set Positivity Checking.
+      #[typing(positive=no)] Inductive I : Prop := not_I_I (not_I : I -> False) : I.
 
    .. coqtop:: all
 
@@ -884,9 +884,7 @@ between universes for inductive types in the Type hierarchy.
 
    .. coqtop:: none
 
-      Unset Positivity Checking.
-      Inductive Lam := lam (_ : Lam -> Lam).
-      Set Positivity Checking.
+      #[typing(positive=no)] Inductive Lam := lam (_ : Lam -> Lam).
 
    .. coqtop:: all
 
@@ -915,9 +913,7 @@ between universes for inductive types in the Type hierarchy.
 
    .. coqtop:: none
 
-      Unset Positivity Checking.
-      Inductive A: Type := introA: ((A -> Prop) -> Prop) -> A.
-      Set Positivity Checking.
+      #[typing(positive=no)] Inductive A: Type := introA: ((A -> Prop) -> Prop) -> A.
 
    .. coqtop:: all
 
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index e7db9cfaca..b8160b7966 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -1152,6 +1152,11 @@ Controlling Typing Flags
    anymore but it still affects the reduction of the term. Unchecked fixpoints are
    printed by :cmd:`Print Assumptions`.
 
+.. attr:: typing(guarded)
+
+   Similar to :flag:`Guard Checking`, but on a per-declaration
+   basis. Takes ``yes/no`` as parameters, i.e. ``typing(guarded=no)``.
+
 .. flag:: Positivity Checking
 
    This flag can be used to enable/disable the positivity checking of inductive
@@ -1159,6 +1164,11 @@ Controlling Typing Flags
    break the consistency of the system, use at your own risk. Unchecked
    (co)inductive types are printed by :cmd:`Print Assumptions`.
 
+.. attr:: typing(positive)
+
+   Similar to :flag:`Positivity Checking`, but on a per-declaration basis.
+   Takes ``yes/no`` as parameters, i.e. ``typing(positive=no)``.
+
 .. flag:: Universe Checking
 
    This flag can be used to enable/disable the checking of universes, providing a
@@ -1167,6 +1177,11 @@ Controlling Typing Flags
    :cmd:`Print Assumptions`. It has the same effect as `-type-in-type` command line
    argument (see :ref:`command-line-options`).
 
+.. attr:: typing(universes)
+
+   Similar to :flag:`Universe Checking`, but on a per-declaration basis.
+   Takes ``yes/no`` as parameters, i.e. ``typing(universes=no)``.
+
 .. cmd:: Print Typing Flags
 
    Print the status of the three typing flags: guard checking, positivity checking
-- 
cgit v1.2.3


From 50af46a596af607493ce46da782389e8a82e8354 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 18 Nov 2020 23:25:17 +0100
Subject: [attributes] [doc] Documentation review by Théo.

Co-authored-by: <Théo Zimmermann <theo.zimmermann@inria.fr>
---
 doc/changelog/12-misc/12586-declare+typing_flags.rst |  2 +-
 doc/sphinx/language/core/coinductive.rst             |  3 ++-
 doc/sphinx/language/core/definitions.rst             |  8 +++++---
 doc/sphinx/language/core/inductive.rst               | 10 ++++++----
 doc/sphinx/proof-engine/vernacular-commands.rst      | 15 +++++++++------
 5 files changed, 23 insertions(+), 15 deletions(-)

(limited to 'doc')

diff --git a/doc/changelog/12-misc/12586-declare+typing_flags.rst b/doc/changelog/12-misc/12586-declare+typing_flags.rst
index bd4e6f401d..52915ceee9 100644
--- a/doc/changelog/12-misc/12586-declare+typing_flags.rst
+++ b/doc/changelog/12-misc/12586-declare+typing_flags.rst
@@ -1,6 +1,6 @@
 - **Added:**
   Typing flags can now be specified per-constant / inductive, this
   allows to fine-grain specify them from plugins or attributes. See
-  the reference manual for details on attribute syntax.
+  :ref:`controlling-typing-flags` for details on attribute syntax.
   (`#12586 <https://github.com/coq/coq/pull/12586>`_,
   by Emilio Jesus Gallego Arias).
diff --git a/doc/sphinx/language/core/coinductive.rst b/doc/sphinx/language/core/coinductive.rst
index 43bbc8b40d..e9737f8712 100644
--- a/doc/sphinx/language/core/coinductive.rst
+++ b/doc/sphinx/language/core/coinductive.rst
@@ -27,7 +27,8 @@ More information on co-inductive definitions can be found in
 
    This command supports the :attr:`universes(polymorphic)`,
    :attr:`universes(template)`, :attr:`universes(cumulative)`,
-   :attr:`private(matching)`, and :attr:`using` attributes.
+   :attr:`private(matching)`, :attr:`typing(universes)`,
+   :attr:`typing(positive)`, and :attr:`using` attributes.
 
 .. example::
 
diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst
index 57771c9036..95bb1b0e0c 100644
--- a/doc/sphinx/language/core/definitions.rst
+++ b/doc/sphinx/language/core/definitions.rst
@@ -90,8 +90,9 @@ Section :ref:`typing-rules`.
    computation on :n:`@term`.
 
    These commands also support the :attr:`universes(polymorphic)`,
-   :attr:`program` (see :ref:`program_definition`),
-   :attr:`canonical` and :attr:`using` attributes.
+   :attr:`program` (see :ref:`program_definition`), :attr:`canonical`,
+   :attr:`typing(universes)`, :attr:`typing(guarded)`, and
+   :attr:`using` attributes.
 
    If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode.
    This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic.
@@ -162,7 +163,8 @@ Chapter :ref:`Tactics`. The basic assertion command is:
    correct at some time of the interactive development of a proof, use the
    command :cmd:`Guarded`.
 
-   This command accepts the :attr:`using` attribute.
+   This command accepts the :attr:`typing(universes)`,
+   :attr:`typing(guarded)`, and :attr:`using` attributes.
 
    .. exn:: The term @term has type @type which should be Set, Prop or Type.
       :undocumented:
diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst
index f277997094..86de059f28 100644
--- a/doc/sphinx/language/core/inductive.rst
+++ b/doc/sphinx/language/core/inductive.rst
@@ -32,7 +32,8 @@ Inductive types
 
    This command supports the :attr:`universes(polymorphic)`,
    :attr:`universes(template)`, :attr:`universes(cumulative)`,
-   :attr:`typing(positive)`, and :attr:`private(matching)` attributes.
+   :attr:`typing(positive)`, :attr:`typing(universes)`, and
+   :attr:`private(matching)` attributes.
 
    Mutually inductive types can be defined by including multiple :n:`@inductive_definition`\s.
    The :n:`@ident`\s are simultaneously added to the environment before the types of constructors are checked.
@@ -51,8 +52,8 @@ Inductive types
 
       The types of the constructors have to satisfy a *positivity
       condition* (see Section :ref:`positivity`). This condition
-      ensures the soundness of the inductive definition. The
-      positivity checking can be disabled using the :flag:`Positivity
+      ensures the soundness of the inductive definition.
+      Positivity checking can be disabled using the :flag:`Positivity
       Checking` flag or the :attr:`typing(positive)` attribute (see
       :ref:`controlling-typing-flags`).
 
@@ -392,7 +393,8 @@ constructions.
    consequently :n:`forall {* @binder }, @type` and its value is equivalent
    to :n:`fun {* @binder } => @term`.
 
-   This command accepts the :attr:`program` attribute.
+   This command accepts the :attr:`program`,
+   :attr:`typing(universes)`, and :attr:`typing(guarded)` attributes.
 
    To be accepted, a :cmd:`Fixpoint` definition has to satisfy syntactical
    constraints on a special argument called the decreasing argument. They
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index b8160b7966..08534c9e07 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -1152,10 +1152,11 @@ Controlling Typing Flags
    anymore but it still affects the reduction of the term. Unchecked fixpoints are
    printed by :cmd:`Print Assumptions`.
 
-.. attr:: typing(guarded)
+.. attr:: typing(guarded{? = {| yes | no } })
+   :name: typing(guarded)
 
    Similar to :flag:`Guard Checking`, but on a per-declaration
-   basis. Takes ``yes/no`` as parameters, i.e. ``typing(guarded=no)``.
+   basis. Disable guard checking locally with ``typing(guarded=no)``.
 
 .. flag:: Positivity Checking
 
@@ -1164,10 +1165,11 @@ Controlling Typing Flags
    break the consistency of the system, use at your own risk. Unchecked
    (co)inductive types are printed by :cmd:`Print Assumptions`.
 
-.. attr:: typing(positive)
+.. attr:: typing(positive{? = {| yes | no } })
+   :name: typing(positive)
 
    Similar to :flag:`Positivity Checking`, but on a per-declaration basis.
-   Takes ``yes/no`` as parameters, i.e. ``typing(positive=no)``.
+   Disable positivity checking locally with ``typing(positive=no)``.
 
 .. flag:: Universe Checking
 
@@ -1177,10 +1179,11 @@ Controlling Typing Flags
    :cmd:`Print Assumptions`. It has the same effect as `-type-in-type` command line
    argument (see :ref:`command-line-options`).
 
-.. attr:: typing(universes)
+.. attr:: typing(universes{? = {| yes | no } })
+   :name: typing(universes)
 
    Similar to :flag:`Universe Checking`, but on a per-declaration basis.
-   Takes ``yes/no`` as parameters, i.e. ``typing(universes=no)``.
+   Disable universe checking locally with ``typing(universe=no)``.
 
 .. cmd:: Print Typing Flags
 
-- 
cgit v1.2.3


From 1f0f1ae93f757be8101d598f8aaf5b564bde9dcd Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 26 Nov 2020 21:32:37 +0100
Subject: [attributes] [typing] Rename `typing` to `bypass_check`

As discussed in the Coq meeting.
---
 doc/sphinx/language/core/coinductive.rst        |  4 ++--
 doc/sphinx/language/core/definitions.rst        |  6 +++---
 doc/sphinx/language/core/inductive.rst          | 12 ++++++------
 doc/sphinx/proof-engine/vernacular-commands.rst | 18 +++++++++---------
 4 files changed, 20 insertions(+), 20 deletions(-)

(limited to 'doc')

diff --git a/doc/sphinx/language/core/coinductive.rst b/doc/sphinx/language/core/coinductive.rst
index e9737f8712..cf46580bdb 100644
--- a/doc/sphinx/language/core/coinductive.rst
+++ b/doc/sphinx/language/core/coinductive.rst
@@ -27,8 +27,8 @@ More information on co-inductive definitions can be found in
 
    This command supports the :attr:`universes(polymorphic)`,
    :attr:`universes(template)`, :attr:`universes(cumulative)`,
-   :attr:`private(matching)`, :attr:`typing(universes)`,
-   :attr:`typing(positive)`, and :attr:`using` attributes.
+   :attr:`private(matching)`, :attr:`bypass_check(universes)`,
+   :attr:`bypass_check(positivity)`, and :attr:`using` attributes.
 
 .. example::
 
diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst
index 95bb1b0e0c..76aa543b8b 100644
--- a/doc/sphinx/language/core/definitions.rst
+++ b/doc/sphinx/language/core/definitions.rst
@@ -91,7 +91,7 @@ Section :ref:`typing-rules`.
 
    These commands also support the :attr:`universes(polymorphic)`,
    :attr:`program` (see :ref:`program_definition`), :attr:`canonical`,
-   :attr:`typing(universes)`, :attr:`typing(guarded)`, and
+   :attr:`bypass_check(universes)`, :attr:`bypass_check(guard)`, and
    :attr:`using` attributes.
 
    If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode.
@@ -163,8 +163,8 @@ Chapter :ref:`Tactics`. The basic assertion command is:
    correct at some time of the interactive development of a proof, use the
    command :cmd:`Guarded`.
 
-   This command accepts the :attr:`typing(universes)`,
-   :attr:`typing(guarded)`, and :attr:`using` attributes.
+   This command accepts the :attr:`bypass_check(universes)`,
+   :attr:`bypass_check(guard)`, and :attr:`using` attributes.
 
    .. exn:: The term @term has type @type which should be Set, Prop or Type.
       :undocumented:
diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst
index 86de059f28..4bee7cc1b1 100644
--- a/doc/sphinx/language/core/inductive.rst
+++ b/doc/sphinx/language/core/inductive.rst
@@ -32,7 +32,7 @@ Inductive types
 
    This command supports the :attr:`universes(polymorphic)`,
    :attr:`universes(template)`, :attr:`universes(cumulative)`,
-   :attr:`typing(positive)`, :attr:`typing(universes)`, and
+   :attr:`bypass_check(positivity)`, :attr:`bypass_check(universes)`, and
    :attr:`private(matching)` attributes.
 
    Mutually inductive types can be defined by including multiple :n:`@inductive_definition`\s.
@@ -54,7 +54,7 @@ Inductive types
       condition* (see Section :ref:`positivity`). This condition
       ensures the soundness of the inductive definition.
       Positivity checking can be disabled using the :flag:`Positivity
-      Checking` flag or the :attr:`typing(positive)` attribute (see
+      Checking` flag or the :attr:`bypass_check(positivity)` attribute (see
       :ref:`controlling-typing-flags`).
 
    .. exn:: The conclusion of @type is not valid; it must be built from @ident.
@@ -394,7 +394,7 @@ constructions.
    to :n:`fun {* @binder } => @term`.
 
    This command accepts the :attr:`program`,
-   :attr:`typing(universes)`, and :attr:`typing(guarded)` attributes.
+   :attr:`bypass_check(universes)`, and :attr:`bypass_check(guard)` attributes.
 
    To be accepted, a :cmd:`Fixpoint` definition has to satisfy syntactical
    constraints on a special argument called the decreasing argument. They
@@ -852,7 +852,7 @@ between universes for inductive types in the Type hierarchy.
 
    .. coqtop:: none
 
-      #[typing(positive=no)] Inductive I : Prop := not_I_I (not_I : I -> False) : I.
+      #[bypass_check(positivity)] Inductive I : Prop := not_I_I (not_I : I -> False) : I.
 
    .. coqtop:: all
 
@@ -886,7 +886,7 @@ between universes for inductive types in the Type hierarchy.
 
    .. coqtop:: none
 
-      #[typing(positive=no)] Inductive Lam := lam (_ : Lam -> Lam).
+      #[bypass_check(positivity)] Inductive Lam := lam (_ : Lam -> Lam).
 
    .. coqtop:: all
 
@@ -915,7 +915,7 @@ between universes for inductive types in the Type hierarchy.
 
    .. coqtop:: none
 
-      #[typing(positive=no)] Inductive A: Type := introA: ((A -> Prop) -> Prop) -> A.
+      #[bypass_check(positivity)] Inductive A: Type := introA: ((A -> Prop) -> Prop) -> A.
 
    .. coqtop:: all
 
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 08534c9e07..e866e4c624 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -1152,11 +1152,11 @@ Controlling Typing Flags
    anymore but it still affects the reduction of the term. Unchecked fixpoints are
    printed by :cmd:`Print Assumptions`.
 
-.. attr:: typing(guarded{? = {| yes | no } })
-   :name: typing(guarded)
+.. attr:: bypass_check(guard{? = {| yes | no } })
+   :name: bypass_check(guard)
 
    Similar to :flag:`Guard Checking`, but on a per-declaration
-   basis. Disable guard checking locally with ``typing(guarded=no)``.
+   basis. Disable guard checking locally with ``bypass_check(guard)``.
 
 .. flag:: Positivity Checking
 
@@ -1165,11 +1165,11 @@ Controlling Typing Flags
    break the consistency of the system, use at your own risk. Unchecked
    (co)inductive types are printed by :cmd:`Print Assumptions`.
 
-.. attr:: typing(positive{? = {| yes | no } })
-   :name: typing(positive)
+.. attr:: bypass_check(positivity{? = {| yes | no } })
+   :name: bypass_check(positivity)
 
    Similar to :flag:`Positivity Checking`, but on a per-declaration basis.
-   Disable positivity checking locally with ``typing(positive=no)``.
+   Disable positivity checking locally with ``bypass_check(positivity)``.
 
 .. flag:: Universe Checking
 
@@ -1179,11 +1179,11 @@ Controlling Typing Flags
    :cmd:`Print Assumptions`. It has the same effect as `-type-in-type` command line
    argument (see :ref:`command-line-options`).
 
-.. attr:: typing(universes{? = {| yes | no } })
-   :name: typing(universes)
+.. attr:: bypass_check(universes{? = {| yes | no } })
+   :name: bypass_check(universes)
 
    Similar to :flag:`Universe Checking`, but on a per-declaration basis.
-   Disable universe checking locally with ``typing(universe=no)``.
+   Disable universe checking locally with ``bypass_check(universes)``.
 
 .. cmd:: Print Typing Flags
 
-- 
cgit v1.2.3