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

1 files changed, 35 insertions, 0 deletions

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.