diff options
| author | letouzey | 2009-09-28 15:04:07 +0000 |
|---|---|---|
| committer | letouzey | 2009-09-28 15:04:07 +0000 |
| commit | 4d90c1983907ff3ea8a5a8c4dca1dba57c5bf3f8 (patch) | |
| tree | e80307fb09a9836c5dd17f16b412e85fa25b6818 /theories/FSets/FMapPositive.v | |
| parent | aac58d6a2a196ac20da147034ac89546c1c236fe (diff) | |
Fix the stdlib doc compilation + switch all .v file to utf8
1) compilation of Library.tex was failing on a "Ext_" in Diaconescu.v
In fact coqdoc was trying to recognize the end of a _emphasis_ and
hence inserted a bogus }. For the moment I've enclosed the phrase
with [ ], but this emphasis "feature" of coqdoc seems _really_
easy to broke. Matthieu ?
2) By the way, this Library document was made from latin1 and utf8
source file, hence bogus characters. All .v containing special
characters are converted to utf8, and their first line is now
mentionning this. (+ killed some old french comments and some
other avoidable special characters).
PLEASE: let's stick to this convention and avoid latin1, at least
in .v files.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12363 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/FSets/FMapPositive.v')
| -rw-r--r-- | theories/FSets/FMapPositive.v | 14 |
1 files changed, 4 insertions, 10 deletions
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v index 112ccce30a..da5b358744 100644 --- a/theories/FSets/FMapPositive.v +++ b/theories/FSets/FMapPositive.v @@ -6,13 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* Finite sets library. - * Authors: Pierre Letouzey and Jean-Christophe Filliâtre - * Institution: LRI, CNRS UMR 8623 - Université Paris Sud - * 91405 Orsay, France *) - (* $Id$ *) +(** * FMapPositive : an implementation of FMapInterface for [positive] keys. *) + Require Import Bool. Require Import ZArith. Require Import OrderedType. @@ -20,17 +17,14 @@ Require Import OrderedTypeEx. Require Import FMapInterface. Set Implicit Arguments. - Open Local Scope positive_scope. -(** * An implementation of [FMapInterface.S] for positive keys. *) - (** This file is an adaptation to the [FMap] framework of a work by Xavier Leroy and Sandrine Blazy (used for building certified compilers). Keys are of type [positive], and maps are binary trees: the sequence of binary digits of a positive number corresponds to a path in such a tree. - This is quite similar to the [IntMap] library, except that no path compression - is implemented, and that the current file is simple enough to be + This is quite similar to the [IntMap] library, except that no path + compression is implemented, and that the current file is simple enough to be self-contained. *) (** Even if [positive] can be seen as an ordered type with respect to the |