diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-02 12:10:53 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-02 18:34:11 +0100 |
| commit | 6ab4479dfa0f9b8fd4df4342fdfdab6c25b62fb7 (patch) | |
| tree | 65ccc8e483adcd60bf1efd3bc3992d045ad90def /test-suite/success/intros.v | |
| parent | cc153dbbe45d5cf7f6ebfef6010adcc4f5bb568c (diff) | |
Improving syntax of pat/constr introduction pattern so that
pat/c1/.../cn behaves as intro H; apply c1, ... , cn in H as pat.
Open to other suggestions of syntax though.
Diffstat (limited to 'test-suite/success/intros.v')
| -rw-r--r-- | test-suite/success/intros.v | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v index 35ba94fb6..741f372ff 100644 --- a/test-suite/success/intros.v +++ b/test-suite/success/intros.v @@ -69,3 +69,12 @@ intros H (H1,?)/H. change (1=1) in H0. exact H1. Qed. + +(* 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. +- exact H2. +- exact H1. +Qed. |