diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-09 23:38:00 +0100 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-10 17:44:19 +0100 |
commit | fb77937a6ba0fe45e978911db08de57f931683e1 (patch) | |
tree | 7a82660e8a0686d4989a615bf5c839ec2e7d8c60 /test-suite/success/intros.v | |
parent | 20e1829ad3de42dd322af972c6f9a585f40738ef (diff) |
Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.
Marking it as experimental.
Diffstat (limited to 'test-suite/success/intros.v')
-rw-r--r-- | test-suite/success/intros.v | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v index 741f372ff..17f160f98 100644 --- a/test-suite/success/intros.v +++ b/test-suite/success/intros.v @@ -34,47 +34,47 @@ intros _ ?. exact H. Qed. -(* A short test about introduction pattern pat/c *) +(* A short test about introduction pattern pat%c *) Goal (True -> 0=0) -> True /\ False -> 0=0. -intros H (H1/H,_). +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,_). +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 +(* 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. +intros H H1%H. exact H1. Qed. Goal forall n, n = S n -> 0=0. -intros n H/n_Sn. +intros n H%n_Sn. destruct H. Qed. (* Another check about generated names and cleared hypotheses with - pat/c patterns *) + pat%c patterns *) Goal (True -> 0=0 /\ 1=1) -> True -> 0=0. -intros H (H1,?)/H. +intros H (H1,?)%H. change (1=1) in H0. exact H1. Qed. -(* Checking iterated pat/c1.../cn introduction patterns and side conditions *) +(* Checking iterated pat%c1...%cn introduction patterns and side conditions *) Goal forall A B C D:Prop, (A -> B -> C) -> (C -> D) -> B -> A -> D. intros * H H0 H1. -intros H2/H/H0. +intros H2%H%H0. - exact H2. - exact H1. Qed. |