diff options
| author | Pierre-Marie Pédrot | 2018-07-24 11:07:04 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-07-24 11:07:04 +0200 |
| commit | ec0e4eb918fc6d95abd5f92b9bea0464662e7245 (patch) | |
| tree | 4a4f41d37605a43e27a58fb2be1540aad0faa592 /doc | |
| parent | 0a00445b113d61a82613f1ba641454b76bd6387c (diff) | |
Update the documentation w.r.t. the new error raised by unify.
Diffstat (limited to 'doc')
| -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 |