diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-09-08 14:19:29 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-09-08 14:19:34 +0200 |
| commit | 7e00e8d602e67810700a7071c419ffd7ef8806c5 (patch) | |
| tree | 0541e014fc1bf128bb13a816c31d1d4ceb18f51c /test-suite/success/intros.v | |
| parent | 11fc2695936c4cff0eea18cb97f6c83eb7cff09d (diff) | |
Fixing incomplete bugfix in 76f27140e6e34 (unfortunately 5 commits
ago) which broke compilation of theories/Logic/WKL.v (collision
between a temporary name and a user name).
Diffstat (limited to 'test-suite/success/intros.v')
| -rw-r--r-- | test-suite/success/intros.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v index 4959b6578..ae1694c58 100644 --- a/test-suite/success/intros.v +++ b/test-suite/success/intros.v @@ -51,3 +51,13 @@ Fail clear H0. 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. |