diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-06-30 09:24:00 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-06-30 17:23:10 +0200 |
| commit | a0ccd7bdc29c35dd291a526891fdbb9909b8e827 (patch) | |
| tree | df984988850c92ffe32d0e57edfa482f931675ee /test-suite/success/induct.v | |
| parent | 1f0f842e92be66f67044bdc6deb70676f0ffc22f (diff) | |
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.
Diffstat (limited to 'test-suite/success/induct.v')
| -rw-r--r-- | test-suite/success/induct.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v index f15bcce8a..4e20a5077 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. + + |