From a0ccd7bdc29c35dd291a526891fdbb9909b8e827 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 30 Jun 2014 09:24:00 +0200
Subject: Synchronized names from the "as" clause with the skeleton of the
 elimination scheme in induction/destruct also for those names which
 correspond to neither the induction hypotheses nor the recursive arguments.

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

(limited to 'test-suite')

diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v
index f15bcce8ae..4e20a50774 100644
--- a/test-suite/success/induct.v
+++ b/test-suite/success/induct.v
@@ -64,3 +64,14 @@ Undo 2.
 Fail induction (S _) in |- * at 4.
 Abort.
 
+(* Check use of "as" clause *)
+
+Inductive I := C : forall x, x<0 -> I -> I.
+
+Goal forall x:I, x=x.
+intros.
+induction x as [y * IHx].
+change (x = x) in IHx. (* We should have IHx:x=x *)
+Abort.
+
+
-- 
cgit v1.2.3