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/language/core/definitions.rst | |
| parent | 50af46a596af607493ce46da782389e8a82e8354 (diff) | |
[attributes] [typing] Rename `typing` to `bypass_check`
As discussed in the Coq meeting.
Diffstat (limited to 'doc/sphinx/language/core/definitions.rst')
| -rw-r--r-- | doc/sphinx/language/core/definitions.rst | 6 |
1 files changed, 3 insertions, 3 deletions
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: |