From 041b8bc806f85114bc3b54101faa84996d6ab50b Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 26 Jun 2014 11:40:25 +0200
Subject: Fix test-suite file for bug # 3036, the unification has _never_
 succeeded, as this would result in an ill-scoped substitution.

---
 test-suite/bugs/closed/3036.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/test-suite/bugs/closed/3036.v b/test-suite/bugs/closed/3036.v
index c1ead05573..451bec9b20 100644
--- a/test-suite/bugs/closed/3036.v
+++ b/test-suite/bugs/closed/3036.v
@@ -165,4 +165,5 @@ Section Stack.
     | None => [False]
     end) * emp.
   Proof.
-    intros. apply himp_ex_conc_trivial.
+    intros. 
+    try apply himp_ex_conc_trivial.
-- 
cgit v1.2.3