diff options
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index ec085a71e5..89668a2d7e 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3976,7 +3976,7 @@ succeeds, and results in an error otherwise. This tactic checks whether its arguments are unifiable, potentially instantiating existential variables. -.. exn:: Not unifiable. +.. exn:: Unable to unify @term with @term. .. tacv:: unify @term @term with @ident |