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

4 files changed, 13 insertions, 10 deletions

diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v
index c54756881..0a4b15d29 100644
--- a/theories/Program/Basics.v
+++ b/theories/Program/Basics.v
@@ -1,3 +1,4 @@
+(* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -9,11 +10,12 @@
 
 (** Standard functions and combinators.
 
-   Proofs about them require functional extensionality and can be found in [Combinators].
+   Proofs about them require functional extensionality and can be found
+   in [Combinators].
 
    Author: Matthieu Sozeau
-   Institution: LRI, CNRS UMR 8623 - Université Paris Sud
-   91405 Orsay, France *)
+   Institution: LRI, CNRS UMR 8623 - University Paris Sud
+*)
 
 (** The polymorphic identity function is defined in [Datatypes]. *)
 
diff --git a/theories/Program/Combinators.v b/theories/Program/Combinators.v
index e12f57668..31661b9d3 100644
--- a/theories/Program/Combinators.v
+++ b/theories/Program/Combinators.v
@@ -1,3 +1,4 @@
+(* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -7,11 +8,11 @@
 (************************************************************************)
 (* $Id$ *)
 
-(** Proofs about standard combinators, exports functional extensionality.
+(** * Proofs about standard combinators, exports functional extensionality.
 
    Author: Matthieu Sozeau
-   Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
-   91405 Orsay, France *)
+   Institution: LRI, CNRS UMR 8623 - University Paris Sud
+*)
 
 Require Import Coq.Program.Basics.
 Require Export FunctionalExtensionality.
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 381a0bae4..ca65f3bbe 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-name: "~/research/coq/trunk/bin/coqtop.byte"; coq-prog-args: ("-emacs-U"); compile-command: "make -C ../.. TIME='time'" -*- *)
+(* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v
index 9828d4b69..aff2da946 100644
--- a/theories/Program/Syntax.v
+++ b/theories/Program/Syntax.v
@@ -10,10 +10,10 @@
 (** Custom notations and implicits for Coq prelude definitions.
 
    Author: Matthieu Sozeau
-   Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
-   91405 Orsay, France *)
+   Institution: LRI, CNRS UMR 8623 - University Paris Sud
+*)
 
-(** Notations for the unit type and value à la Haskell. *)
+(** Haskell-style notations for the unit type and value. *)
 
 Notation " () " := Datatypes.unit : type_scope.
 Notation " () " := tt.