aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--test-suite/success/apply.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index 24d5cf8a9..074004fa1 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -371,7 +371,7 @@ Qed.
Goal True.
Fail eapply existT.
-Set Trivial Tactic Unification Under Conjunction.
+Set Universal Lemma Under Conjunction.
eapply existT.
Abort.