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).

1 files changed, 12 insertions, 0 deletions

diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index c6eff3eeb..66629f7fd 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.