diff options
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. |