diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 0d32ed46f7..ad44171daa 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3424,7 +3424,7 @@ let intros_symmetry = (* Transitivity tactics *) -(* This tactic first tries to apply a constant named trans_eq, where eq +(* This tactic first tries to apply a constant named eq_trans, where eq is the name of the equality predicate. If this constant is not defined and the conclusion is a=b, it solves the goal doing Cut x1=x2; |