diff options
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 526a7d3bf..238e56197 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3903,9 +3903,10 @@ match against it. hypotheses using assert in order for :tacn:`congruence` to use them. .. tacv:: congruence with {+ @term} + :name: congruence with - Adds :n:`{+ @term}` to the pool of terms used by :tacn:`congruence`. This helps - in case you have partially applied constructors in your goal. + Adds :n:`{+ @term}` to the pool of terms used by :tacn:`congruence`. This helps + in case you have partially applied constructors in your goal. .. exn:: I don’t know how to handle dependent equality @@ -3919,7 +3920,7 @@ match against it. arguments are supplied for some partially applied constructors. Any term of an appropriate type will allow the tactic to successfully solve the goal. Those additional arguments can be given to congruence by filling in the holes in the - terms given in the error message, using the with variant described above. + terms given in the error message, using the :tacn:`congruence with` variant described above. .. opt:: Congruence Verbose |