From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Nov 2015 11:31:34 +0100 Subject: Imported Upstream version 8.5~beta3+dfsg --- test-suite/success/intros.v | 36 ++++++++++++++++++++++++++++++++++++ 1 file changed, 36 insertions(+) (limited to 'test-suite/success/intros.v') diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v index 9443d01e..35ba94fb 100644 --- a/test-suite/success/intros.v +++ b/test-suite/success/intros.v @@ -33,3 +33,39 @@ Goal True -> True -> True. intros _ ?. exact H. Qed. + +(* A short test about introduction pattern pat/c *) +Goal (True -> 0=0) -> True /\ False -> 0=0. +intros H (H1/H,_). +exact H1. +Qed. + +(* A test about bugs in 8.5beta2 *) +Goal (True -> 0=0) -> True /\ False -> False -> 0=0. +intros H H0 H1. +destruct H0 as (a/H,_). +(* Check that H0 is removed (was bugged in 8.5beta2) *) +Fail clear H0. +(* Check position of newly created hypotheses when using pat/c (was + left at top in 8.5beta2) *) +match goal with H:_ |- _ => clear H end. (* clear H1:False *) +match goal with H:_ |- _ => exact H end. (* check that next hyp shows 0=0 *) +Qed. + +Goal (True -> 0=0) -> True -> 0=0. +intros H H1/H. +exact H1. +Qed. + +Goal forall n, n = S n -> 0=0. +intros n H/n_Sn. +destruct H. +Qed. + +(* Another check about generated names and cleared hypotheses with + pat/c patterns *) +Goal (True -> 0=0 /\ 1=1) -> True -> 0=0. +intros H (H1,?)/H. +change (1=1) in H0. +exact H1. +Qed. -- cgit v1.2.3