diff options
| author | Emilio Jesus Gallego Arias | 2020-11-26 21:32:37 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-11-26 22:08:01 +0100 |
| commit | 1f0f1ae93f757be8101d598f8aaf5b564bde9dcd (patch) | |
| tree | 5afe9610e6412cf6e15bd3e158f04e32bd2d17e2 /doc/sphinx/proof-engine | |
| parent | 50af46a596af607493ce46da782389e8a82e8354 (diff) | |
[attributes] [typing] Rename `typing` to `bypass_check`
As discussed in the Coq meeting.
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 18 |
1 files changed, 9 insertions, 9 deletions
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 |