diff options
| author | Pierre-Marie Pédrot | 2020-09-08 10:37:24 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-09-08 10:37:24 +0200 |
| commit | dde607ce50ddcf5f965d4ce222ca50f4d169a2f3 (patch) | |
| tree | 7f1eb9b6d5af851e776b0a6eb7594eb8b8910c00 /test-suite | |
| parent | edb2cefe61d5f5b3230ab33842e61423ca02fbdb (diff) | |
| parent | e5890700b4574ee9207b2daf6ec95707b9290275 (diff) | |
Merge PR #12954: Fixes a freshness issue with destruct/induction (see comment in #12944).
Ack-by: RalfJung
Ack-by: jashug
Reviewed-by: ppedrot
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/bug_12944.v | 12 | ||||
| -rw-r--r-- | test-suite/success/induct.v | 10 |
2 files changed, 22 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_12944.v b/test-suite/bugs/closed/bug_12944.v new file mode 100644 index 0000000000..d6720d9906 --- /dev/null +++ b/test-suite/bugs/closed/bug_12944.v @@ -0,0 +1,12 @@ + +Inductive vector A : nat -> Type := + |nil : vector A 0 + |cons : forall (h:A) (n:nat), vector A n -> vector A (S n). + +Global Set Mangle Names. + +Lemma vlookup_middle {A n} (v : vector A n) : True. +Proof. + induction v as [|?? IHv]. + all:exact I. +Qed. diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v index 73fe53c757..a39b17e1f1 100644 --- a/test-suite/success/induct.v +++ b/test-suite/success/induct.v @@ -196,3 +196,13 @@ Goal forall m n:nat, n=m. double induction m n. Abort. +(* Mentioned as part of bug #12944 *) + +Inductive test : Set := cons : forall (IHv : nat) (v : test), test. + +Goal test -> test. +induction 1 as [? IHv]. +Undo. +destruct 1 as [? IHv]. +exact IHv. (* Check that the name is granted *) +Qed. |