diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-02-18 19:55:35 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-02-18 19:58:08 +0100 |
| commit | e28be21112c174a4c1a84d45a50745f0ad4e646a (patch) | |
| tree | f24c4886d2ae4942092abb945a6adc81ffbcc563 /test-suite/success/intros.v | |
| parent | 9e585d7479af0db837528a2fe2ce1690e22a36cb (diff) | |
Fixing a bug with introduction patterns over inductive types containing let-ins.
Diffstat (limited to 'test-suite/success/intros.v')
| -rw-r--r-- | test-suite/success/intros.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v index 69d66f100..af5f99401 100644 --- a/test-suite/success/intros.v +++ b/test-suite/success/intros.v @@ -98,3 +98,10 @@ intros x ->. - reflexivity. - exact I. Qed. + +(* Fixing a bug when destructing a type with let-ins in the constructor *) + +Inductive I := C : let x:=1 in x=1 -> I. +Goal I -> True. +intros [x H]. (* Was failing in 8.5 *) +Abort. |