diff options
Diffstat (limited to 'test-suite')
| -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 69d66f1008..af5f994010 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. |