From 387351b4c0ffeff65d8a7192f5073cfd4bd20f53 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 5 Dec 2015 00:14:37 +0100
Subject: Changing "destruct !hyp" into "destruct (hyp)" (and similarly for
 induction) based on a suggestion of Guillaume M. (done like this in
 ssreflect).

This is actually consistent with the hack of using "destruct (1)" to
mean the term 1 by opposition to the use of "destruct 1" to mean the
first non-dependent hypothesis of the goal.
---
 test-suite/success/destruct.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index 59cd25cd76..9f091e3996 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -389,7 +389,7 @@ Abort.
 
 Goal forall b:bool, True.
 intro b.
-destruct !b.
+destruct (b).
 clear b. (* b has to be here *)
 Abort.
 
-- 
cgit v1.2.3