Skip to content

Commit 9969af4

Browse files
committed
Warn about duplicated file names
1 parent 84fd979 commit 9969af4

File tree

1 file changed

+2
-0
lines changed

1 file changed

+2
-0
lines changed

doc/stdlib/index-list.html.template

+2
Original file line numberDiff line numberDiff line change
@@ -40,6 +40,7 @@ through the <tt>Require Import</tt> command.</p>
4040

4141
<dt> <b>Program</b>:
4242
Support for dependently-typed programming in namespace Stdlib.Program.
43+
Beware that there are also Tactics.v and Wf.v files in Init.
4344
</dt>
4445
<dd>
4546
theories/Program/All/Subset.v
@@ -359,6 +360,7 @@ through the <tt>Require Import</tt> command.</p>
359360
<dt> <b>Strings</b>
360361
Implementation of string as list of ASCII characters,
361362
in namespace Stdlib.Strings.
363+
Beware that there is also a Byte.v file in Init.
362364
</dt>
363365
<dd>
364366
theories/Strings/Byte.v

0 commit comments

Comments
 (0)