aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Classes/SetoidDec.v
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-09-28 15:04:07 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-09-28 15:04:07 +0000
commit4d90c1983907ff3ea8a5a8c4dca1dba57c5bf3f8 (patch)
treee80307fb09a9836c5dd17f16b412e85fa25b6818 /theories/Classes/SetoidDec.v
parentaac58d6a2a196ac20da147034ac89546c1c236fe (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/SetoidDec.v')
-rw-r--r--theories/Classes/SetoidDec.v29
1 files changed, 17 insertions, 12 deletions
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,