From ca609f7ea0653a282a81e5d4f9392b1c05a03d8f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 6 Nov 2014 11:29:10 +0100
Subject: Restoring clear_flag (thanks a lot to jonikelee to notice it).

---
 test-suite/success/destruct.v | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index c74bda2a9b..f5848ffe0e 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -377,6 +377,14 @@ intros.
 Fail destruct H.
 Abort.
 
+(* Check keep option (bug #3791) *)
+
+Goal forall b:bool, True.
+intro b.
+destruct !b.
+clear b. (* b has to be here *)
+Abort.
+
 (* Check clearing of names *)
 
 Inductive IND2 : nat -> Prop := CONSTR2 : forall y, y = y -> IND2 y.
-- 
cgit v1.2.3