diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/language/core/coinductive.rst | 3 | ||||
| -rw-r--r-- | doc/sphinx/language/core/definitions.rst | 11 | ||||
| -rw-r--r-- | doc/sphinx/language/core/inductive.rst | 28 | ||||
| -rw-r--r-- | doc/sphinx/language/extensions/arguments-command.rst | 14 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 18 | ||||
| -rw-r--r-- | doc/sphinx/proofs/writing-proofs/rewriting.rst | 7 |
6 files changed, 61 insertions, 20 deletions
diff --git a/doc/sphinx/language/core/coinductive.rst b/doc/sphinx/language/core/coinductive.rst index 43bbc8b40d..cf46580bdb 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:`bypass_check(universes)`, + :attr:`bypass_check(positivity)`, and :attr:`using` attributes. .. example:: diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst index 57771c9036..ec5b896dab 100644 --- a/doc/sphinx/language/core/definitions.rst +++ b/doc/sphinx/language/core/definitions.rst @@ -90,8 +90,9 @@ Section :ref:`typing-rules`. computation on :n:`@term`. These commands also support the :attr:`universes(polymorphic)`, - :attr:`program` (see :ref:`program_definition`), - :attr:`canonical` and :attr:`using` attributes. + :attr:`program` (see :ref:`program_definition`), :attr:`canonical`, + :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. This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic. @@ -162,7 +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:`using` attribute. + 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: @@ -173,7 +175,8 @@ Chapter :ref:`Tactics`. The basic assertion command is: The name you provided is already defined. You have then to choose another name. - .. exn:: Nested proofs are not allowed unless you turn the Nested Proofs Allowed flag on. + .. exn:: Nested proofs are discouraged and not allowed by default. This error probably means that you forgot to close the last "Proof." with "Qed." or "Defined.". \ + If you really intended to use nested proofs, you can do so by turning the "Nested Proofs Allowed" flag on. You are asserting a new statement while already being in proof editing mode. This feature, called nested proofs, is disabled by default. diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst index 9fda2ab1fa..4bee7cc1b1 100644 --- a/doc/sphinx/language/core/inductive.rst +++ b/doc/sphinx/language/core/inductive.rst @@ -31,7 +31,8 @@ Inductive types proposition). This command supports the :attr:`universes(polymorphic)`, - :attr:`universes(template)`, :attr:`universes(cumulative)`, and + :attr:`universes(template)`, :attr:`universes(cumulative)`, + :attr:`bypass_check(positivity)`, :attr:`bypass_check(universes)`, and :attr:`private(matching)` attributes. Mutually inductive types can be defined by including multiple :n:`@inductive_definition`\s. @@ -49,10 +50,12 @@ Inductive types .. exn:: Non strictly positive occurrence of @ident in @type. - The types of the constructors have to satisfy a *positivity condition* - (see Section :ref:`positivity`). This condition ensures the soundness of - the inductive definition. The positivity checking can be disabled using - the :flag:`Positivity Checking` flag (see :ref:`controlling-typing-flags`). + The types of the constructors have to satisfy a *positivity + condition* (see Section :ref:`positivity`). This condition + ensures the soundness of the inductive definition. + Positivity checking can be disabled using the :flag:`Positivity + Checking` flag or the :attr:`bypass_check(positivity)` attribute (see + :ref:`controlling-typing-flags`). .. exn:: The conclusion of @type is not valid; it must be built from @ident. @@ -390,7 +393,8 @@ constructions. consequently :n:`forall {* @binder }, @type` and its value is equivalent to :n:`fun {* @binder } => @term`. - This command accepts the :attr:`program` attribute. + This command accepts the :attr:`program`, + :attr:`bypass_check(universes)`, and :attr:`bypass_check(guard)` attributes. To be accepted, a :cmd:`Fixpoint` definition has to satisfy syntactical constraints on a special argument called the decreasing argument. They @@ -848,9 +852,7 @@ between universes for inductive types in the Type hierarchy. .. coqtop:: none - Unset Positivity Checking. - Inductive I : Prop := not_I_I (not_I : I -> False) : I. - Set Positivity Checking. + #[bypass_check(positivity)] Inductive I : Prop := not_I_I (not_I : I -> False) : I. .. coqtop:: all @@ -884,9 +886,7 @@ between universes for inductive types in the Type hierarchy. .. coqtop:: none - Unset Positivity Checking. - Inductive Lam := lam (_ : Lam -> Lam). - Set Positivity Checking. + #[bypass_check(positivity)] Inductive Lam := lam (_ : Lam -> Lam). .. coqtop:: all @@ -915,9 +915,7 @@ between universes for inductive types in the Type hierarchy. .. coqtop:: none - Unset Positivity Checking. - Inductive A: Type := introA: ((A -> Prop) -> Prop) -> A. - Set Positivity Checking. + #[bypass_check(positivity)] Inductive A: Type := introA: ((A -> Prop) -> Prop) -> A. .. coqtop:: all diff --git a/doc/sphinx/language/extensions/arguments-command.rst b/doc/sphinx/language/extensions/arguments-command.rst index 2460461ede..95c5914e47 100644 --- a/doc/sphinx/language/extensions/arguments-command.rst +++ b/doc/sphinx/language/extensions/arguments-command.rst @@ -89,11 +89,25 @@ Setting properties of a function's arguments The construct :n:`@name {? % @scope }` declares :n:`@name` as non-implicit if `clear implicits` is specified or at least one other name is declared implicit in the same list of :n:`@name`\s. :token:`scope` can be either a scope name or its delimiting key. See :ref:`binding_to_scope`. + .. exn:: To rename arguments the 'rename' flag must be specified. + :undocumented: + + .. exn:: Flag 'rename' expected to rename @name into @name. + :undocumented: + `clear implicits` makes all implicit arguments into explicit arguments + + .. exn:: The 'clear implicits' flag must be omitted if implicit annotations are given. + :undocumented: + `default implicits` automatically determine the implicit arguments of the object. See :ref:`auto_decl_implicit_args`. + + .. exn:: The 'default implicits' flag is incompatible with implicit annotations. + :undocumented: + `rename` rename implicit arguments for the object. See the example :ref:`here <renaming_implicit_arguments>`. `assert` diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index e7db9cfaca..e866e4c624 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1152,6 +1152,12 @@ Controlling Typing Flags anymore but it still affects the reduction of the term. Unchecked fixpoints are printed by :cmd:`Print Assumptions`. +.. 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 ``bypass_check(guard)``. + .. flag:: Positivity Checking This flag can be used to enable/disable the positivity checking of inductive @@ -1159,6 +1165,12 @@ 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:: 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 ``bypass_check(positivity)``. + .. flag:: Universe Checking This flag can be used to enable/disable the checking of universes, providing a @@ -1167,6 +1179,12 @@ Controlling Typing Flags :cmd:`Print Assumptions`. It has the same effect as `-type-in-type` command line argument (see :ref:`command-line-options`). +.. 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 ``bypass_check(universes)``. + .. cmd:: Print Typing Flags Print the status of the three typing flags: guard checking, positivity checking diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst index 2de6b2a18c..b7f2927000 100644 --- a/doc/sphinx/proofs/writing-proofs/rewriting.rst +++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst @@ -146,6 +146,13 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. only in the conclusion of the goal. The clause argument must not contain any ``type of`` nor ``value of``. + .. tacv:: cutrewrite {? {| <- | -> } } (@term__1 = @term__2) {? in @ident } + :name: cutrewrite + + .. deprecated:: 8.5 + + Use :tacn:`replace` instead. + .. tacn:: subst @ident :name: subst |