From 47b4573a77ef88f8528c8247108eba8b04d81525 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 2 Aug 2015 18:47:08 +0200
Subject: Fixing test apply.v (had wrong option name).

---
 test-suite/success/apply.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index 24d5cf8a99..074004fa12 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.
 
-- 
cgit v1.2.3