diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-09-16 21:44:47 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-09-16 22:05:15 +0200 |
| commit | 16db94e6c142217a81cc78be8788137617c24de7 (patch) | |
| tree | c52543ec1759d53f3bc14ca28f789d5bae9846b5 /test-suite/success/intros.v | |
| parent | 498cbad3e5e5d69d2ee771f90de45c0fe28cc494 (diff) | |
In pat/constr introduction patterns, fixing in a better way clearing problems
of temporary hypotheses than 76f27140e6e34 did.
Diffstat (limited to 'test-suite/success/intros.v')
| -rw-r--r-- | test-suite/success/intros.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v index ae1694c58..35ba94fb6 100644 --- a/test-suite/success/intros.v +++ b/test-suite/success/intros.v @@ -61,3 +61,11 @@ 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. |