diff options
Diffstat (limited to 'test-suite/bugs/closed/4746.v')
| -rw-r--r-- | test-suite/bugs/closed/4746.v | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4746.v b/test-suite/bugs/closed/4746.v new file mode 100644 index 00000000..d64cc6fe --- /dev/null +++ b/test-suite/bugs/closed/4746.v @@ -0,0 +1,14 @@ +Variables P Q : nat -> Prop. +Variable f : nat -> nat. + +Goal forall (x:nat), (forall y, P y -> forall z, Q z -> y=f z -> False) -> False. +Proof. +intros. +ecase H with (3:=eq_refl). +Abort. + +Goal forall (x:nat), (forall y, y=x -> False) -> False. +Proof. +intros. +unshelve ecase H with (1:=eq_refl). +Qed. |