From f41de34bcd48f008cf7d3fae4c7fce925048e606 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Fri, 2 Oct 2015 21:32:25 +0200
Subject: Mark the Coq.Compat files for documentation. (Fix bug #4353)

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

(limited to 'doc/stdlib')

diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 024e13413a..866193ffb4 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -591,7 +591,7 @@ through the <tt>Require Import</tt> command.</p>
   </dd>
 
   <dt> <b>Program</b>:
-    Support for dependently-typed programming.
+    Support for dependently-typed programming
   </dt>
   <dd>
     theories/Program/Basics.v
@@ -612,4 +612,12 @@ through the <tt>Require Import</tt> command.</p>
     theories/Unicode/Utf8_core.v
     theories/Unicode/Utf8.v
   </dd>
+
+  <dt> <b>Compat</b>:
+    Compatibility wrappers for previous versions of Coq
+  </dt>
+  <dd>
+    theories/Compat/Coq84.v
+    theories/Compat/Coq85.v
+  </dd>
 </dl>
-- 
cgit v1.2.3


From 4bd5dcfeb558f826d90123357a3e5336f96b2213 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 22 Sep 2015 18:45:27 +0200
Subject: Adding an amazing property of Prop.

---
 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 866193ffb4..33de399c0d 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -59,6 +59,7 @@ through the <tt>Require Import</tt> command.</p>
     theories/Logic/WeakFan.v
     theories/Logic/WKL.v
     theories/Logic/FinFun.v
+    theories/Logic/PropFacts.v
   </dd>
 
   <dt> <b>Structures</b>:
-- 
cgit v1.2.3


From 81ef6a6dc1bfc3db0e7df3e32b6446fc4d2c4008 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 14 Dec 2015 11:22:54 +0100
Subject: Moved proof_admitted to its own file, named "AdmitAxiom.v".

---
 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 866193ffb4..292b2b36cc 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -617,6 +617,7 @@ through the <tt>Require Import</tt> command.</p>
     Compatibility wrappers for previous versions of Coq
   </dt>
   <dd>
+    theories/Compat/AdmitAxiom.v
     theories/Compat/Coq84.v
     theories/Compat/Coq85.v
   </dd>
-- 
cgit v1.2.3


From 4b4a4b6b41e6b303d556638ed2a79b1493b1ecf4 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Wed, 13 Jan 2016 17:38:27 +0100
Subject: MMaps: remove it from final 8.5 release, since this new library isn't
 mature enough

 In particular, its interface might still change (in interaction with interested
 colleagues). So let's not give it too much visibility yet. Instead, I'll turn
 it as an opam packages for now.
---
 doc/stdlib/index-list.html.template | 7 -------
 1 file changed, 7 deletions(-)

(limited to 'doc/stdlib')

diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 292b2b36cc..d6b1af797f 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -476,13 +476,6 @@ through the <tt>Require Import</tt> command.</p>
     theories/MSets/MSetPositive.v
     theories/MSets/MSetToFiniteSet.v
     (theories/MSets/MSets.v)
-    theories/MMaps/MMapAVL.v
-    theories/MMaps/MMapFacts.v
-    theories/MMaps/MMapInterface.v
-    theories/MMaps/MMapList.v
-    theories/MMaps/MMapPositive.v
-    theories/MMaps/MMapWeakList.v
-    (theories/MMaps/MMaps.v)
   </dd>
 
   <dt> <b>FSets</b>:
-- 
cgit v1.2.3