diff options
Diffstat (limited to 'theories/Lists/List.v')
| -rwxr-xr-x | theories/Lists/List.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Lists/List.v b/theories/Lists/List.v index c9052de6c5..528e61ab08 100755 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -(*** THIS IS A OLD CONTRIB. IT IS NO LONGER MAINTAINED ***) +(** THIS IS A OLD CONTRIB. IT IS NO LONGER MAINTAINED ***) Require Le. |