diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 23 | ||||
| -rw-r--r-- | doc/sphinx/language/core/definitions.rst | 21 | ||||
| -rw-r--r-- | doc/sphinx/language/extensions/match.rst | 7 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 20 | ||||
| -rw-r--r-- | doc/sphinx/proofs/automatic-tactics/auto.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/proofs/writing-proofs/proof-mode.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/using/tools/coqdoc.rst | 8 |
7 files changed, 62 insertions, 27 deletions
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index cdd31fcb86..2474c784b8 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -336,20 +336,23 @@ Summary of the commands .. cmd:: Instance {? @ident_decl {* @binder } } : @type {? @hint_info } {? {| := %{ {* @field_def } %} | := @term } } - .. insertprodn hint_info hint_info + .. insertprodn hint_info one_pattern .. prodn:: - hint_info ::= %| {? @natural } {? @one_term } + hint_info ::= %| {? @natural } {? @one_pattern } + one_pattern ::= @one_term Declares a typeclass instance named :token:`ident_decl` of the class :n:`@type` with the specified parameters and with fields defined by :token:`field_def`, where each field must be a declared field of the class. - Add one or more :token:`binder`\s to declare a parameterized instance. :token:`hint_info` - specifies the hint priority, where 0 is the highest priority as for + Adds one or more :token:`binder`\s to declare a parameterized instance. :token:`hint_info` + may be used to specify the hint priority, where 0 is the highest priority as for :tacn:`auto` hints. If the priority is not specified, the default is the number - of non-dependent binders of the instance. + of non-dependent binders of the instance. If :token:`one_pattern` is given, terms + matching that pattern will trigger use of the instance. Otherwise, + use is triggered based on the conclusion of the type. This command supports the :attr:`global` attribute that can be used on instances declared in a section so that their @@ -388,6 +391,16 @@ Summary of the commands equivalent to ``Hint Resolve ident : typeclass_instances``, except it registers instances for :cmd:`Print Instances`. + .. flag:: Instance Generalized Output + + .. deprecated:: 8.13 + + Disabled by default, this provides compatibility with Coq + version 8.12 and earlier. + + When enabled, the type of the instance is implicitly generalized + over unbound and :ref:`generalizable <implicit-generalization>` variables as though surrounded by ``\`{}``. + .. cmd:: Print Instances @reference Shows the list of instances associated with the typeclass :token:`reference`. diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst index 4ea3ea5e6d..79489c85f6 100644 --- a/doc/sphinx/language/core/definitions.rst +++ b/doc/sphinx/language/core/definitions.rst @@ -13,15 +13,18 @@ Let-in definitions .. prodn:: term_let ::= let @name {? : @type } := @term in @term | let @name {+ @binder } {? : @type } := @term in @term - | let ( {*, @name } ) {? {? as @name } return @term100 } := @term in @term - | let ' @pattern := @term {? return @term100 } in @term - | let ' @pattern in @pattern := @term return @term100 in @term - -:n:`let @ident := @term in @term’` -denotes the local binding of :n:`@term` to the variable -:n:`@ident` in :n:`@term`’. There is a syntactic sugar for let-in -definition of functions: :n:`let @ident {+ @binder} := @term in @term’` -stands for :n:`let @ident := fun {+ @binder} => @term in @term’`. + | @destructuring_let + +:n:`let @ident := @term__1 in @term__2` represents the local binding of +the variable :n:`@ident` to the value :n:`@term__1` in :n:`@term__2`. + +:n:`let @ident {+ @binder} := @term__1 in @term__2` is an abbreviation +for :n:`let @ident := fun {+ @binder} => @term__1 in @term__2`. + +.. seealso:: + + Extensions of the `let ... in ...` syntax are described in + :ref:`irrefutable-patterns`. .. index:: single: ... : ... (type cast) diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst index 23389eba3b..8e62c2af13 100644 --- a/doc/sphinx/language/extensions/match.rst +++ b/doc/sphinx/language/extensions/match.rst @@ -86,6 +86,13 @@ Pattern-matching on terms inhabiting inductive type having only one constructor can be alternatively written using :g:`let … in …` constructions. There are two variants of them. +.. insertprodn destructuring_let destructuring_let + +.. prodn:: + destructuring_let ::= let ( {*, @name } ) {? {? as @name } return @term100 } := @term in @term + | let ' @pattern := @term {? return @term100 } in @term + | let ' @pattern in @pattern := @term return @term100 in @term + First destructuring let syntax ++++++++++++++++++++++++++++++ diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 7baf193266..86d1d25745 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -133,7 +133,7 @@ to accessible objects. (see Section :ref:`invocation-of-tactics`). .. prodn:: search_item ::= {? {| head | hyp | concl | headhyp | headconcl } : } @string {? % @scope_key } - | {? {| head | hyp | concl | headhyp | headconcl } : } @one_term + | {? {| head | hyp | concl | headhyp | headconcl } : } @one_pattern | is : @logical_kind Searched objects can be filtered by patterns, by the constants they @@ -141,9 +141,9 @@ to accessible objects. (see Section :ref:`invocation-of-tactics`). names. The location of the pattern or constant within a term - :n:`@one_term` + :n:`@one_pattern` Search for objects whose type contains a subterm matching the - pattern :n:`@one_term`. Holes of the pattern are indicated by + pattern :n:`@one_pattern`. Holes of the pattern are indicated by `_` or :n:`?@ident`. If the same :n:`?@ident` occurs more than once in the pattern, all occurrences in the subterm must be identical. See :ref:`this example <search-pattern>`. @@ -312,7 +312,7 @@ to accessible objects. (see Section :ref:`invocation-of-tactics`). Search is:Instance [ Reflexive | Symmetric ]. -.. cmd:: SearchHead @one_term {? {| inside | outside } {+ @qualid } } +.. cmd:: SearchHead @one_pattern {? {| inside | outside } {+ @qualid } } .. deprecated:: 8.12 @@ -320,8 +320,8 @@ to accessible objects. (see Section :ref:`invocation-of-tactics`). Displays the name and type of all hypotheses of the selected goal (if any) and theorems of the current context that have the - form :n:`{? forall {* @binder }, } {* P__i -> } C` where :n:`@one_term` - matches a subterm of `C` in head position. For example, a :n:`@one_term` of `f _ b` + form :n:`{? forall {* @binder }, } {* P__i -> } C` where :n:`@one_pattern` + matches a subterm of `C` in head position. For example, a :n:`@one_pattern` of `f _ b` matches `f a b`, which is a subterm of `C` in head position when `C` is `f a b c`. See :cmd:`Search` for an explanation of the `inside`/`outside` clauses. @@ -337,12 +337,12 @@ to accessible objects. (see Section :ref:`invocation-of-tactics`). SearchHead le. SearchHead (@eq bool). -.. cmd:: SearchPattern @one_term {? {| inside | outside } {+ @qualid } } +.. cmd:: SearchPattern @one_pattern {? {| inside | outside } {+ @qualid } } Displays the name and type of all hypotheses of the selected goal (if any) and theorems of the current context ending with :n:`{? forall {* @binder }, } {* P__i -> } C` that match the pattern - :n:`@one_term`. + :n:`@one_pattern`. See :cmd:`Search` for an explanation of the `inside`/`outside` clauses. @@ -362,11 +362,11 @@ to accessible objects. (see Section :ref:`invocation-of-tactics`). SearchPattern (?X1 + _ = _ + ?X1). -.. cmd:: SearchRewrite @one_term {? {| inside | outside } {+ @qualid } } +.. cmd:: SearchRewrite @one_pattern {? {| inside | outside } {+ @qualid } } Displays the name and type of all hypotheses of the selected goal (if any) and theorems of the current context that have the form - :n:`{? forall {* @binder }, } {* P__i -> } LHS = RHS` where :n:`@one_term` + :n:`{? forall {* @binder }, } {* P__i -> } LHS = RHS` where :n:`@one_pattern` matches either `LHS` or `RHS`. See :cmd:`Search` for an explanation of the `inside`/`outside` clauses. diff --git a/doc/sphinx/proofs/automatic-tactics/auto.rst b/doc/sphinx/proofs/automatic-tactics/auto.rst index e6dc6f6c51..485b92342d 100644 --- a/doc/sphinx/proofs/automatic-tactics/auto.rst +++ b/doc/sphinx/proofs/automatic-tactics/auto.rst @@ -280,9 +280,7 @@ automatically created. sections. + :attr:`export` are visible from other modules when they import the current - module. Requiring it is not enough. This attribute is only effective for - the :cmd:`Hint Resolve`, :cmd:`Hint Immediate`, :cmd:`Hint Unfold` and - :cmd:`Hint Extern` variants of the command. + module. Requiring it is not enough. + :attr:`global` hints are made available by merely requiring the current module. diff --git a/doc/sphinx/proofs/writing-proofs/proof-mode.rst b/doc/sphinx/proofs/writing-proofs/proof-mode.rst index fd8a0329d6..40d032543f 100644 --- a/doc/sphinx/proofs/writing-proofs/proof-mode.rst +++ b/doc/sphinx/proofs/writing-proofs/proof-mode.rst @@ -288,12 +288,18 @@ Name a set of section hypotheses for ``Proof using`` existential variables remain. To instantiate existential variables during proof edition, you should use the tactic :tacn:`instantiate`. + .. deprecated:: 8.13 + .. cmd:: Grab Existential Variables This command can be run when a proof has no more goal to be solved but has remaining uninstantiated existential variables. It takes every uninstantiated existential variable and turns it into a goal. + .. deprecated:: 8.13 + + Use :cmd:`Unshelve` instead. + Proof modes ``````````` diff --git a/doc/sphinx/using/tools/coqdoc.rst b/doc/sphinx/using/tools/coqdoc.rst index 7ab8f9d763..b68b2ed2a7 100644 --- a/doc/sphinx/using/tools/coqdoc.rst +++ b/doc/sphinx/using/tools/coqdoc.rst @@ -200,6 +200,14 @@ at the beginning of a line. if n <= 1 then 1 else n * fact (n-1) >> +Verbatim material on a single line is also possible (assuming that +``>>`` is not part of the text to be presented as verbatim). + +.. example:: + + :: + + Here is the corresponding caml expression: << fact (n-1) >> Hyperlinks |