diff options
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 42 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 61 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 52 |
4 files changed, 122 insertions, 35 deletions
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 0ea8c7be2d..1071682ead 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -1208,7 +1208,7 @@ Interactive debugger .. flag:: Ltac Debug - This option governs the step-by-step debugger that comes with the |Ltac| interpreter + This option governs the step-by-step debugger that comes with the |Ltac| interpreter. When the debugger is activated, it stops at every step of the evaluation of the current |Ltac| expression and prints information on what it is doing. diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 3ca0ffe678..9fbac95f0c 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -157,14 +157,24 @@ compatible with the rest of |Coq|, up to a few discrepancies: (see :ref:`pattern_conditional_ssr`). To use the generalized form, turn off the |SSR| Boolean ``if`` notation using the command: ``Close Scope boolean_if_scope``. -+ The following two options can be unset to disable the incompatible - rewrite syntax and allow reserved identifiers to appear in scripts. ++ The following flags can be unset to make |SSR| more compatible with + parts of Coq: - .. coqtop:: in +.. flag:: SsrRewrite + + Controls whether the incompatible rewrite syntax is enabled (the default). + Disabling the flag makes the syntax compatible with other parts of Coq. + +.. flag:: SsrIdents - Unset SsrRewrite. - Unset SsrIdents. + Controls whether tactics can refer to |SSR|-generated variables that are + in the form _xxx_. Scripts with explicit references to such variables + are fragile; they are prone to failure if the proof is later modified or + if the details of variable name generation change in future releases of Coq. + The default is on, which gives an error message when the user tries to + create such identifiers. Disabling the flag generates a warning instead, + increasing compatibility with other parts of Coq. |Gallina| extensions -------------------- @@ -3063,6 +3073,17 @@ An :token:`r_item` can be: rewrite -[f y x]/(y + _). +.. flag:: SsrOldRewriteGoalsOrder + + Controls the order in which generated subgoals (side conditions) + are added to the + proof context. The flag is off by default, which puts subgoals generated + by conditional rules first, followed by the main goal. When it is on, + the main goal appears first. If your proofs are organized to complete + proving the main goal before side conditions, turning the flag on will save you + from having to add :tacn:`last first` tactics that would be needed + to keep the main goal as the currently focused goal. + Remarks and examples ~~~~~~~~~~~~~~~~~~~~ @@ -5428,6 +5449,17 @@ right hand side double , view hint declaration see :ref:`declaring_new_hints_ssr prenex implicits declaration see :ref:`parametric_polymorphism_ssr` +Settings +~~~~~~~~ + +.. flag:: Debug Ssreflect + + *Developer only.* Print debug information on reflect. + +.. flag:: Debug SsrMatching + + *Developer only.* Print debug information on SSR matching. + .. rubric:: Footnotes .. [#1] Unfortunately, even after a call to the Set Printing All command, diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 150aadc15a..ad80cb62e1 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -264,6 +264,11 @@ Applying theorems This tactic behaves like :tacn:`simple refine` except it performs type checking without resolution of typeclasses. + .. flag:: Debug Unification + + Enables printing traces of unification steps used during + elaboration/typechecking and the :tacn:`refine` tactic. + .. tacn:: apply @term :name: apply @@ -606,6 +611,10 @@ Applying theorems when the instantiation of a variable cannot be found (cf. :tacn:`eapply` and :tacn:`apply`). +.. flag:: Debug Tactic Unification + + Enables printing traces of unification steps in tactic unification. + Tactic unification is used in tactics such as :tacn:`apply` and :tacn:`rewrite`. .. _managingthelocalcontext: @@ -2096,9 +2105,9 @@ and an explanation of the underlying technique. Part of the behavior of the ``inversion`` tactic is to generate 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 - :flag`Keep Proof Equalities`. + relate two proofs (i.e. equalities between :token:`term`\s whose type is in sort + :g:`Prop`). This behavior can be turned off by using the + :flag:`Keep Proof Equalities` setting. .. tacv:: inversion @num @@ -2534,6 +2543,13 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. unresolved bindings into existential variables, if any, instead of failing. It has the same variants as :tacn:`rewrite` has. + .. flag:: Keyed Unification + + Makes higher-order unification used by :tacn:`rewrite` rely on a set of keys to drive + unification. The subterms, considered as rewriting candidates, must start with + the same key as the left- or right-hand side of the lemma given to rewrite, and the arguments + are then unified up to full reduction. + .. tacn:: replace @term with @term’ :name: replace @@ -4503,3 +4519,42 @@ user-defined tactics. significant changes in your theories to obtain the same result. As a drawback of the re-engineering of the code, this tactic has also been completely revised to get a very compact and readable version. + +Delaying solving unification constraints +---------------------------------------- + +.. tacn:: solve_constraints + :name: solve_constraints + :undocumented: + +.. flag:: Solve Unification Constraints + + By default, after each tactic application, postponed typechecking unification + problems are resolved using heuristics. Unsetting this flag disables this + behavior, allowing tactics to leave unification constraints unsolved. Use the + :tacn:`solve_constraints` tactic at any point to solve the constraints. + +Proof maintenance +----------------- + +*Experimental.* Many tactics, such as :tacn:`intros`, can automatically generate names, such +as "H0" or "H1" for a new hypothesis introduced from a goal. Subsequent proof steps +may explicitly refer to these names. However, future versions of Coq may not assign +names exactly the same way, which could cause the proof to fail because the +new names don't match the explicit references in the proof. + +The following "Mangle Names" settings let users find all the +places where proofs rely on automatically generated names, which can +then be named explicitly to avoid any incompatibility. These +settings cause Coq to generate different names, producing errors for +references to automatically generated names. + +.. flag:: Mangle Names + + When set, generated names use the prefix specified in the following + option instead of the default prefix. + +.. opt:: Mangle Names Prefix @string + :name: Mangle Names Prefix + + Specifies the prefix to use when generating names. diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 4bc85f386d..a98a46ba21 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -274,8 +274,8 @@ Requests to the environment This searches for all statements or types of definition that contains a subterm that matches the pattern - `term_pattern` (holes of the pattern are either denoted by `_` or by - `?ident` when non linear patterns are expected). + :token:`term_pattern` (holes of the pattern are either denoted by `_` or by + :n:`?@ident` when non linear patterns are expected). .. cmdv:: Search { + [-]@term_pattern_string } @@ -580,7 +580,7 @@ file is a particular case of module called *library file*. replayed nor rechecked. To locate the file in the file system, :n:`@qualid` is decomposed under the - form `dirpath.ident` and the file `ident.vo` is searched in the physical + form :n:`dirpath.@ident` and the file :n:`@ident.vo` is searched in the physical directory of the file system that is mapped in |Coq| loadpath to the logical path dirpath (see Section :ref:`libraries-and-filesystem`). The mapping between physical directories and logical names at the time of requiring the @@ -611,7 +611,7 @@ file is a particular case of module called *library file*. .. cmdv:: Require [Import | Export] {+ @qualid } This loads the - modules named by the :n:`qualid` sequence and their recursive + modules named by the :token:`qualid` sequence and their recursive dependencies. If ``Import`` or ``Export`` is given, it also imports these modules and all the recursive dependencies that were marked or transitively marked @@ -620,8 +620,8 @@ file is a particular case of module called *library file*. .. cmdv:: From @dirpath Require @qualid This command acts as :cmd:`Require`, but picks - any library whose absolute name is of the form dirpath.dirpath’.qualid - for some `dirpath’`. This is useful to ensure that the :n:`@qualid` library + any library whose absolute name is of the form :n:`@dirpath.@dirpath’.@qualid` + for some :n:`@dirpath’`. This is useful to ensure that the :token:`qualid` library comes from a given package by making explicit its absolute root. .. exn:: Cannot load qualid: no physical path bound to dirpath. @@ -637,21 +637,21 @@ file is a particular case of module called *library file*. The command tried to load library file :n:`@ident`.vo that depends on some specific version of library :n:`@qualid` which is not the - one already loaded in the current |Coq| session. Probably `ident.v` was + one already loaded in the current |Coq| session. Probably :n:`@ident.v` was not properly recompiled with the last version of the file containing - module :n:`@qualid`. + module :token:`qualid`. .. exn:: Bad magic number. - The file `ident.vo` was found but either it is not a + The file :n:`@ident.vo` was found but either it is not a |Coq| compiled module, or it was compiled with an incompatible version of |Coq|. - .. exn:: The file `ident.vo` contains library dirpath and not library dirpath’. + .. exn:: The file :n:`@ident.vo` contains library dirpath and not library dirpath’. - The library file `dirpath’` is indirectly required by the + The library file :n:`@dirpath’` is indirectly required by the ``Require`` command but it is bound in the current loadpath to the - file `ident.vo` which was bound to a different library name `dirpath` at + file :n:`@ident.vo` which was bound to a different library name :token:`dirpath` at the time it was compiled. @@ -675,10 +675,10 @@ file is a particular case of module called *library file*. .. cmd:: Declare ML Module {+ @string } This commands loads the OCaml compiled files - with names given by the :n:`@string` sequence + with names given by the :token:`string` sequence (dynamic link). It is mainly used to load tactics dynamically. The files are searched into the current OCaml loadpath (see the - command ``Add ML Path`` in Section :ref:`libraries-and-filesystem`). + command :cmd:`Add ML Path`). Loading of OCaml files is only possible under the bytecode version of ``coqtop`` (i.e. ``coqtop`` called with option ``-byte``, see chapter :ref:`thecoqcommands`), or when |Coq| has been compiled with a @@ -698,9 +698,9 @@ file is a particular case of module called *library file*. .. cmd:: Print ML Modules - This prints the name of all OCaml modules loaded with ``Declare - ML Module``. To know from where these module were loaded, the user - should use the command ``Locate File`` (see :ref:`here <locate-file>`) + This prints the name of all OCaml modules loaded with :cmd:`Declare ML Module`. + To know from where these module were loaded, the user + should use the command :cmd:`Locate File`. .. _loadpath: @@ -721,7 +721,7 @@ the toplevel, and using them in source files is discouraged. .. cmd:: Cd @string - This command changes the current directory according to :n:`@string` which + This command changes the current directory according to :token:`string` which can be any valid path. .. cmdv:: Cd @@ -732,24 +732,24 @@ the toplevel, and using them in source files is discouraged. .. cmd:: Add LoadPath @string as @dirpath This command is equivalent to the command line option - ``-Q`` :n:`@string` :n:`@dirpath`. It adds the physical directory string to the current + :n:`-Q @string @dirpath`. It adds the physical directory string to the current |Coq| loadpath and maps it to the logical directory dirpath. .. cmdv:: Add LoadPath @string - Performs as Add LoadPath :n:`@string` as :n:`@dirpath` but + Performs as :n:`Add LoadPath @string @dirpath` but for the empty directory path. .. cmd:: Add Rec LoadPath @string as @dirpath This command is equivalent to the command line option - ``-R`` :n:`@string` :n:`@dirpath`. It adds the physical directory string and all its + :n:`-R @string @dirpath`. It adds the physical directory string and all its subdirectories to the current |Coq| loadpath. .. cmdv:: Add Rec LoadPath @string - Works as :cmd:`Add Rec LoadPath` :n:`@string` as :n:`@dirpath` but for the empty + Works as :n:`Add Rec LoadPath @string as @dirpath` but for the empty logical directory path. @@ -792,7 +792,7 @@ the toplevel, and using them in source files is discouraged. .. cmd:: Locate File @string This command displays the location of file string in the current - loadpath. Typically, string is a .cmo or .vo or .v file. + loadpath. Typically, string is a ``.cmo`` or ``.vo`` or ``.v`` file. .. cmd:: Locate Library @dirpath @@ -858,7 +858,7 @@ interactively, they cannot be part of a vernacular file loaded via state label is an integer which grows after each successful command. It is displayed in the prompt when in -emacs mode. Just as :cmd:`Back` (see above), the :cmd:`BackTo` command now handles proof states. For that, it may - have to undo some extra commands and end on a state `num′ ≤ num` if + have to undo some extra commands and end on a state :n:`@num′ ≤ @num` if necessary. .. cmdv:: Backtrack @num @num @num @@ -1157,7 +1157,7 @@ described first. This command allows giving a short name to a reduction expression, for instance lazy beta delta [foo bar]. This short name can then be used - in ``Eval`` :n:`@ident` ``in`` ... or ``eval`` directives. This command + in :n:`Eval @ident in` or ``eval`` directives. This command accepts the Local modifier, for discarding this reduction name at the end of the file or module. For the moment the name cannot be qualified. In @@ -1165,7 +1165,7 @@ described first. functor applications will be refused if these declarations are not local. The name :n:`@ident` cannot be used directly as an Ltac tactic, but nothing prevents the user to also perform a - ``Ltac`` `ident` ``:=`` `convtactic`. + :n:`Ltac @ident := @convtactic`. .. seealso:: :ref:`performingcomputations` |