diff options
Diffstat (limited to 'test-suite/success/intros.v')
-rw-r--r-- | test-suite/success/intros.v | 44 |
1 files changed, 44 insertions, 0 deletions
diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v index 11156aa0..ee69df97 100644 --- a/test-suite/success/intros.v +++ b/test-suite/success/intros.v @@ -84,3 +84,47 @@ Qed. Goal forall x : nat, True. intros y%(fun x => x). Abort. + +(* Fixing a bug in the order of side conditions of a "->" step *) + +Goal (True -> 1=0) -> 1=1. +intros ->. +- reflexivity. +- exact I. +Qed. + +Goal forall x, (True -> x=0) -> 0=x. +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. + +(* Ensuring that the (pat1,...,patn) intropatterns has the expected size, up + to skipping let-ins *) + +Goal I -> 1=1. +intros (H). (* This skips x *) +exact H. +Qed. + +Goal I -> 1=1. +Fail intros (x,H,H'). +Fail intros [|]. +intros (x,H). +exact H. +Qed. + +Goal Acc le 0 -> True. +Fail induction 1 as (n,H). (* Induction hypothesis is missing *) +induction 1 as (n,H,IH). +exact Logic.I. +Qed. + + |