diff options
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 29 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 157 |
2 files changed, 98 insertions, 88 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 4f2f74aae4..19573eee43 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3222,7 +3222,7 @@ the conversion in hypotheses :n:`{+ @ident}`. + A constant can be marked to be unfolded only if applied to enough arguments. The number of arguments required can be specified using the - ``/`` symbol in the argument list of the :cmd:`Arguments <Arguments (implicits)>` vernacular command. + ``/`` symbol in the argument list of the :cmd:`Arguments` command. .. example:: @@ -3759,6 +3759,24 @@ automatically created. .. cmd:: Hint @hint_definition : {+ @ident} The general command to add a hint to some databases :n:`{+ @ident}`. + + This command supports the :attr:`local`, :attr:`global` and :attr:`export` + locality attributes. When no locality is explictly given, the + command is :attr:`local` inside a section and :attr:`global` otherwise. + + + :attr:`local` hints are never visible from other modules, even if they + require or import the current module. Inside a section, the :attr:`local` + attribute is useless since hints do not survive anyway to the closure of + 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. + + + :attr:`global` hints are made available by merely requiring the current + module. + The various possible :production:`hint_definition`\s are given below. .. cmdv:: Hint @hint_definition @@ -3767,13 +3785,6 @@ automatically created. .. deprecated:: 8.10 - .. cmdv:: Local Hint @hint_definition : {+ @ident} - - This is used to declare hints that must not be exported to the other modules - that require and import the current module. Inside a section, the flag - Local is useless since hints do not survive anyway to the closure of - sections. - .. cmdv:: Hint Resolve @qualid {? | {? @num} {? @pattern}} : @ident :name: Hint Resolve @@ -4275,7 +4286,7 @@ some incompatibilities. :name: Firstorder Solver The default tactic used by :tacn:`firstorder` when no rule applies is - :g:`auto with *`, it can be reset locally or globally using this option. + :g:`auto with core`, it can be reset locally or globally using this option. .. cmd:: Print Firstorder Solver diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index d1f3dcc309..b22c5286fe 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -91,34 +91,30 @@ and tables: Flags, options and tables are identified by a series of identifiers, each with an initial capital letter. -.. cmd:: {? {| Local | Global | Export } } Set @flag +.. cmd:: Set @flag :name: Set - Sets :token:`flag` on. Scoping qualifiers are - described :ref:`here <set_unset_scope_qualifiers>`. + Sets :token:`flag` on. -.. cmd:: {? {| Local | Global | Export } } Unset @flag +.. cmd:: Unset @flag :name: Unset - Sets :token:`flag` off. Scoping qualifiers are - described :ref:`here <set_unset_scope_qualifiers>`. + Sets :token:`flag` off. .. cmd:: Test @flag Prints the current value of :token:`flag`. -.. cmd:: {? {| Local | Global | Export } } Set @option {| @num | @string } +.. cmd:: Set @option {| @num | @string } :name: Set @option - Sets :token:`option` to the specified value. Scoping qualifiers are - described :ref:`here <set_unset_scope_qualifiers>`. + Sets :token:`option` to the specified value. -.. cmd:: {? {| Local | Global | Export } } Unset @option +.. cmd:: Unset @option :name: Unset @option - Sets :token:`option` to its default value. Scoping qualifiers are - described :ref:`here <set_unset_scope_qualifiers>`. + Sets :token:`option` to its default value. .. cmd:: Test @option @@ -157,27 +153,37 @@ capital letter. A synonym for :cmd:`Print Options`. -.. _set_unset_scope_qualifiers: +Locality attributes supported by :cmd:`Set` and :cmd:`Unset` +```````````````````````````````````````````````````````````` + +The :cmd:`Set` and :cmd:`Unset` commands support the :attr:`local`, +:attr:`global` and :attr:`export` locality attributes: + +* no attribute: the original setting is *not* restored at the end of + the current module or section. +* :attr:`local` (an alternative syntax is to use the ``Local`` + prefix): the setting is applied within the current module or + section. The original value of the setting is restored at the end + of the current module or section. +* :attr:`export` (an alternative syntax is to use the ``Export`` + prefix): similar to :attr:`local`, the original value of the setting + is restored at the end of the current module or section. In + addition, if the value is set in a module, then :cmd:`Import`\-ing + the module sets the option or flag. +* :attr:`global` (an alternative syntax is to use the ``Global`` + prefix): the original setting is *not* restored at the end of the + current module or section. In addition, if the value is set in a + file, then :cmd:`Require`\-ing the file sets the option. + +Newly opened modules and sections inherit the current settings. -Scope qualifiers for :cmd:`Set` and :cmd:`Unset` -````````````````````````````````````````````````` - -:n:`{? {| Local | Global | Export } }` - -Flag and option settings can be global in scope or local to nested scopes created by -:cmd:`Module` and :cmd:`Section` commands. There are four alternatives: - -* no qualifier: the original setting is *not* restored at the end of the current module or section. -* **Local**: the setting is applied within the current scope. The original value of the option - or flag is restored at the end of the current module or section. -* **Global**: similar to no qualifier, the original setting is *not* restored at the end of the current - module or section. In addition, if the value is set in a file, then :cmd:`Require`-ing - the file sets the option. -* **Export**: similar to **Local**, the original value of the option or flag is restored at the - end of the current module or section. In addition, if the value is set in a file, then :cmd:`Import`-ing - the file sets the option. +.. note:: -Newly opened scopes inherit the current settings. + The use of the :attr:`global` attribute with the :cmd:`Set` and + :cmd:`Unset` commands is discouraged. If your goal is to define + project-wide settings, you should rather use the command-line + arguments ``-set`` and ``-unset`` for setting flags and options + (cf. :ref:`command-line-options`). .. _requests-to-the-environment: @@ -315,18 +321,6 @@ Requests to the environment Search (?x * _ + ?x * _)%Z outside OmegaLemmas. - .. cmdv:: SearchAbout - :name: SearchAbout - - .. deprecated:: 8.5 - - Up to |Coq| version 8.4, :cmd:`Search` had the behavior of current - :cmd:`SearchHead` and the behavior of current :cmd:`Search` was obtained with - command :cmd:`SearchAbout`. For compatibility, the deprecated name - :cmd:`SearchAbout` can still be used as a synonym of :cmd:`Search`. For - compatibility, the list of objects to search when using :cmd:`SearchAbout` - may also be enclosed by optional ``[ ]`` delimiters. - .. cmd:: SearchHead @term @@ -602,11 +596,11 @@ file is a particular case of module called *library file*. This loads and declares the module :n:`@qualid` and its dependencies then imports the contents of :n:`@qualid` as described - :ref:`here <import_qualid>`. It does not import the modules on which - qualid depends unless these modules were themselves required in module + for :cmd:`Import`. It does not import the modules that + :n:`@qualid` depends on unless these modules were themselves required in module :n:`@qualid` - using :cmd:`Require Export`, as described below, or recursively required - through a sequence of :cmd:`Require Export`. If the module required has + using :cmd:`Require Export`, or recursively required + through a series of :cmd:`Require Export`. If the module required has already been loaded, :cmd:`Require Import` :n:`@qualid` simply imports it, as :cmd:`Import` :n:`@qualid` would. @@ -665,13 +659,9 @@ file is a particular case of module called *library file*. the time it was compiled. - .. exn:: Require is not allowed inside a module or a module type. + .. warn:: Require inside a module is deprecated and strongly discouraged. You can Require a module at toplevel and optionally Import it inside another one. - This command - is not allowed inside a module or a module type being defined. It is - meant to describe a dependency between compilation units. Note however - that the commands ``Import`` and ``Export`` alone can be used inside modules - (see Section :ref:`Import <import_qualid>`). + Note that the :cmd:`Import` and :cmd:`Export` commands can be used inside modules. .. seealso:: Chapter :ref:`thecoqcommands` @@ -927,16 +917,17 @@ Quitting and debugging .. cmd:: Fail @command - For debugging scripts, sometimes it is desirable to know - whether a command or a tactic fails. If the given :n:`@command` - fails, the ``Fail`` statement succeeds, without changing the proof - state, and in interactive mode, the system - prints a message confirming the failure. - If the given :n:`@command` succeeds, the statement is an error, and - it prints a message indicating that the failure did not occur. + For debugging scripts, sometimes it is desirable to know whether a + command or a tactic fails. If the given :n:`@command` fails, then + :n:`Fail @command` succeeds (excepts in the case of + critical errors, like a "stack overflow"), without changing the + proof state, and in interactive mode, the system prints a message + confirming the failure. .. exn:: The command has not failed! - :undocumented: + + If the given :n:`@command` succeeds, then :n:`Fail @command` + fails with this error message. .. _controlling-display: @@ -1152,44 +1143,52 @@ described first. Controlling the locality of commands ----------------------------------------- +.. attr:: global + local -.. cmd:: Local @command - Global @command - - Some commands support a Local or Global prefix modifier to control the - scope of their effect. There are four kinds of commands: - + Some commands support a :attr:`local` or :attr:`global` attribute + to control the scope of their effect. There is also a legacy (and + much more commonly used) syntax using the ``Local`` or ``Global`` + prefixes (see :n:`@legacy_attr`). There are four kinds of + commands: + Commands whose default is to extend their effect both outside the section and the module or library file they occur in. For these - commands, the Local modifier limits the effect of the command to the + commands, the :attr:`local` attribute limits the effect of the command to the current section or module it occurs in. As an example, the :cmd:`Coercion` and :cmd:`Strategy` commands belong to this category. + Commands whose default behavior is to stop their effect at the end of the section they occur in but to extend their effect outside the module or - library file they occur in. For these commands, the Local modifier limits the + library file they occur in. For these commands, the :attr:`local` attribute limits the effect of the command to the current module if the command does not occur in a - section and the Global modifier extends the effect outside the current + section and the :attr:`global` attribute extends the effect outside the current sections and current module if the command occurs in a section. As an example, - the :cmd:`Arguments <Arguments (implicits)>`, :cmd:`Ltac` or :cmd:`Notation` commands belong + the :cmd:`Arguments`, :cmd:`Ltac` or :cmd:`Notation` commands belong to this category. Notice that a subclass of these commands do not support - extension of their scope outside sections at all and the Global modifier is not + extension of their scope outside sections at all and the :attr:`global` attribute is not applicable to them. + Commands whose default behavior is to stop their effect at the end - of the section or module they occur in. For these commands, the ``Global`` - modifier extends their effect outside the sections and modules they - occur in. The :cmd:`Transparent` and :cmd:`Opaque` - (see Section :ref:`vernac-controlling-the-reduction-strategies`) commands + of the section or module they occur in. For these commands, the :attr:`global` + attribute extends their effect outside the sections and modules they + occur in. The :cmd:`Transparent` and :cmd:`Opaque` commands belong to this category. + Commands whose default behavior is to extend their effect outside sections but not outside modules when they occur in a section and to extend their effect outside the module or library file they occur in - when no section contains them. For these commands, the Local modifier - limits the effect to the current section or module while the Global - modifier extends the effect outside the module even when the command + when no section contains them. For these commands, the :attr:`local` attribute + limits the effect to the current section or module while the :attr:`global` + attribute extends the effect outside the module even when the command occurs in a section. The :cmd:`Set` and :cmd:`Unset` commands belong to this category. +.. attr:: export + + Some commands support an :attr:`export` attribute. The effect of + the attribute is to make the effect of the command available when + the module containing it is imported. It is supported in + particular by the :cmd:`Hint`, :cmd:`Set` and :cmd:`Unset` + commands. + .. _controlling-typing-flags: Controlling Typing Flags |