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 | |
| 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
56 files changed, 232 insertions, 235 deletions
diff --git a/Makefile.doc b/Makefile.doc index 3da6e10b8..49b377ef7 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -189,14 +189,14 @@ ifdef QUICK doc/stdlib/index-body.html: - rm -rf doc/stdlib/html $(MKDIR) doc/stdlib/html - $(COQDOC) -q -boot -d doc/stdlib/html --multi-index --html -g \ + $(COQDOC) -q -boot -d doc/stdlib/html --multi-index --html -g --utf8 \ -R theories Coq $(THEORIESVO:.vo=.v) mv doc/stdlib/html/index.html doc/stdlib/index-body.html else doc/stdlib/index-body.html: $(COQDOC) $(THEORIESVO) - rm -rf doc/stdlib/html $(MKDIR) doc/stdlib/html - $(COQDOC) -q -boot -d doc/stdlib/html --multi-index --html -g \ + $(COQDOC) -q -boot -d doc/stdlib/html --multi-index --html -g --utf8 \ -R theories Coq $(THEORIESVO:.vo=.v) mv doc/stdlib/html/index.html doc/stdlib/index-body.html endif @@ -213,11 +213,11 @@ doc/stdlib/html/index.html: doc/stdlib/index-list.html doc/stdlib/index-body.htm ifdef QUICK doc/stdlib/Library.coqdoc.tex: - $(COQDOC) -q -boot --gallina --body-only --latex --stdout \ + $(COQDOC) -q -boot --gallina --body-only --latex --stdout --utf8 \ -R theories Coq $(THEORIESLIGHTVO:.vo=.v) >> $@ else doc/stdlib/Library.coqdoc.tex: $(COQDOC) $(THEORIESLIGHTVO) - $(COQDOC) -q -boot --gallina --body-only --latex --stdout \ + $(COQDOC) -q -boot --gallina --body-only --latex --stdout --utf8 \ -R theories Coq $(THEORIESLIGHTVO:.vo=.v) >> $@ endif diff --git a/doc/stdlib/Library.tex b/doc/stdlib/Library.tex index 8a5c7ab76..f5509c3a3 100755 --- a/doc/stdlib/Library.tex +++ b/doc/stdlib/Library.tex @@ -1,6 +1,6 @@ \documentclass[11pt]{report} -\usepackage[latin1]{inputenc} +\usepackage[utf8x]{inputenc} \usepackage[T1]{fontenc} \usepackage{fullpage} \usepackage[color]{../../coqdoc} diff --git a/plugins/micromega/Refl.v b/plugins/micromega/Refl.v index c86fe8fb6..3b0de76b4 100644 --- a/plugins/micromega/Refl.v +++ b/plugins/micromega/Refl.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 *) @@ -8,7 +9,7 @@ (* *) (* Micromega: A reflexive tactic using the Positivstellensatz *) (* *) -(* Frédéric Besson (Irisa/Inria) 2006-2008 *) +(* Frédéric Besson (Irisa/Inria) 2006-2008 *) (* *) (************************************************************************) diff --git a/plugins/micromega/VarMap.v b/plugins/micromega/VarMap.v index c0b86f5ed..0a66fce35 100644 --- a/plugins/micromega/VarMap.v +++ b/plugins/micromega/VarMap.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 *) @@ -8,7 +9,7 @@ (* *) (* Micromega: A reflexive tactic using the Positivstellensatz *) (* *) -(* Frédéric Besson (Irisa/Inria) 2006-2008 *) +(* Frédéric Besson (Irisa/Inria) 2006-2008 *) (* *) (************************************************************************) diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v index 2682a8848..19b6a8164 100644 --- a/theories/Bool/Bvector.v +++ b/theories/Bool/Bvector.v @@ -17,33 +17,33 @@ Require Import Arith. Open Local Scope nat_scope. (** -On s'inspire de List.v pour fabriquer les vecteurs de bits. -La dimension du vecteur est un paramètre trop important pour -se contenter de la fonction "length". -La première idée est de faire un record avec la liste et la longueur. -Malheureusement, cette verification a posteriori amene a faire -de nombreux lemmes pour gerer les longueurs. -La seconde idée est de faire un type dépendant dans lequel la -longueur est un paramètre de construction. Cela complique un -peu les inductions structurelles et dans certains cas on -utilisera un terme de preuve comme définition, car le -mécanisme d'inférence du type du filtrage n'est pas toujours -aussi puissant que celui implanté par les tactiques d'élimination. +We build bit vectors in the spirit of List.v. +The size of the vector is a parameter which is too important +to be accessible only via function "length". +The first idea is to build a record with both the list and the length. +Unfortunately, this a posteriori verification leads to +numerous lemmas for handling lengths. +The second idea is to use a dependent type in which the length +is a building parameter. This leads to structural induction that +are slightly more complex and in some cases we will use a proof-term +as definition, since the type inference mechanism for pattern-matching +is sometimes weaker that the one implemented for elimination tactiques. *) Section VECTORS. (** -Un vecteur est une liste de taille n d'éléments d'un ensemble A. -Si la taille est non nulle, on peut extraire la première composante et -le reste du vecteur, la dernière composante ou rajouter ou enlever -une composante (carry) ou repeter la dernière composante en fin de vecteur. -On peut aussi tronquer le vecteur de ses p dernières composantes ou -au contraire l'étendre (concaténer) d'un vecteur de longueur p. -Une fonction unaire sur A génère une fonction des vecteurs de taille n -dans les vecteurs de taille n en appliquant f terme à terme. -Une fonction binaire sur A génère une fonction des couples de vecteurs -de taille n dans les vecteurs de taille n en appliquant f terme à terme. +A vector is a list of size n whose elements belongs to a set A. +If the size is non-zero, we can extract the first component and the +rest of the vector, as well as the last component, or adding or +removing a component (carry) or repeating the last component at the +end of the vector. +We can also truncate the vector and remove its p last components or +reciprocally extend the vector by concatenation. +A unary function over A generates a function on vectors of size n by +applying f pointwise. +A binary function over A generates a function on pairs of vectors of +size n by applying f pointwise. *) Variable A : Type. @@ -188,15 +188,16 @@ Implicit Arguments Vcons [A n]. Section BOOLEAN_VECTORS. (** -Un vecteur de bits est un vecteur sur l'ensemble des booléens de longueur fixe. -ATTENTION : le stockage s'effectue poids FAIBLE en tête. -On en extrait le bit de poids faible (head) et la fin du vecteur (tail). -On calcule la négation d'un vecteur, le et, le ou et le xor bit à bit de 2 vecteurs. -On calcule les décalages d'une position vers la gauche (vers les poids forts, on -utilise donc Vshiftout, vers la droite (vers les poids faibles, on utilise Vshiftin) en -insérant un bit 'carry' (logique) ou en répétant le bit de poids fort (arithmétique). -ATTENTION : Tous les décalages prennent la taille moins un comme paramètre -(ils ne travaillent que sur des vecteurs au moins de longueur un). +A bit vector is a vector over booleans. +Notice that the LEAST significant bit comes first (little-endian representation). +We extract the least significant bit (head) and the rest of the vector (tail). +We compute bitwise operation on vector: negation, and, or, xor. +We compute size-preserving shifts: to the left (towards most significant bits, +we hence use Vshiftout) and to the right (towards least significant bits, +we use Vshiftin) by inserting a 'carry' bit (logical shift) or by repeating +the most significant bit (arithmetical shift). +NOTA BENE: all shift operations expect predecessor of size as parameter +(they only work on non-empty vectors). *) Definition Bvector := vector bool. diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v index 4b9b26384..e87482d84 100644 --- a/theories/Classes/EquivDec.v +++ b/theories/Classes/EquivDec.v @@ -6,11 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Decidable equivalences. - * - * Author: Matthieu Sozeau - * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud - * 91405 Orsay, France *) +(** * Decidable equivalences. + + Author: Matthieu Sozeau + Institution: LRI, CNRS UMR 8623 - University Paris Sud +*) (* $Id$ *) @@ -18,8 +18,8 @@ Require Export Coq.Classes.Equivalence. -(** The [DecidableSetoid] class asserts decidability of a [Setoid]. It can be useful in proofs to reason more - classically. *) +(** The [DecidableSetoid] class asserts decidability of a [Setoid]. + It can be useful in proofs to reason more classically. *) Require Import Coq.Logic.Decidable. Require Import Coq.Bool.Bool. @@ -31,13 +31,15 @@ Open Scope equiv_scope. Class DecidableEquivalence `(equiv : Equivalence A) := setoid_decidable : forall x y : A, decidable (x === y). -(** The [EqDec] class gives a decision procedure for a particular setoid equality. *) +(** The [EqDec] class gives a decision procedure for a particular + setoid equality. *) Class EqDec A R {equiv : Equivalence R} := equiv_dec : forall x y : A, { x === y } + { x =/= y }. -(** We define the [==] overloaded notation for deciding equality. It does not take precedence - of [==] defined in the type scope, hence we can have both at the same time. *) +(** We define the [==] overloaded notation for deciding equality. It does not + take precedence of [==] defined in the type scope, hence we can have both + at the same time. *) Notation " x == y " := (equiv_dec (x :>) (y :>)) (no associativity, at level 70) : equiv_scope. @@ -70,13 +72,14 @@ Infix "<>b" := nequiv_decb (no associativity, at level 70). (** Decidable leibniz equality instances. *) -(** The equiv is burried inside the setoid, but we can recover it by specifying which setoid we're talking about. *) +(** The equiv is burried inside the setoid, but we can recover it by specifying + which setoid we're talking about. *) Program Instance nat_eq_eqdec : EqDec nat eq := eq_nat_dec. Program Instance bool_eqdec : EqDec bool eq := bool_dec. -Program Instance unit_eqdec : EqDec unit eq := λ x y, in_left. +Program Instance unit_eqdec : EqDec unit eq := fun x y => in_left. Next Obligation. Proof. @@ -105,8 +108,8 @@ Program Instance sum_eqdec `(EqDec A eq, EqDec B eq) : | inl _, inr _ | inr _, inl _ => in_right end }. -(** Objects of function spaces with countable domains like bool have decidable equality. - Proving the reflection requires functional extensionality though. *) +(** Objects of function spaces with countable domains like bool have decidable + equality. Proving the reflection requires functional extensionality though. *) Program Instance bool_function_eqdec `(EqDec A eq) : ! EqDec (bool -> A) eq := { equiv_dec f g := diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v index aa20ebd49..78e66d374 100644 --- a/theories/Classes/Equivalence.v +++ b/theories/Classes/Equivalence.v @@ -6,11 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Typeclass-based setoids. Definitions on [Equivalence]. +(** * Typeclass-based setoids. Definitions on [Equivalence]. Author: Matthieu Sozeau - Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud - 91405 Orsay, France *) + Institution: LRI, CNRS UMR 8623 - University Paris Sud +*) (* $Id$ *) @@ -29,7 +29,8 @@ Open Local Scope signature_scope. Definition equiv `{Equivalence A R} : relation A := R. -(** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *) +(** Overloaded notations for setoid equivalence and inequivalence. + Not to be confused with [eq] and [=]. *) Notation " x === y " := (equiv x y) (at level 70, no associativity) : equiv_scope. diff --git a/theories/Classes/Functions.v b/theories/Classes/Functions.v index 80d60d658..8c6161036 100644 --- a/theories/Classes/Functions.v +++ b/theories/Classes/Functions.v @@ -6,11 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Functional morphisms. +(** * Functional morphisms. Author: Matthieu Sozeau - Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud - 91405 Orsay, France *) + Institution: LRI, CNRS UMR 8623 - University Paris Sud +*) (* $Id$ *) diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v index 7be92139e..f6e51018a 100644 --- a/theories/Classes/Init.v +++ b/theories/Classes/Init.v @@ -6,12 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Initialization code for typeclasses, setting up the default tactic +(** * Initialization code for typeclasses, setting up the default tactic for instance search. Author: Matthieu Sozeau - Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud - 91405 Orsay, France *) + Institution: LRI, CNRS UMR 8623 - University Paris Sud +*) (* $Id$ *) 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. diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v index 5b61e2c07..dbe7b5c88 100644 --- a/theories/Classes/Morphisms_Prop.v +++ b/theories/Classes/Morphisms_Prop.v @@ -6,11 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* [Proper] instances for propositional connectives. +(** * [Proper] instances for propositional connectives. Author: Matthieu Sozeau - Institution: LRI, CNRS UMR 8623 - Université Paris Sud - 91405 Orsay, France *) + Institution: LRI, CNRS UMR 8623 - University Paris Sud +*) Require Import Coq.Classes.Morphisms. Require Import Coq.Program.Basics. @@ -56,11 +56,11 @@ Program Instance ex_iff_morphism {A : Type} : Proper (pointwise_relation A iff = Proof. unfold pointwise_relation in H. split ; intros. - destruct H0 as [xâ‚ Hâ‚]. - exists xâ‚. rewrite H in Hâ‚. assumption. + destruct H0 as [x1 H1]. + exists x1. rewrite H in H1. assumption. - destruct H0 as [xâ‚ Hâ‚]. - exists xâ‚. rewrite H. assumption. + destruct H0 as [x1 H1]. + exists x1. rewrite H. assumption. Qed. Program Instance ex_impl_morphism {A : Type} : diff --git a/theories/Classes/Morphisms_Relations.v b/theories/Classes/Morphisms_Relations.v index e9301298e..9c42ff155 100644 --- a/theories/Classes/Morphisms_Relations.v +++ b/theories/Classes/Morphisms_Relations.v @@ -6,11 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Morphism instances for relations. +(** * Morphism instances for relations. 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 Relation_Definitions. Require Import Coq.Classes.Morphisms. @@ -38,8 +38,8 @@ Lemma predicate_implication_pointwise (l : list Type) : Proper (@predicate_implication l ==> pointwise_lifting impl l) id. Proof. do 2 red. unfold predicate_implication. auto. Qed. -(** The instanciation at relation allows to rewrite applications of relations [R x y] to [R' x y] *) -(* when [R] and [R'] are in [relation_equivalence]. *) +(** The instanciation at relation allows to rewrite applications of relations + [R x y] to [R' x y] when [R] and [R'] are in [relation_equivalence]. *) Instance relation_equivalence_pointwise : Proper (relation_equivalence ==> pointwise_relation A (pointwise_relation A iff)) id. diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index b2f62cb87..0222ad115 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.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 *) @@ -6,12 +7,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Typeclass-based relations, tactics and standard instances. +(** * Typeclass-based relations, tactics and standard instances + This is the basic theory needed to formalize morphisms and setoids. Author: Matthieu Sozeau - Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud - 91405 Orsay, France *) + Institution: LRI, CNRS UMR 8623 - University Paris Sud +*) (* $Id$ *) diff --git a/theories/Classes/SetoidAxioms.v b/theories/Classes/SetoidAxioms.v index ebc1d7be9..ef115b2ed 100644 --- a/theories/Classes/SetoidAxioms.v +++ b/theories/Classes/SetoidAxioms.v @@ -6,11 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Extensionality axioms that can be used when reasoning with setoids. - * - * Author: Matthieu Sozeau - * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud - * 91405 Orsay, France *) +(** * Extensionality axioms that can be used when reasoning with setoids. + + Author: Matthieu Sozeau + Institution: LRI, CNRS UMR 8623 - University Paris Sud +*) (* $Id$ *) @@ -21,7 +21,7 @@ Unset Strict Implicit. Require Export Coq.Classes.SetoidClass. -(* Application of the extensionality axiom to turn a goal on +(** Application of the extensionality axiom to turn a goal on Leibniz equality to a setoid equivalence (use with care!). *) Axiom setoideq_eq : forall `{sa : Setoid a} (x y : a), x == y -> x = y. diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v index 6af4b5ffe..33d98548d 100644 --- a/theories/Classes/SetoidClass.v +++ b/theories/Classes/SetoidClass.v @@ -6,11 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Typeclass-based setoids, tactics and standard instances. +(** * Typeclass-based setoids, tactics and standard 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$ *) diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v index 71d80c959..32e75adae 100644 --- a/theories/Classes/SetoidDec.v +++ b/theories/Classes/SetoidDec.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 *) @@ -6,11 +7,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Decidable setoid equality theory. - * - * Author: Matthieu Sozeau - * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud - * 91405 Orsay, France *) +(** * Decidable setoid equality theory. + + Author: Matthieu Sozeau + Institution: LRI, CNRS UMR 8623 - University Paris Sud +*) (* $Id$ *) @@ -21,21 +22,23 @@ Unset Strict Implicit. Require Export Coq.Classes.SetoidClass. -(** The [DecidableSetoid] class asserts decidability of a [Setoid]. It can be useful in proofs to reason more - classically. *) +(** The [DecidableSetoid] class asserts decidability of a [Setoid]. + It can be useful in proofs to reason more classically. *) Require Import Coq.Logic.Decidable. Class DecidableSetoid `(S : Setoid A) := setoid_decidable : forall x y : A, decidable (x == y). -(** The [EqDec] class gives a decision procedure for a particular setoid equality. *) +(** The [EqDec] class gives a decision procedure for a particular setoid + equality. *) Class EqDec `(S : Setoid A) := equiv_dec : forall x y : A, { x == y } + { x =/= y }. -(** We define the [==] overloaded notation for deciding equality. It does not take precedence - of [==] defined in the type scope, hence we can have both at the same time. *) +(** We define the [==] overloaded notation for deciding equality. It does not + take precedence of [==] defined in the type scope, hence we can have both + at the same time. *) Notation " x == y " := (equiv_dec (x :>) (y :>)) (no associativity, at level 70). @@ -72,7 +75,8 @@ Infix "<>b" := nequiv_decb (no associativity, at level 70). Require Import Coq.Arith.Arith. -(** The equiv is burried inside the setoid, but we can recover it by specifying which setoid we're talking about. *) +(** The equiv is burried inside the setoid, but we can recover + it by specifying which setoid we're talking about. *) Program Instance eq_setoid A : Setoid A | 10 := { equiv := eq ; setoid_equiv := eq_equivalence }. @@ -105,7 +109,8 @@ Program Instance prod_eqdec `(! EqDec (eq_setoid A), ! EqDec (eq_setoid B)) : Eq Solve Obligations using unfold complement ; program_simpl. -(** Objects of function spaces with countable domains like bool have decidable equality. *) +(** Objects of function spaces with countable domains like bool + have decidable equality. *) Program Instance bool_function_eqdec `(! EqDec (eq_setoid A)) : EqDec (eq_setoid (bool -> A)) := λ f g, diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v index 12356385c..c40e37e24 100644 --- a/theories/Classes/SetoidTactics.v +++ b/theories/Classes/SetoidTactics.v @@ -6,11 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Tactics for typeclass-based setoids. - * - * Author: Matthieu Sozeau - * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud - * 91405 Orsay, France *) +(** * Tactics for typeclass-based setoids. + + Author: Matthieu Sozeau + Institution: LRI, CNRS UMR 8623 - University Paris Sud +*) (* $Id$ *) @@ -34,12 +34,13 @@ Class DefaultRelation A (R : relation A). Definition default_relation `{DefaultRelation A R} := R. -(** Every [Equivalence] gives a default relation, if no other is given (lowest priority). *) +(** Every [Equivalence] gives a default relation, if no other is given + (lowest priority). *) Instance equivalence_default `(Equivalence A R) : DefaultRelation R | 4. -(** The setoid_replace tactics in Ltac, defined in terms of default relations and - the setoid_rewrite tactic. *) +(** The setoid_replace tactics in Ltac, defined in terms of default relations + and the setoid_rewrite tactic. *) Ltac setoidreplace H t := let Heq := fresh "Heq" in @@ -137,9 +138,11 @@ Tactic Notation "setoid_replace" constr(x) "with" constr(y) "by" tactic3(t) := setoidreplaceinat (rel x y) id ltac:t o. -(** The [add_morphism_tactic] tactic is run at each [Add Morphism] command before giving the hand back - to the user to discharge the proof. It essentially amounts to unfold the right amount of [respectful] calls - and substitute leibniz equalities. One can redefine it using [Ltac add_morphism_tactic ::= t]. *) +(** The [add_morphism_tactic] tactic is run at each [Add Morphism] + command before giving the hand back to the user to discharge the + proof. It essentially amounts to unfold the right amount of + [respectful] calls and substitute leibniz equalities. One can + redefine it using [Ltac add_morphism_tactic ::= t]. *) Require Import Coq.Program.Tactics. diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index 189cf88ad..a53a485d3 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -1,4 +1,3 @@ - (***********************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v index 52766bf96..c4b8f2a8d 100644 --- a/theories/FSets/FMapFullAVL.v +++ b/theories/FSets/FMapFullAVL.v @@ -1,4 +1,3 @@ - (***********************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v index 112ccce30..da5b35874 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 diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v index 0f0e675ee..36964ad01 100644 --- a/theories/FSets/FSetAVL.v +++ b/theories/FSets/FSetAVL.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (***********************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) @@ -6,16 +7,11 @@ (* * 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$ *) -(** * FSetAVL *) +(** * FSetAVL : Implementation of FSetInterface via AVL trees *) -(** This module implements sets using AVL trees. +(** This module implements finite sets using AVL trees. It follows the implementation from Ocaml's standard library, All operations given here expect and produce well-balanced trees diff --git a/theories/FSets/FSetFullAVL.v b/theories/FSets/FSetFullAVL.v index bc0d758bd..d8a31ba5f 100644 --- a/theories/FSets/FSetFullAVL.v +++ b/theories/FSets/FSetFullAVL.v @@ -6,16 +6,9 @@ (* * 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$ *) -(** * FSetFullAVL - - This file contains some complements to [FSetAVL]. +(** * FSetFullAVL : some complements to FSetAVL - Functor [AvlProofs] proves that trees of [FSetAVL] are not only binary search trees, but moreover well-balanced ones. This is done diff --git a/theories/FSets/FSetToFiniteSet.v b/theories/FSets/FSetToFiniteSet.v index 23420109c..01138270e 100644 --- a/theories/FSets/FSetToFiniteSet.v +++ b/theories/FSets/FSetToFiniteSet.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$ *) +(** * Finite sets library : conversion to old [Finite_sets] *) + Require Import Ensembles Finite_sets. Require Import FSetInterface FSetProperties OrderedTypeEx DecidableTypeEx. diff --git a/theories/FSets/OrderedTypeAlt.v b/theories/FSets/OrderedTypeAlt.v index 3a9fa1a73..23ae4c85a 100644 --- a/theories/FSets/OrderedTypeAlt.v +++ b/theories/FSets/OrderedTypeAlt.v @@ -5,12 +5,6 @@ (* // * This file is distributed under the terms of the *) (* * 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$ *) Require Import OrderedType. diff --git a/theories/FSets/OrderedTypeEx.v b/theories/FSets/OrderedTypeEx.v index e76cead2d..a39f336a5 100644 --- a/theories/FSets/OrderedTypeEx.v +++ b/theories/FSets/OrderedTypeEx.v @@ -6,11 +6,6 @@ (* * 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$ *) Require Import OrderedType. diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index 32880b2f7..02e6d3daf 100644 --- a/theories/Logic/ChoiceFacts.v +++ b/theories/Logic/ChoiceFacts.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 *) @@ -81,7 +82,7 @@ unpublished. [[Bell93]] John L. Bell, Hilbert's Epsilon Operator in Intuitionistic Type Theories, Mathematical Logic Quarterly, volume 39, 1993. -[Carlstrøm05] Jesper Carlstrøm, Interpreting descriptions in +[Carlström05] Jesper Carlström, Interpreting descriptions in intentional type theory, Journal of Symbolic Logic 70(2):488-514, 2005. *) @@ -126,7 +127,7 @@ Definition FunctionalRelReification_on := (** ID_epsilon (constructive version of indefinite description; combined with proof-irrelevance, it may be connected to - Carlstrøm's type theory with a constructive indefinite description + Carlström's type theory with a constructive indefinite description operator) *) Definition ConstructiveIndefiniteDescription_on := @@ -134,7 +135,7 @@ Definition ConstructiveIndefiniteDescription_on := (exists x, P x) -> { x:A | P x }. (** ID_iota (constructive version of definite description; combined - with proof-irrelevance, it may be connected to Carlstrøm's and + with proof-irrelevance, it may be connected to Carlström's and Stenlund's type theory with a constructive definite description operator) *) @@ -764,7 +765,7 @@ be applied on the same Type universes on both sides of the first We adapt the proof to show that constructive definite description transports excluded-middle from [Prop] to [Set]. - [[ChicliPottierSimpson02]] Laurent Chicli, Loïc Pottier, Carlos + [[ChicliPottierSimpson02]] Laurent Chicli, Loïc Pottier, Carlos Simpson, Mathematical Quotients and Quotient Types in Coq, Proceedings of TYPES 2002, Lecture Notes in Computer Science 2646, Springer Verlag. *) diff --git a/theories/Logic/ClassicalEpsilon.v b/theories/Logic/ClassicalEpsilon.v index 0d65a89ba..cee55dc81 100644 --- a/theories/Logic/ClassicalEpsilon.v +++ b/theories/Logic/ClassicalEpsilon.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 *) @@ -74,7 +75,7 @@ Definition epsilon_spec (A : Type) (i:inhabited A) (P : A->Prop) : (** A proof that if [P] is inhabited, [epsilon a P] does not depend on the actual proof that the domain of [P] is inhabited - (proof idea kindly provided by Pierre Castéran) *) + (proof idea kindly provided by Pierre Castéran) *) Lemma epsilon_inh_irrelevance : forall (A:Type) (i j : inhabited A) (P:A->Prop), diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v index 9ec916a7d..b22a3a874 100644 --- a/theories/Logic/ClassicalFacts.v +++ b/theories/Logic/ClassicalFacts.v @@ -31,7 +31,7 @@ Table of contents: 3.1. Weak excluded middle -3.2. Gödel-Dummett axiom and right distributivity of implication over +3.2. Gödel-Dummett axiom and right distributivity of implication over disjunction 3 3. Independence of general premises and drinker's paradox @@ -290,7 +290,7 @@ End Proof_irrelevance_CIC. cannot be refined. [[Berardi90]] Stefano Berardi, "Type dependence and constructive - mathematics", Ph. D. thesis, Dipartimento Matematica, Università di + mathematics", Ph. D. thesis, Dipartimento Matematica, Università di Torino, 1990. *) @@ -417,7 +417,7 @@ End Proof_irrelevance_CCI. (** We show the following increasing in the strength of axioms: - weak excluded-middle - - right distributivity of implication over disjunction and Gödel-Dummett axiom + - right distributivity of implication over disjunction and Gödel-Dummett axiom - independence of general premises and drinker's paradox - excluded-middle *) @@ -436,20 +436,20 @@ Definition weak_excluded_middle := (** The interest in the equivalent variant [weak_generalized_excluded_middle] is that it holds even in logic - without a primitive [False] connective (like Gödel-Dummett axiom) *) + without a primitive [False] connective (like Gödel-Dummett axiom) *) Definition weak_generalized_excluded_middle := forall A B:Prop, ((A -> B) -> B) \/ (A -> B). -(** ** Gödel-Dummett axiom *) +(** ** Gödel-Dummett axiom *) -(** [(A->B) \/ (B->A)] is studied in [[Dummett59]] and is based on [[Gödel33]]. +(** [(A->B) \/ (B->A)] is studied in [[Dummett59]] and is based on [[Gödel33]]. [[Dummett59]] Michael A. E. Dummett. "A Propositional Calculus with a Denumerable Matrix", In the Journal of Symbolic Logic, Vol 24 No. 2(1959), pp 97-103. - [[Gödel33]] Kurt Gödel. "Zum intuitionistischen Aussagenkalkül", + [[Gödel33]] Kurt Gödel. "Zum intuitionistischen Aussagenkalkül", Ergeb. Math. Koll. 4 (1933), pp. 34-38. *) @@ -500,13 +500,13 @@ Qed. It is a generalization to predicate logic of the right distributivity of implication over disjunction (hence of - Gödel-Dummett axiom) whose own constructive form (obtained by a + Gödel-Dummett axiom) whose own constructive form (obtained by a restricting the third formula to be negative) is called Kreisel-Putnam principle [[KreiselPutnam57]]. [[KreiselPutnam57]], Georg Kreisel and Hilary Putnam. "Eine - Unableitsbarkeitsbeweismethode für den intuitionistischen - Aussagenkalkül". Archiv für Mathematische Logik und + Unableitsbarkeitsbeweismethode für den intuitionistischen + Aussagenkalkül". Archiv für Mathematische Logik und Graundlagenforschung, 3:74- 78, 1957. [[Troelstra73]], Anne Troelstra, editor. Metamathematical diff --git a/theories/Logic/ClassicalUniqueChoice.v b/theories/Logic/ClassicalUniqueChoice.v index c1f9881fa..2a32323cb 100644 --- a/theories/Logic/ClassicalUniqueChoice.v +++ b/theories/Logic/ClassicalUniqueChoice.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 *) @@ -19,7 +20,7 @@ excluded-middle in [Set], hence it implies a strongly classical world. Especially it conflicts with the impredicativity of [Set]. - [ChicliPottierSimpson02] Laurent Chicli, Loïc Pottier, Carlos + [ChicliPottierSimpson02] Laurent Chicli, Loïc Pottier, Carlos Simpson, Mathematical Quotients and Quotient Types in Coq, Proceedings of TYPES 2002, Lecture Notes in Computer Science 2646, Springer Verlag. *) diff --git a/theories/Logic/ConstructiveEpsilon.v b/theories/Logic/ConstructiveEpsilon.v index 337ee05b6..6d22b1a9e 100644 --- a/theories/Logic/ConstructiveEpsilon.v +++ b/theories/Logic/ConstructiveEpsilon.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 *) diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v index 18f3181b6..22c838c26 100644 --- a/theories/Logic/Diaconescu.v +++ b/theories/Logic/Diaconescu.v @@ -39,7 +39,7 @@ [Bell93] John L. Bell, Hilbert's epsilon operator and classical logic, Journal of Philosophical Logic, 22: 1-18, 1993 - [Carlström04] Jesper Carlström, EM + Ext_ + AC_int <-> AC_ext, + [Carlström04] Jesper Carlström, [EM + Ext_ + AC_int <-> AC_ext], Mathematical Logic Quaterly, vol 50(3), pp 236-240, 2004. *) diff --git a/theories/Logic/Eqdep.v b/theories/Logic/Eqdep.v index 3c3b7bbfa..5c6b4e89f 100644 --- a/theories/Logic/Eqdep.v +++ b/theories/Logic/Eqdep.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 *) diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v index a4b4b5b4a..4689fb46c 100644 --- a/theories/Logic/EqdepFacts.v +++ b/theories/Logic/EqdepFacts.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 *) @@ -25,7 +26,7 @@ References: [1] T. Streicher, Semantical Investigations into Intensional Type Theory, - Habilitationsschrift, LMU München, 1993. + Habilitationsschrift, LMU München, 1993. [2] M. Hofmann, T. Streicher, The groupoid interpretation of type theory, Proceedings of the meeting Twenty-five years of constructive type theory, Venice, Oxford University Press, 1998 diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v index 21ff55c19..0a1cd9ab4 100644 --- a/theories/NArith/BinPos.v +++ b/theories/NArith/BinPos.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 *) diff --git a/theories/NArith/Pnat.v b/theories/NArith/Pnat.v index f989e01d0..0891dea21 100644 --- a/theories/NArith/Pnat.v +++ b/theories/NArith/Pnat.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 *) 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. diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index 93b723af3..0fe8bb176 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.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 *) diff --git a/theories/Reals/Ranalysis3.v b/theories/Reals/Ranalysis3.v index 3de97ba90..3b685cd8a 100644 --- a/theories/Reals/Ranalysis3.v +++ b/theories/Reals/Ranalysis3.v @@ -60,7 +60,7 @@ Proof. case (Req_dec (f1 x) 0); intro. case (Req_dec l1 0); intro. (***********************************) -(* Cas n° 1 *) +(* First case *) (* (f1 x)=0 l1 =0 *) (***********************************) cut (0 < Rmin eps_f2 (Rmin alp_f2 alp_f1d)); @@ -118,7 +118,7 @@ Proof. apply Rmin_2; assumption. right; symmetry in |- *; apply quadruple_var. (***********************************) -(* Cas n° 2 *) +(* Second case *) (* (f1 x)=0 l1<>0 *) (***********************************) assert (H10 := derivable_continuous_pt _ _ X). @@ -218,7 +218,7 @@ Proof. apply Rinv_neq_0_compat; repeat apply prod_neq_R0; [ discrR | discrR | discrR | assumption ]. (***********************************) -(* Cas n° 3 *) +(* Third case *) (* (f1 x)<>0 l1=0 l2=0 *) (***********************************) case (Req_dec l1 0); intro. @@ -291,7 +291,7 @@ Proof. apply (cond_pos alp_f1d). apply (cond_pos alp_f2d). (***********************************) -(* Cas n° 4 *) +(* Fourth case *) (* (f1 x)<>0 l1=0 l2<>0 *) (***********************************) elim (H0 (Rabs (Rsqr (f2 x) * eps / (8 * f1 x)))); @@ -421,7 +421,7 @@ Proof. apply Rinv_neq_0_compat; discrR. apply Rinv_neq_0_compat; assumption. (***********************************) -(* Cas n° 5 *) +(* Fifth case *) (* (f1 x)<>0 l1<>0 l2=0 *) (***********************************) case (Req_dec l2 0); intro. @@ -538,7 +538,7 @@ Proof. (apply Rinv_neq_0_compat; discrR) || (red in |- *; intro H12; rewrite H12 in H6; elim (Rlt_irrefl _ H6)). (***********************************) -(* Cas n° 6 *) +(* Sixth case *) (* (f1 x)<>0 l1<>0 l2<>0 *) (***********************************) elim (H0 (Rabs (Rsqr (f2 x) * eps / (8 * f1 x)))). diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v index 88cead7a5..63684c1f3 100644 --- a/theories/Reals/RiemannInt.v +++ b/theories/Reals/RiemannInt.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 *) @@ -423,7 +424,7 @@ Proof. Qed. (***************************************) -(** C°([a,b]) is included in L1([a,b]) *) +(** C°([a,b]) is included in L1([a,b]) *) (***************************************) Lemma maxN : diff --git a/theories/Reals/Rtopology.v b/theories/Reals/Rtopology.v index c115969e3..5b55896b1 100644 --- a/theories/Reals/Rtopology.v +++ b/theories/Reals/Rtopology.v @@ -1598,17 +1598,17 @@ Theorem Heine : (forall x:R, X x -> continuity_pt f x) -> uniform_continuity f X. Proof. intros f0 X H0 H; elim (domain_P1 X); intro Hyp. -(* X est vide *) +(* X is empty *) unfold uniform_continuity in |- *; intros; exists (mkposreal _ Rlt_0_1); intros; elim Hyp; exists x; assumption. elim Hyp; clear Hyp; intro Hyp. -(* X possède un seul élément *) +(* X has only one element *) unfold uniform_continuity in |- *; intros; exists (mkposreal _ Rlt_0_1); intros; elim Hyp; clear Hyp; intros; elim H4; clear H4; intros; assert (H6 := H5 _ H1); assert (H7 := H5 _ H2); rewrite H6; rewrite H7; unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0; apply (cond_pos eps). -(* X possède au moins deux éléments distincts *) +(* X has at least two distinct elements *) assert (X_enc : exists m : R, (exists M : R, (forall x:R, X x -> m <= x <= M) /\ m < M)). diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v index 6d3dc02a9..87d8e1350 100644 --- a/theories/Strings/Ascii.v +++ b/theories/Strings/Ascii.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 *) @@ -8,7 +9,7 @@ (* $Id$ *) -(** Contributed by Laurent Théry (INRIA); +(** Contributed by Laurent Théry (INRIA); Adapted to Coq V8 by the Coq Development Team *) Require Import Bool. diff --git a/theories/Strings/String.v b/theories/Strings/String.v index 82a60c189..21c0a15e9 100644 --- a/theories/Strings/String.v +++ b/theories/Strings/String.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 *) @@ -8,7 +9,7 @@ (* $Id$ *) -(** Contributed by Laurent Théry (INRIA); +(** Contributed by Laurent Théry (INRIA); Adapted to Coq V8 by the Coq Development Team *) Require Import Arith. diff --git a/theories/Unicode/Utf8.v b/theories/Unicode/Utf8.v index 940cec9bd..3a11c9e5e 100644 --- a/theories/Unicode/Utf8.v +++ b/theories/Unicode/Utf8.v @@ -1,4 +1,4 @@ -(* -*- coding:utf-8 -* *) +(* -*- 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/ZArith/BinInt.v b/theories/ZArith/BinInt.v index b8301d0f4..06ba2eb89 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.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 *) diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v index de05c296d..30c08fdc1 100644 --- a/theories/ZArith/Int.v +++ b/theories/ZArith/Int.v @@ -6,14 +6,9 @@ (* * 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$ *) -(** An axiomatization of integers. *) +(** * An light axiomatization of integers (used in FSetAVL). *) (** We define a signature for an integer datatype based on [Z]. The goal is to allow a switch after extraction to ocaml's diff --git a/theories/ZArith/Zabs.v b/theories/ZArith/Zabs.v index 51c2a2905..36eb41104 100644 --- a/theories/ZArith/Zabs.v +++ b/theories/ZArith/Zabs.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 *) diff --git a/theories/ZArith/Zbinary.v b/theories/ZArith/Zbinary.v index 4c9ee2405..0a6c94986 100644 --- a/theories/ZArith/Zbinary.v +++ b/theories/ZArith/Zbinary.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 *) @@ -16,27 +17,22 @@ Require Import ZArith. Require Export Zpower. Require Import Omega. -(** L'évaluation des vecteurs de booléens se font à la fois en binaire et - en complément à deux. Le nombre appartient à Z. - On utilise donc Omega pour faire les calculs dans Z. - De plus, on utilise les fonctions 2^n où n est un naturel, ici la longueur. - two_power_nat = [n:nat](POS (shift_nat n xH)) - : nat->Z - two_power_nat_S - : (n:nat)`(two_power_nat (S n)) = 2*(two_power_nat n)` - Z_lt_ge_dec - : (x,y:Z){`x < y`}+{`x >= y`} +(** The evaluation of boolean vector is done both in binary and + two's complement. The computed number belongs to Z. + We hence use Omega to perform computations in Z. + Moreover, we use functions [2^n] where [n] is a natural number + (here the vector length). *) Section VALUE_OF_BOOLEAN_VECTORS. -(** Les calculs sont effectués dans la convention positive usuelle. - Les valeurs correspondent soit à l'écriture binaire (nat), - soit au complément à deux (int). - On effectue le calcul suivant le schéma de Horner. - Le complément à deux n'a de sens que sur les vecteurs de taille - supérieure ou égale à un, le bit de signe étant évalué négativement. +(** Computations are done in the usual convention. + The values correspond either to the binary coding (nat) or + to the two's complement coding (int). + We perform the computation via Horner scheme. + The two's complement coding only makes sense on vectors whose + size is greater or equal to one (a sign bit should be present). *) Definition bit_value (b:bool) : Z := @@ -68,12 +64,12 @@ End VALUE_OF_BOOLEAN_VECTORS. Section ENCODING_VALUE. -(** On calcule la valeur binaire selon un schema de Horner. - Le calcul s'arrete à la longueur du vecteur sans vérification. - On definit une fonction Zmod2 calquee sur Zdiv2 mais donnant le quotient - de la division z=2q+r avec 0<=r<=1. - La valeur en complément à deux est calculée selon un schema de Horner - avec Zmod2, le paramètre est la taille moins un. +(** We compute the binary value via a Horner scheme. + Computation stops at the vector length without checks. + We define a function Zmod2 similar to Zdiv2 returning the + quotient of division z=2q+r with 0<=r<=1. + The two's complement value is also computed via a Horner scheme + with Zmod2, the parameter is the size minus one. *) Definition Zmod2 (z:Z) := @@ -134,9 +130,8 @@ End ENCODING_VALUE. Section Z_BRIC_A_BRAC. - (** Bibliotheque de lemmes utiles dans la section suivante. - Utilise largement ZArith. - Mériterait d'être récrite. + (** Some auxiliary lemmas used in the next section. Large use of ZArith. + Deserve to be properly rewritten. *) Lemma binary_value_Sn : @@ -282,8 +277,8 @@ End Z_BRIC_A_BRAC. Section COHERENT_VALUE. -(** On vérifie que dans l'intervalle de définition les fonctions sont - réciproques l'une de l'autre. Elles utilisent les lemmes du bric-a-brac. +(** We check that the functions are reciprocal on the definition interval. + This uses earlier library lemmas. *) Lemma binary_to_Z_to_binary : diff --git a/theories/ZArith/Zcompare.v b/theories/ZArith/Zcompare.v index f146a80e1..2515b7f7b 100644 --- a/theories/ZArith/Zcompare.v +++ b/theories/ZArith/Zcompare.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,7 +10,7 @@ (*i $$ i*) (**********************************************************************) -(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) +(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) (**********************************************************************) Require Export BinPos. diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index 3435874cc..bc35ba405 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.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 *) diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v index c406a1542..dd35cd139 100644 --- a/theories/ZArith/Zmin.v +++ b/theories/ZArith/Zmin.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 *) diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v index 46b23fe63..3d9853ff0 100644 --- a/theories/ZArith/Znat.v +++ b/theories/ZArith/Znat.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 *) diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v index 7aef3ea8e..70cbe0f28 100644 --- a/theories/ZArith/Zorder.v +++ b/theories/ZArith/Zorder.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,7 +8,7 @@ (************************************************************************) (*i $Id$ i*) -(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *) +(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) Require Import BinPos. Require Import BinInt. diff --git a/theories/ZArith/auxiliary.v b/theories/ZArith/auxiliary.v index 6ebdcb50a..7af99ece9 100644 --- a/theories/ZArith/auxiliary.v +++ b/theories/ZArith/auxiliary.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 *) @@ -8,7 +9,7 @@ (*i $Id$ i*) -(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) +(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) Require Export Arith_base. Require Import BinInt. |