From 29a5127dac6d4fbc317e38452cf0fe05916adc56 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 26 Oct 2014 14:23:00 +0100
Subject: Fixing destruct/induction with a using clause on a non-inductive
 type, that was broken by commit bf01856940 + use types from induction scheme
 to restrict selection of pattern + accept matching from partially applied
 term when using "using".

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

(limited to 'test-suite')

diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index 314b612e1c..a3b4b192ee 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -200,3 +200,38 @@ edestruct (H _ _).
 - apply (eq_refl x).
 Qed.
 *)
+Abort.
+
+(* Test selection when not in an inductive type *)
+Parameter A:Type.
+Axiom elim: forall P, A -> P.
+Goal forall a:A, a = a.
+induction a using elim.
+Qed.
+
+Goal forall a:nat -> A, a 0 = a 1.
+intro a.
+induction (a 0) using elim.
+Qed.
+
+(* From Oct 2014, a subterm is found, as if without "using"; in 8.4,
+   it did not find a subterm *)
+
+Goal forall a:nat -> A, a 0 = a 1.
+intro a.
+induction a using elim.
+Qed.
+
+Goal forall a:nat -> A, forall b, a 0 = b.
+intros a b.
+induction a using elim.
+Qed.
+
+(* From Oct 2014, first subterm is found; in 8.4, it failed because it
+   found "a 0" and wanted to clear a *)
+
+Goal forall a:nat -> nat, a 0 = a 1.
+intro a.
+destruct a.
+change (0 = a 1).
+Abort.
-- 
cgit v1.2.3