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

1 files changed, 15 insertions, 0 deletions

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