From 47828f078ac7359e8e2e1891bc6ef48812bb73a5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 27 Oct 2014 08:03:01 +0100
Subject: Ensuring compatibility when an hypothesis used for destruct is
 dependent in the goal without being fully applied: it cannot be erased. This
 used to work in 8.4 when the hypothesis was in an empty type. I fixed this
 and (somehow arbitrarily) generalized the non-erasing to other inductive
 types instead of failing.

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

(limited to 'test-suite')

diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index 26dab73ef6..4704a08e59 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -235,3 +235,20 @@ intro a.
 destruct a.
 change (0 = a 1).
 Abort.
+
+(* This example of a variable not fully applied in the goal was working in 8.4*)
+
+Goal forall H : 0<>0, H = H.
+destruct H.
+reflexivity.
+Qed.
+
+(* Check that variables not fully applied in the goal are not erased
+   (this example was failing in 8.4 because of a forbidden "clear H" in
+   the code of "destruct H" *)
+
+Goal forall H : True -> True, H = H.
+destruct H.
+- exact I.
+- reflexivity.
+Qed.
-- 
cgit v1.2.3