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: --- doc/sphinx/language/core/coinductive.rst | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'doc/sphinx/language/core/coinductive.rst') 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:: -- 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 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'doc/sphinx/language/core/coinductive.rst') 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:: -- cgit v1.2.3