diff options
| author | Hugo Herbelin | 2018-07-25 17:29:16 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-07-25 17:29:16 +0200 |
| commit | 6f52f7bce0de9ac58142b05e17b5dc380fc169e7 (patch) | |
| tree | 7357f0850eb60fe532fce4831910f1896af5c078 | |
| parent | 523de4f878293cf1d582bd70300b34d497e705b3 (diff) | |
Doc: preliminary work before #7291 which add an "Unable to unify" message.
We adopt the convention that error messages with a template use the
sphinx syntax used in defining syntax rules.
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 9b4d724e02..306673d9a2 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -281,7 +281,7 @@ Applying theorems :g:`t`:sub:`n` in the goal. See :tacn:`pattern` to transform the goal so that it gets the form :g:`(fun x => Q) u`:sub:`1` :g:`...` :g:`u`:sub:`n`. - .. exn:: Unable to unify ... with ... . + .. exn:: Unable to unify @term with @term. The apply tactic failed to match the conclusion of :token:`term` and the current goal. You can help the apply tactic by transforming your goal with @@ -3935,7 +3935,7 @@ match against it. discriminable equality but this proof could not be built in Coq because of dependently-typed functions. -.. exn:: Goal is solvable by congruence but some arguments are missing. Try congruence with ..., replacing metavariables by arbitrary terms. +.. exn:: Goal is solvable by congruence but some arguments are missing. Try congruence with {+ @term}, replacing metavariables by arbitrary terms. The decision procedure could solve the goal with the provision that additional arguments are supplied for some partially applied constructors. Any term of an |