diff options
| author | Hugo Herbelin | 2020-08-30 21:44:36 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-08-31 12:33:52 +0200 |
| commit | 4c3064c6e679cfbe4ce13a76b50a17bcfffe4d71 (patch) | |
| tree | 1188f5ae30cf85463cd54e9164eefb6b0dc8166c /test-suite | |
| parent | 94d9fe2b6cb06fe7f862683d8337433e18314001 (diff) | |
Fixes a freshness issue with induction (see comment in #12944).
The names computed in consume_pattern were lost when calling
intros_pattern_core. Moreover, the computation of names to avoid was
done several time. We compute it once for all.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/induct.v | 10 |
1 files changed, 10 insertions, 0 deletions
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. |