From 2b26c3e9a011af1f77e4f4fc61c73943d2bb0dfc Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 2 Oct 2014 15:47:14 +0200
Subject: Fixing bug #2810 (autounfold on local variable declared as hint but
 cleared).

---
 test-suite/bugs/closed/2810.v | 1 +
 1 file changed, 1 insertion(+)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/2810.v b/test-suite/bugs/closed/2810.v
index 9e33e49162..a66078c60a 100644
--- a/test-suite/bugs/closed/2810.v
+++ b/test-suite/bugs/closed/2810.v
@@ -6,4 +6,5 @@ Section foo.
 
   Goal False.
     clear B. autounfold with core.
+  Abort.
 End foo.
-- 
cgit v1.2.3