From 4e85cc6e9792da116f1b20e484b2ce629c6f6865 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Sun, 2 Oct 2016 20:27:59 +0200
Subject: Adding explicitly a file to work in the context of propositional
 extensionality.

---
 doc/stdlib/index-list.html.template | 1 +
 1 file changed, 1 insertion(+)

(limited to 'doc/stdlib')

diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 4ffdbb115..aeb0de48a 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -56,6 +56,7 @@ through the <tt>Require Import</tt> command.</p>
     theories/Logic/Description.v
     theories/Logic/Epsilon.v
     theories/Logic/IndefiniteDescription.v
+    theories/Logic/PropExtensionality.v
     theories/Logic/PropExtensionalityFacts.v
     theories/Logic/FunctionalExtensionality.v
     theories/Logic/ExtensionalFunctionRepresentative.v
-- 
cgit v1.2.3