aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-03-05 16:42:07 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-03-05 16:42:07 +0000
commit93842330896c5940a1456068e72880b6481dcba8 (patch)
tree3ab1880c84e51a06863594ab779ffc2a8e755c67
parent993befdfc914e1a112e4c0beb80e0c5468535a0b (diff)
Restore documentation of library String which was removed in 2007 (r10049)
probably inadvertantly since it is not reported in the commit log. (Thanks to Cédric who noticed it.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13877 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--doc/stdlib/index-list.html.template4
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 1329abcc8..712681856 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -492,13 +492,13 @@ through the <tt>Require Import</tt> command.</p>
theories/FSets/FMapFullAVL.v
</dd>
-<!-- <dt> <b>Strings</b>
+ <dt> <b>Strings</b>
Implementation of string as list of ascii characters
</dt>
<dd>
theories/Strings/Ascii.v
theories/Strings/String.v
- </dd> -->
+ </dd>
<dt> <b>Reals</b>:
Formalization of real numbers