From c236b51348d2a39d8f105ef0c4e8a53fabc6e285 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Tue, 15 Jul 2014 18:15:26 +0200
Subject: Added a (constructive) proof of Weak Konig's lemma for decidable
 trees. Renamed Fan.v into WeakFan.v since this was a proof of Weak Fan
 Theorem after all.

---
 doc/stdlib/index-list.html.template | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'doc/stdlib')

diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index c3b2aad58..75b5e7fea 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -68,7 +68,8 @@ through the <tt>Require Import</tt> command.</p>
     theories/Logic/IndefiniteDescription.v
     theories/Logic/FunctionalExtensionality.v
     theories/Logic/ExtensionalityFacts.v
-    theories/Logic/Fan.v
+    theories/Logic/WeakFan.v
+    theories/Logic/WKL.v
     theories/Logic/FinFun.v
   </dd>
     
-- 
cgit v1.2.3