diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-05-15 11:37:43 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-05-15 11:39:49 +0200 |
commit | 5d015ae0d90fd7fd3d440acee6ccd501d8b63ba0 (patch) | |
tree | e73fb685fea3bd4aa5a9eecde1df69c518acccf0 /theories | |
parent | 76c3b40482978fffca50f6f59e8bcae455680aba (diff) | |
parent | 3fb81febe8efc34860688cac88a2267cfe298cf7 (diff) |
Merge v8.5 into trunk
Conflicts:
tactics/eauto.ml4
(merging eauto.ml4 and adapting coq_micromega.ml to new typing.ml API)
Diffstat (limited to 'theories')
-rw-r--r-- | theories/Classes/RelationClasses.v | 5 | ||||
-rw-r--r-- | theories/Lists/List.v | 10 |
2 files changed, 10 insertions, 5 deletions
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 1a40e5d59..15cb02d37 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) := diff --git a/theories/Lists/List.v b/theories/Lists/List.v index c34bbd56e..2437184a9 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 := |