diff options
| author | Théo Zimmermann | 2018-07-28 19:36:54 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-07-28 19:36:54 +0200 |
| commit | f416349d504dcdd3a5744c85ab4554f2f6989ebf (patch) | |
| tree | 9a4efb346763a70863d07085b28f30ee48e315fd /doc | |
| parent | 3c41245404eacd105c0dbcae78f47ba103131788 (diff) | |
| parent | 6f52f7bce0de9ac58142b05e17b5dc380fc169e7 (diff) | |
Merge PR #8148: Doc: preliminary work before #7291 which add an "Unable to unify" message
Diffstat (limited to 'doc')
| -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 |