From b7e72d0e0ca64168fc16875bf779dbc27d2a1820 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 5 Dec 2015 10:21:33 +0100
Subject: Fix to previous commit (ClassicalFacts.v).

---
 theories/Logic/ClassicalFacts.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v
index f82b00a0dd..d4ebfb42fa 100644
--- a/theories/Logic/ClassicalFacts.v
+++ b/theories/Logic/ClassicalFacts.v
@@ -688,7 +688,7 @@ Section Unrestricted_minimization_entails_excluded_middle.
     apply unrestricted_minimization in h as ([|[|m]] & hm & hmm).
     + intuition.
     + right.
-      intros /p₀/hmm/PeanoNat.Nat.nle_succ_0-HA. assumption.
+      intros HA. apply p₀, hmm, PeanoNat.Nat.nle_succ_0 in HA. assumption.
     + destruct hm as [([=],_) | [=] ].
   Qed.
 
-- 
cgit v1.2.3