From b2e1d4ea930c07ca27168fb43908a32d1101fce0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 30 Oct 2014 13:23:10 +0100
Subject: Avoid "destruct H" to apply on H itself when H is a section variable.

Need some contorsion for not using the general scheme of naming based
which uses the hypothesis name as base ident, and for instead keeping
a name generated on the type of the section variable, as it was before
for section variables (example of incompatibility in FMapPositive).
---
 test-suite/success/destruct.v | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index c6eff3eebe..66629f7fd3 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -277,3 +277,15 @@ Abort.
 Goal forall f : A -> nat -> nat, f a 0 = f a 1.
 intros.
 destruct f.
+
+(* This one was not working in 8.4 *)
+
+Section S1.
+Variables x y : Type.
+Variable H : x = y.
+Goal True.
+destruct H. (* Was not working in 8.4 *)
+(* Now check that H statement has not be itself subject of the rewriting *)
+change (x=y) in H.
+Abort.
+End S1.
-- 
cgit v1.2.3