aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-10-06 07:02:24 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-03-03 14:40:31 +0100
commit7497d4129775d15cdce862a0ac681c6400aabe54 (patch)
tree534649a6dca0cea29028e657c4cbe55838f9fac6 /doc
parenta0bd33bdb81271025494d3f7ac7ae20bd6671579 (diff)
Logic library: Adding a characterization of excluded-middle in term of
choice of a representative in a partition of bool. Also move a result about propositional extensionality from ClassicalFacts.v to PropExtensionalityFacts.v, generalizing it by symmetry. Also spotting typos (thanks to Théo).
Diffstat (limited to 'doc')
-rw-r--r--doc/stdlib/index-list.html.template1
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 9216c81fc..4a685a3b8 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -55,6 +55,7 @@ through the <tt>Require Import</tt> command.</p>
theories/Logic/Description.v
theories/Logic/Epsilon.v
theories/Logic/IndefiniteDescription.v
+ theories/Logic/PropExtensionalityFacts.v
theories/Logic/FunctionalExtensionality.v
theories/Logic/ExtensionalityFacts.v
theories/Logic/WeakFan.v