From 7e00e8d602e67810700a7071c419ffd7ef8806c5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 8 Sep 2015 14:19:29 +0200
Subject: 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).

---
 test-suite/success/intros.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v
index 4959b65788..ae1694c58c 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.
-- 
cgit v1.2.3