Listing a few examples of destruct showing unsatisfactory behaviors.

1 files changed, 36 insertions, 0 deletions

diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index 66629f7fd3..56ec6a02d6 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -289,3 +289,39 @@ destruct H. (* Was not working in 8.4 *)
 change (x=y) in H.
 Abort.
 End S1.
+
+(* These ones are not satisfactory at the current time
+
+Section S2.
+Variable H : 1=1.
+Goal 0=1.
+destruct H.
+(* Should expand the n... *)
+  n := 1 : nat
+  H : n = n
+  ============================
+   0 = n
+*)
+Abort.
+End S2.
+
+(* Should expand the n... *)
+Goal 1=1->0=1.
+intro H.
+destruct H.
+(*
+  n := 1 : nat
+  ============================
+   0 = n
+*)
+
+(* Should expand the x0... *)
+Goal forall x:nat, x=x->x=1.
+intros x H.
+destruct H.
+(*
+  x : nat
+  x0 := x : nat
+  ============================
+   x0=1
+*)