From abd6bbd90753fd98355e551d8dc8ecfd07494639 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Mon, 16 Apr 2018 16:12:07 +0200 Subject: [Sphinx] Fix a lot of references and description of options --- doc/sphinx/addendum/implicit-coercions.rst | 41 ++--- doc/sphinx/addendum/type-classes.rst | 111 ++++++------- doc/sphinx/language/gallina-extensions.rst | 22 +-- .../proof-engine/ssreflect-proof-language.rst | 7 +- doc/sphinx/proof-engine/tactics.rst | 154 ++++++++--------- doc/sphinx/proof-engine/vernacular-commands.rst | 182 ++++++--------------- 6 files changed, 196 insertions(+), 321 deletions(-) diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index ec1b942e0..19d4ba9ba 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -255,17 +255,16 @@ Displaying Available Coercions Activating the Printing of Coercions ------------------------------------- -.. cmd:: Set Printing Coercions. +.. opt:: Printing Coercions - This command forces all the coercions to be printed. - Conversely, to skip the printing of coercions, use - ``Unset Printing Coercions``. By default, coercions are not printed. + When on, this option forces all the coercions to be printed. + By default, coercions are not printed. -.. cmd:: Add Printing Coercion @qualid. +.. cmd:: Add Printing Coercion @qualid - This command forces coercion denoted by `qualid` to be printed. - To skip the printing of coercion `qualid`, use - ``Remove Printing Coercion`` `qualid`. By default, a coercion is never printed. + This command forces coercion denoted by :n:`@qualid` to be printed. To skip + the printing of coercion :n:`@qualid`, use :cmd:`Remove Printing Coercion`. By + default, a coercion is never printed. .. _coercions-classes-as-records: @@ -291,12 +290,9 @@ by extending the existing :cmd:`Record` macro. Its new syntax is: (this may fail if the uniform inheritance condition is not satisfied). -.. note:: +.. cmdv:: Structure {? >} @ident {? @binders} : @sort := {? @ident} { {+; @ident :{? >} @term } }. - The keyword ``Structure`` is a synonym of ``Record``. - -.. - FIXME: \comindex{Structure} + This is a synonym of :cmd:`Record`. Coercions and Sections @@ -312,20 +308,17 @@ coercions which do not verify the uniform inheritance condition any longer are also forgotten. Coercions and Modules ---------------------= - -From |Coq| version 8.3, the coercions present in a module are activated -only when the module is explicitly imported. Formerly, the coercions -were activated as soon as the module was required, whatever it was -imported or not. - -To recover the behavior of the versions of |Coq| prior to 8.3, use the -following command: +--------------------- -.. cmd:: Set Automatic Coercions Import. +.. opt:: Automatic Coercions Import -To cancel the effect of the option, use instead ``Unset Automatic Coercions Import``. + Since |Coq| version 8.3, the coercions present in a module are activated + only when the module is explicitly imported. Formerly, the coercions + were activated as soon as the module was required, whatever it was + imported or not. + This option makes it possible to recover the behavior of the versions of + |Coq| prior to 8.3. Examples -------- diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 8861cac8a..d6955b310 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -466,80 +466,72 @@ Typeclasses Transparent, Typclasses Opaque This is equivalent to ``Hint Transparent, Opaque ident : typeclass_instances``. -Set Typeclasses Dependency Order -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +.. opt:: Typeclasses Dependency Order -This option (on by default since 8.6) respects the dependency order -between subgoals, meaning that subgoals which are depended on by other -subgoals come first, while the non-dependent subgoals were put before -the dependent ones previously (Coq v8.5 and below). This can result in -quite different performance behaviors of proof search. + This option (on by default since 8.6) respects the dependency order + between subgoals, meaning that subgoals which are depended on by other + subgoals come first, while the non-dependent subgoals were put before + the dependent ones previously (Coq v8.5 and below). This can result in + quite different performance behaviors of proof search. -Set Typeclasses Filtered Unification -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +.. opt:: Typeclasses Filtered Unification -This option, available since Coq 8.6 and off by default, switches the -hint application procedure to a filter-then-unify strategy. To apply a -hint, we first check that the goal *matches* syntactically the -inferred or specified pattern of the hint, and only then try to -*unify* the goal with the conclusion of the hint. This can drastically -improve performance by calling unification less often, matching -syntactic patterns being very quick. This also provides more control -on the triggering of instances. For example, forcing a constant to -explicitely appear in the pattern will make it never apply on a goal -where there is a hole in that place. + This option, available since Coq 8.6 and off by default, switches the + hint application procedure to a filter-then-unify strategy. To apply a + hint, we first check that the goal *matches* syntactically the + inferred or specified pattern of the hint, and only then try to + *unify* the goal with the conclusion of the hint. This can drastically + improve performance by calling unification less often, matching + syntactic patterns being very quick. This also provides more control + on the triggering of instances. For example, forcing a constant to + explicitely appear in the pattern will make it never apply on a goal + where there is a hole in that place. -Set Typeclasses Limit Intros -~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +.. opt:: Typeclasses Limit Intros + This option (on by default) controls the ability to apply hints while + avoiding (functional) eta-expansions in the generated proof term. It + does so by allowing hints that conclude in a product to apply to a + goal with a matching product directly, avoiding an introduction. + *Warning:* this can be expensive as it requires rebuilding hint + clauses dynamically, and does not benefit from the invertibility + status of the product introduction rule, resulting in potentially more + expensive proof-search (i.e. more useless backtracking). -This option (on by default) controls the ability to apply hints while -avoiding (functional) eta-expansions in the generated proof term. It -does so by allowing hints that conclude in a product to apply to a -goal with a matching product directly, avoiding an introduction. -*Warning:* this can be expensive as it requires rebuilding hint -clauses dynamically, and does not benefit from the invertibility -status of the product introduction rule, resulting in potentially more -expensive proof-search (i.e. more useless backtracking). +.. opt:: Typeclass Resolution For Conversion -Set Typeclass Resolution For Conversion -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + This option (on by default) controls the use of typeclass resolution + when a unification problem cannot be solved during elaboration/type- + inference. With this option on, when a unification fails, typeclass + resolution is tried before launching unification once again. -This option (on by default) controls the use of typeclass resolution -when a unification problem cannot be solved during elaboration/type- -inference. With this option on, when a unification fails, typeclass -resolution is tried before launching unification once again. +.. opt:: Typeclasses Strict Resolution -Set Typeclasses Strict Resolution -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + Typeclass declarations introduced when this option is set have a + stricter resolution behavior (the option is off by default). When + looking for unifications of a goal with an instance of this class, we + “freeze” all the existentials appearing in the goals, meaning that + they are considered rigid during unification and cannot be + instantiated. -Typeclass declarations introduced when this option is set have a -stricter resolution behavior (the option is off by default). When -looking for unifications of a goal with an instance of this class, we -“freeze” all the existentials appearing in the goals, meaning that -they are considered rigid during unification and cannot be -instantiated. +.. opt:: Typeclasses Unique Solutions -Set Typeclasses Unique Solutions -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + When a typeclass resolution is launched we ensure that it has a single + solution or fail. This ensures that the resolution is canonical, but + can make proof search much more expensive. -When a typeclass resolution is launched we ensure that it has a single -solution or fail. This ensures that the resolution is canonical, but -can make proof search much more expensive. +.. opt:: Typeclasses Unique Instances -Set Typeclasses Unique Instances -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -Typeclass declarations introduced when this option is set have a more -efficient resolution behavior (the option is off by default). When a -solution to the typeclass goal of this class is found, we never -backtrack on it, assuming that it is canonical. + Typeclass declarations introduced when this option is set have a more + efficient resolution behavior (the option is off by default). When a + solution to the typeclass goal of this class is found, we never + backtrack on it, assuming that it is canonical. Typeclasses eauto `:=` @@ -562,7 +554,7 @@ Typeclasses eauto `:=` Set Typeclasses Debug ~~~~~~~~~~~~~~~~~~~~~ -.. cmd:: Set Typeclasses Debug {? Verbosity @num} +.. opt:: Typeclasses Debug {? Verbosity @num} These options allow to see the resolution steps of typeclasses that are performed during search. The ``Debug`` option is synonymous to ``Debug @@ -570,11 +562,10 @@ Verbosity 1``, and ``Debug Verbosity 2`` provides more information (tried tactics, shelving of goals, etc…). -Set Refine Instance Mode -~~~~~~~~~~~~~~~~~~~~~~~~ +.. opt:: Refine Instance Mode -The option Refine Instance Mode allows to switch the behavior of -instance declarations made through the Instance command. +This options allows to switch the behavior of instance declarations made through +the Instance command. + When it is on (the default), instances that have unsolved holes in their proof-term silently open the proof mode with the remaining diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index f474eade7..8d47949db 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -148,7 +148,7 @@ available: It can be activated for printing with -.. cmd:: Set Printing Projections. +.. opt:: Printing Projections .. example:: @@ -249,7 +249,7 @@ printing of pattern-matching over primitive records. Primitive Record Types ++++++++++++++++++++++ -When the ``Set Primitive Projections`` option is on, definitions of +When the :opt:`Primitive Projections` option is on, definitions of record types change meaning. When a type is declared with primitive projections, its :g:`match` construct is disabled (see :ref:`primitive_projections` though). To eliminate the (co-)inductive type, one must use its defined primitive projections. @@ -328,7 +328,7 @@ patterns are allowed, as in ML-like languages. The extension just acts as a macro that is expanded during parsing into a sequence of match on simple patterns. Especially, a construction defined using the extended match is generally printed -under its expanded form (see ``Set Printing Matching`` in :ref:`controlling-match-pp`). +under its expanded form (see :opt:`Printing Matching`). See also: :ref:`extendedpatternmatching`. @@ -1506,10 +1506,10 @@ inserted. In the second case, the function is considered to be implicitly applied to the implicit arguments it is waiting for: one says that the implicit argument is maximally inserted. -Each implicit argument can be declared to have to be inserted -maximally or non maximally. This can be governed argument per argument -by the command ``Implicit Arguments`` (see Section :ref:`declare-implicit-args`) or globally by the -command ``Set Maximal Implicit Insertion`` (see Section :ref:`controlling-insertion-implicit-args`). +Each implicit argument can be declared to have to be inserted maximally or non +maximally. This can be governed argument per argument by the command ``Implicit +Arguments`` (see Section :ref:`declare-implicit-args`) or globally by the +:opt:`Maximal Implicit Insertion` option. See also :ref:`displaying-implicit-args`. @@ -1882,7 +1882,7 @@ arguments that are not detected as strict implicit arguments. This “defensive” mode can quickly make the display cumbersome so this can be deactivated by turning this option off. -See also: ``Set Printing All`` in :ref:`printing_constructions_full`. +See also: :opt:`Printing All`. Interaction with subtyping ~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -2134,9 +2134,9 @@ sensitive to the implicit arguments). Turning this option on deactivates all high-level printing features such as coercions, implicit arguments, returned type of pattern-matching, notations and various syntactic sugar for pattern-matching or record projections. -Otherwise said, ``Set Printing All`` includes the effects of the commands -``Set Printing Implicit``, ``Set Printing Coercions``, ``Set Printing Synth``, -``Unset Printing Projections``, and ``Unset Printing Notations``. To reactivate +Otherwise said, :opt:`Printing All` includes the effects of the options +:opt:`Printing Implicit`, :opt:`Printing Coercions`, :opt:`Printing Synth`, +:opt:`Printing Projections`, and :opt:`Printing Notations`. To reactivate the high-level printing features, use the command ``Unset Printing All``. .. _printing-universes: diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 074c6f1e2..6ddb0b027 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -2749,12 +2749,9 @@ type classes inference. No inference for ``t``. Unresolved instances are quantified in the (inferred) type of ``t`` and abstracted in ``t``. +.. opt:: SsrHave NoTCResolution -The behavior of |SSR| 1.4 and below (never resolve type classes) -can be restored with the option - -.. cmd:: Set SsrHave NoTCResolution. - + This option restores the behavior of |SSR| 1.4 and below (never resolve type classes). Variants: the suff and wlog tactics ``````````````````````````````````` diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 08aa7110d..1868f4b9d 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -51,20 +51,15 @@ specified, the default selector is used. tactic_invocation : toplevel_selector : tactic. : |tactic . -.. cmd:: Set Default Goal Selector @toplevel_selector. +.. opt:: Default Goal Selector @toplevel_selector. -After using this command, the default selector – used when no selector -is specified when applying a tactic – is set to the chosen value. The -initial value is 1, hence the tactics are, by default, applied to the -first goal. Using Set Default Goal Selector ‘‘all’’ will make is so -that tactics are, by default, applied to every goal simultaneously. -Then, to apply a tactic tac to the first goal only, you can write -1:tac. Although more selectors are available, only ‘‘all’’ or a single -natural number are valid default goal selectors. - -.. cmd:: Test Default Goal Selector. - -This command displays the current default selector. + This option controls the default selector – used when no selector is + specified when applying a tactic – is set to the chosen value. The initial + value is 1, hence the tactics are, by default, applied to the first goal. + Using value ``all`` will make is so that tactics are, by default, applied to + every goal simultaneously. Then, to apply a tactic tac to the first goal + only, you can write ``1:tac``. Although more selectors are available, only + ``all`` or a single natural number are valid default goal selectors. .. _bindingslist: @@ -123,14 +118,12 @@ following syntax: The role of an occurrence clause is to select a set of occurrences of a term in a goal. In the first case, the :n:`@ident {? at {* num}}` parts indicate that -occurrences have to be selected in the hypotheses named :n:`@ident`. If no numbers -are given for hypothesis :n:`@ident`, then all the occurrences of `term` in the -hypothesis are selected. If numbers are given, they refer to occurrences of -`term` when the term is printed using option ``Set Printing All`` (see -:ref:`printing_constructions_full`), counting from left to right. In -particular, occurrences of `term` in implicit arguments (see -:ref:`ImplicitArguments`) or coercions (see :ref:`Coercions`) -are counted. +occurrences have to be selected in the hypotheses named :n:`@ident`. If no +numbers are given for hypothesis :n:`@ident`, then all the occurrences of `term` +in the hypothesis are selected. If numbers are given, they refer to occurrences +of `term` when the term is printed using option :opt:`Printing All`, counting +from left to right. In particular, occurrences of `term` in implicit arguments +(see :ref:`ImplicitArguments`) or coercions (see :ref:`Coercions`) are counted. If a minus sign is given between at and the list of occurrences, it negates the condition so that the clause denotes all the occurrences @@ -346,7 +339,7 @@ does. This summarizes the different syntaxes for ``apply`` and ``eapply``. .. tacv:: lapply @term - :name: `lapply + :name: lapply This tactic applies to any goal, say :g:`G`. The argument term has to be well-formed in the current context, its type being reducible to a non-dependent @@ -437,7 +430,7 @@ sequence ``cut B. 2:apply H.`` where ``cut`` is described below. ``forall A, ... -> A``. Excluding this kind of lemma can be avoided by setting the following option: -.. opt:: Set Universal Lemma Under Conjunction. +.. opt:: Universal Lemma Under Conjunction This option, which preserves compatibility with versions of Coq prior to 8.4 is also available for :n:`apply @term in @ident` (see :tacn:`apply ... in`). @@ -829,15 +822,10 @@ quantification or an implication. so that all the arguments of the i-th constructors of the corresponding inductive type are introduced can be controlled with the following option: - .. cmd:: Set Bracketing Last Introduction Pattern. - - Force completion, if needed, when the last introduction pattern is a - disjunctive or conjunctive pattern (this is the default). + .. opt:: Bracketing Last Introduction Pattern - .. cmd:: Unset Bracketing Last Introduction Pattern. - - Deactivate completion when the last introduction pattern is a disjunctive or - conjunctive pattern. + Force completion, if needed, when the last introduction pattern is a + disjunctive or conjunctive pattern (on by default). .. tacn:: clear @ident :name: clear @@ -1239,7 +1227,7 @@ name of the variable (here :g:`n`) is chosen based on :g:`T`. This is equivalent to :n:`generalize @term` but it generalizes only over the specified occurrences of :n:`@term` (counting from left to right on the - expression printed using option :g:`Set Printing All`). + expression printed using option :opt:`Printing All`). .. tacv:: generalize @term as @ident @@ -1964,13 +1952,13 @@ It is possible to ensure that :n:`injection @term` erases the original hypothesis and leaves the generated equalities in the context rather than putting them as antecedents of the current goal, as if giving :n:`injection @term as` (with an empty list of names). To obtain this -behavior, the option ``Set Structural Injection`` must be activated. This +behavior, the option :opt:`Structural Injection` must be activated. This option is off by default. -By default, ``injection`` only creates new equalities between :n:`@terms` whose +By default, :tacn:`injection` only creates new equalities between :n:`@terms` whose type is in sort :g:`Type` or :g:`Set`, thus implementing a special behavior for objects that are proofs of a statement in :g:`Prop`. This behavior can be -turned off by setting the option ``Set Keep Proof Equalities``. +turned off by setting the option :opt:`Keep Proof Equalities`. .. tacn:: inversion @ident :name: inversion @@ -1996,8 +1984,8 @@ turned off by setting the option ``Set Keep Proof Equalities``. equalities between expressions that appeared in the hypothesis that is being processed. By default, no equalities are generated if they relate two proofs (i.e. equalities between :n:`@terms` whose type is in sort - :g:`Prop`). This behavior can be turned off by using the option ``Set Keep - Proof Equalities``. + :g:`Prop`). This behavior can be turned off by using the option + :opt`Keep Proof Equalities`. .. tacv:: inversion @num @@ -2513,28 +2501,28 @@ unfolded and cleared. .. note:: - The behavior of subst can be controlled using option ``Set Regular Subst - Tactic.`` When this option is activated, subst also deals with the - following corner cases: - - + A context with ordered hypotheses :n:`@ident`:sub:`1` :n:`= @ident`:sub:`2` - and :n:`@ident`:sub:`1` :n:`= t`, or :n:`t′ = @ident`:sub:`1`` with `t′` not - a variable, and no other hypotheses of the form :n:`@ident`:sub:`2` :n:`= u` - or :n:`u = @ident`:sub:`2`; without the option, a second call to - subst would be necessary to replace :n:`@ident`:sub:`2` by `t` or - `t′` respectively. - + The presence of a recursive equation which without the option would - be a cause of failure of :tacn:`subst`. - + A context with cyclic dependencies as with hypotheses :n:`@ident`:sub:`1` :n:`= f @ident`:sub:`2` - and :n:`@ident`:sub:`2` :n:`= g @ident`:sub:`1` which without the - option would be a cause of failure of :tacn:`subst`. - - Additionally, it prevents a local definition such as :n:`@ident := t` to be - unfolded which otherwise it would exceptionally unfold in configurations - containing hypotheses of the form :n:`@ident = u`, or :n:`u′ = @ident` - with `u′` not a variable. Finally, it preserves the initial order of - hypotheses, which without the option it may break. The option is on by - default. + The behavior of subst can be controlled using option :opt:`Regular Subst + Tactic`. When this option is activated, subst also deals with the + following corner cases: + + + A context with ordered hypotheses :n:`@ident`:sub:`1` :n:`= @ident`:sub:`2` + and :n:`@ident`:sub:`1` :n:`= t`, or :n:`t′ = @ident`:sub:`1`` with `t′` not + a variable, and no other hypotheses of the form :n:`@ident`:sub:`2` :n:`= u` + or :n:`u = @ident`:sub:`2`; without the option, a second call to + subst would be necessary to replace :n:`@ident`:sub:`2` by `t` or + `t′` respectively. + + The presence of a recursive equation which without the option would + be a cause of failure of :tacn:`subst`. + + A context with cyclic dependencies as with hypotheses :n:`@ident`:sub:`1` :n:`= f @ident`:sub:`2` + and :n:`@ident`:sub:`2` :n:`= g @ident`:sub:`1` which without the + option would be a cause of failure of :tacn:`subst`. + + Additionally, it prevents a local definition such as :n:`@ident := t` to be + unfolded which otherwise it would exceptionally unfold in configurations + containing hypotheses of the form :n:`@ident = u`, or :n:`u′ = @ident` + with `u′` not a variable. Finally, it preserves the initial order of + hypotheses, which without the option it may break. The option is on by + default. .. tacn:: stepl @term @@ -3578,24 +3566,21 @@ We propose a smooth transitional path by providing the ``Loose Hint Behavior`` option which accepts three flags allowing for a fine-grained handling of non-imported hints. -**Variants:** - -.. cmd:: Set Loose Hint Behavior "Lax" +.. opt:: Loose Hint Behavior %( "Lax" %| "Warn" %| "Strict" %) - This is the default, and corresponds to the historical behavior, that - is, hints defined outside of a section have a global scope. + This option accepts three values, which control the behavior of hints w.r.t. + :cmd:`Import`: -.. cmd:: Set Loose Hint Behavior "Warn" + - "Lax": this is the default, and corresponds to the historical behavior, + that is, hints defined outside of a section have a global scope. - When set, it outputs a warning when a non-imported hint is used. Note that - this is an over-approximation, because a hint may be triggered by a run that - will eventually fail and backtrack, resulting in the hint not being actually - useful for the proof. + - "Warn": outputs a warning when a non-imported hint is used. Note that this + is an over-approximation, because a hint may be triggered by a run that + will eventually fail and backtrack, resulting in the hint not being + actually useful for the proof. -.. cmd:: Set Loose Hint Behavior "Strict" - - When set, it changes the behavior of an unloaded hint to a immediate fail - tactic, allowing to emulate an import-scoped hint mechanism. + - "Strict": changes the behavior of an unloaded hint to a immediate fail + tactic, allowing to emulate an import-scoped hint mechanism. .. _tactics-implicit-automation: @@ -3734,17 +3719,10 @@ some incompatibilities. Empty_set, unit, True``, :tacn:`dintuition` recognizes also all inductive types with one constructors and no indices, i.e. record-style connectives. -Some aspects of the tactic :tacn:`intuition` can be controlled using options. -To avoid that inner negations which do not need to be unfolded are -unfolded, use: - -.. cmd:: Unset Intuition Negation Unfolding - +.. opt:: Intuition Negation Unfolding -To do that all negations of the goal are unfolded even inner ones -(this is the default), use: - -.. cmd:: Set Intuition Negation Unfolding + Controls whether :tacn:`intuition` unfolds inner negations which do not need + to be unfolded. This option is on by default. .. tacn:: rtauto :name: rtauto @@ -3769,9 +3747,8 @@ usual logical connectives but instead may reason about any first-order class inductive definition. The default tactic used by :tacn:`firstorder` when no rule applies is :g:`auto -with \*`, it can be reset locally or globally using the ``Set Firstorder -Solver`` tactic vernacular command and printed using ``Print Firstorder -Solver``. +with \*`, it can be reset locally or globally using the :opt:`Firstorder Solver` +option and printed using :cmd:`Print Firstorder Solver`. .. tacv:: firstorder @tactic @@ -3792,8 +3769,9 @@ Solver``. This combines the effects of the different variants of :tacn:`firstorder`. -Proof-search is bounded by a depth parameter which can be set by -typing the ``Set Firstorder Depth n`` vernacular command. +.. opt:: Firstorder Depth @natural + + This option controls the proof-search depth bound. .. tacn:: congruence :name: congruence diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index da4034fb8..6a20c0466 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -77,14 +77,11 @@ section. Flags, Options and Tables ----------------------------- -|Coq| configurability is based on flags (e.g. ``Set Printing All`` in -Section :ref:`printing_constructions_full`), options (e.g. ``Set Printing Widthinteger`` in Section -:ref:`controlling-display`), or tables (e.g. ``Add Printing Record ident``, in Section -:ref:`record-types`). -The names of flags, options and tables are made of non-empty sequences of identifiers -(conventionally with capital initial -letter). The general commands handling flags, options and tables are -given below. +|Coq| configurability is based on flags (e.g. :opt:`Printing All`), options +(e.g. :opt:`Printing Width`), or tables (e.g. :cmd:`Add Printing Record`). The +names of flags, options and tables are made of non-empty sequences of +identifiers (conventionally with capital initial letter). The general commands +handling flags, options and tables are given below. .. TODO : flag is not a syntax entry @@ -93,7 +90,6 @@ given below. This command switches :n:`@flag` on. The original state of :n:`@flag` is restored when the current module ends. - Variants: .. cmdv:: Local Set @flag. @@ -256,11 +252,10 @@ See also: Section :ref:`performingcomputations`. .. cmd::Extraction @term. This command displays the extracted term from :n:`@term`. The extraction is -processed according to the distinction between ``Set`` and ``Prop``; that is -to say, between logical and computational content (see Section -:ref:`sorts`). The extracted term is displayed in OCaml -syntax, -where global identifiers are still displayed as in |Coq| terms. +processed according to the distinction between :g:`Set` and :g:`Prop`; that is +to say, between logical and computational content (see Section :ref:`sorts`). +The extracted term is displayed in OCaml syntax, where global identifiers are +still displayed as in |Coq| terms. Variants: @@ -1065,20 +1060,11 @@ expressed in seconds), then it is interrupted and an error message is displayed. -.. cmd:: Set Default Timeout @num. - -After using this command, all subsequent commands behave as if they -were passed to a Timeout command. Commands already starting by a -`Timeout` are unaffected. - - -.. cmd:: Unset Default Timeout. - -This command turns off the use of a default timeout. - -.. cmd:: Test Default Timeout. +.. opt:: Default Timeout @num -This command displays whether some default timeout has been set or not. + This option controls a default timeout for subsequent commands, as if they + were passed to a :cmd:`Timeout` command. Commands already starting by a + :cmd:`Timeout` are unaffected. .. cmd:: Fail @command. @@ -1099,128 +1085,58 @@ Error messages: Controlling display ----------------------- +.. opt:: Silent -.. cmd:: Set Silent. - -This command turns off the normal displaying. - - -.. cmd:: Unset Silent. - -This command turns the normal display on. - -.. todo:: check that spaces are handled well - -.. cmd:: Set Warnings ‘‘(@ident {* , @ident } )’’. - -This command configures the display of warnings. It is experimental, -and expects, between quotes, a comma-separated list of warning names -or categories. Adding - in front of a warning or category disables it, -adding + makes it an error. It is possible to use the special -categories all and default, the latter containing the warnings enabled -by default. The flags are interpreted from left to right, so in case -of an overlap, the flags on the right have higher priority, meaning -that `A,-A` is equivalent to `-A`. - - -.. cmd:: Set Search Output Name Only. - -This command restricts the output of search commands to identifier -names; turning it on causes invocations of ``Search``, ``SearchHead``, -``SearchPattern``, ``SearchRewrite`` etc. to omit types from their output, -printing only identifiers. - - -.. cmd:: Unset Search Output Name Only. - -This command turns type display in search results back on. - - -.. cmd:: Set Printing Width @integer. - -This command sets which left-aligned part of the width of the screen -is used for display. - - -.. cmd:: Unset Printing Width. - -This command resets the width of the screen used for display to its -default value (which is 78 at the time of writing this documentation). - - -.. cmd:: Test Printing Width. - -This command displays the current screen width used for display. - - -.. cmd:: Set Printing Depth @integer. - -This command sets the nesting depth of the formatter used for pretty- -printing. Beyond this depth, display of subterms is replaced by dots. - - -.. cmd:: Unset Printing Depth. - -This command resets the nesting depth of the formatter used for -pretty-printing to its default value (at the time of writing this -documentation, the default value is 50). - - -.. cmd:: Test Printing Depth. - -This command displays the current nesting depth used for display. - - -.. cmd:: Unset Printing Compact Contexts. - -This command resets the displaying of goals contexts to non compact -mode (default at the time of writing this documentation). Non compact -means that consecutive variables of different types are printed on -different lines. - - -.. cmd:: Set Printing Compact Contexts. - -This command sets the displaying of goals contexts to compact mode. -The printer tries to reduce the vertical size of goals contexts by -putting several variables (even if of different types) on the same -line provided it does not exceed the printing width (See Set Printing -Width above). - - -.. cmd:: Test Printing Compact Contexts. - -This command displays the current state of compaction of goal. + This option controls the normal displaying. +.. opt:: Warnings "@ident {* , @ident }" -.. cmd:: Unset Printing Unfocused. + This option configures the display of warnings. It is experimental, and + expects, between quotes, a comma-separated list of warning names or + categories. Adding - in front of a warning or category disables it, adding + + makes it an error. It is possible to use the special categories all and + default, the latter containing the warnings enabled by default. The flags are + interpreted from left to right, so in case of an overlap, the flags on the + right have higher priority, meaning that `A,-A` is equivalent to `-A`. -This command resets the displaying of goals to focused goals only -(default). Unfocused goals are created by focusing other goals with -bullets (see :ref:`bullets`) or curly braces (see `here `). +.. opt:: Search Output Name Only + This option restricts the output of search commands to identifier names; + turning it on causes invocations of :cmd:`Search`, :cmd:`SearchHead`, + :cmd:`SearchPattern`, :cmd:`SearchRewrite` etc. to omit types from their + output, printing only identifiers. -.. cmd:: Set Printing Unfocused. +.. opt:: Printing Width @integer -This command enables the displaying of unfocused goals. The goals are -displayed after the focused ones and are distinguished by a separator. + This command sets which left-aligned part of the width of the screen is used + for display. At the time of writing this documentation, the default value + is 78. +.. opt:: Printing Depth @integer -.. cmd:: Test Printing Unfocused. + This option controls the nesting depth of the formatter used for pretty- + printing. Beyond this depth, display of subterms is replaced by dots. At the + time of writing this documentation, the default value is 50. -This command displays the current state of unfocused goals display. +.. opt:: Printing Compact Contexts + This option controls the compact display mode for goals contexts. When on, + the printer tries to reduce the vertical size of goals contexts by putting + several variables (even if of different types) on the same line provided it + does not exceed the printing width (see :opt:`Printing Width`). At the time + of writing this documentation, it is off by default. -.. cmd:: Set Printing Dependent Evars Line. +.. opt:: Printing Unfocused -This command enables the printing of the “(dependent evars: …)” line -when -emacs is passed. + This option controls whether unfocused goals are displayed. Such goals are + created by focusing other goals with bullets (see :ref:`bullets`) or curly + braces (see `here `). It is off by default. +.. cmd:: Printing Dependent Evars Line -.. cmd:: Unset Printing Dependent Evars Line. + This option controls the printing of the “(dependent evars: …)” line when + ``-emacs`` is passed. -This command disables the printing of the “(dependent evars: …)” line -when -emacs is passed. .. _vernac-controlling-the-reduction-strategies: -- cgit v1.2.3