diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-28 15:04:07 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-28 15:04:07 +0000 |
commit | 4d90c1983907ff3ea8a5a8c4dca1dba57c5bf3f8 (patch) | |
tree | e80307fb09a9836c5dd17f16b412e85fa25b6818 /theories/Classes/Morphisms.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/Classes/Morphisms.v')
-rw-r--r-- | theories/Classes/Morphisms.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index 55aad6e73..656b9d74e 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-name: "~/research/coq/trunk/bin/coqtop.byte"; coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.Morphisms"); compile-command: "make -C ../.. TIME='time -p'" -*- *) +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -7,11 +7,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Typeclass-based morphism definition and standard, minimal instances. +(** * Typeclass-based morphism definition and standard, minimal instances Author: Matthieu Sozeau - Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud - 91405 Orsay, France *) + Institution: LRI, CNRS UMR 8623 - University Paris Sud +*) (* $Id$ *) @@ -26,8 +26,8 @@ Require Export Coq.Classes.RelationClasses. These will be used by the [setoid_rewrite] tactic later. *) (** A morphism for a relation [R] is a proper element of the relation. - The relation [R] will be instantiated by [respectful] and [A] by an arrow type - for usual morphisms. *) + The relation [R] will be instantiated by [respectful] and [A] by an arrow + type for usual morphisms. *) Class Proper {A} (R : relation A) (m : A) : Prop := proper : R m m. |