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/proof-engine/vernacular-commands.rst | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

(limited to 'doc/sphinx/proof-engine')

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