From 1f3ea50258490ac8b5a395ac0ff2bca7326e755f Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 12 May 2015 17:55:10 +0200
Subject: Mark PreOrder as a consequence of Equivalence. (Fix bug #4213)

---
 theories/Classes/RelationClasses.v | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'theories')

diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 1a40e5d599..15cb02d37f 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -89,6 +89,11 @@ Section Defs.
   Global Instance Equivalence_PER {R} `(E:Equivalence R) : PER R | 10 :=
     { }. 
 
+  (** An Equivalence is a PreOrder plus symmetry. *)
+
+  Global Instance Equivalence_PreOrder {R} `(E:Equivalence R) : PreOrder R | 10 :=
+    { }.
+
   (** We can now define antisymmetry w.r.t. an equivalence relation on the carrier. *)
   
   Class Antisymmetric eqA `{equ : Equivalence eqA} (R : relation A) :=
-- 
cgit v1.2.3


From b338af912c32ab87d6668923add72a56408bddf8 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Tue, 12 May 2015 17:41:45 +0200
Subject: List.nth_error directly produces Some/None instead of value/error

 List.nth_error and List.hd_error were the only remaining places in
 the whole stdlib to use type "Exc" instead of "option" directly.
 So let's simplify things and use option everywhere. In particular,
 during teaching sessions about lists, we won't have anymore to explain
 the (lack of) difference between Exc,value,error and option,Some,None.

 This might cause a few incompatibilities in proof scripts, if they
 syntactically expect "value" or "error" to occur, but this should
 hopefully be very rare and quite easy to fix.
---
 theories/Lists/List.v | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'theories')

diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 5819fbe5ef..e0e5d94d82 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -45,8 +45,8 @@ Section Lists.
 
   Definition hd_error (l:list A) :=
     match l with
-      | [] => error
-      | x :: _ => value x
+      | [] => None
+      | x :: _ => Some x
     end.
 
   Definition tl (l:list A) :=
@@ -393,11 +393,11 @@ Section Elts.
     simpl; auto.
   Qed.
 
-  Fixpoint nth_error (l:list A) (n:nat) {struct n} : Exc A :=
+  Fixpoint nth_error (l:list A) (n:nat) {struct n} : option A :=
     match n, l with
-      | O, x :: _ => value x
+      | O, x :: _ => Some x
       | S n, _ :: l => nth_error l n
-      | _, _ => error
+      | _, _ => None
     end.
 
   Definition nth_default (default:A) (l:list A) (n:nat) : A :=
-- 
cgit v1.2.3