diff options
Diffstat (limited to 'theories/Lists/List.v')
| -rw-r--r-- | theories/Lists/List.v | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/theories/Lists/List.v b/theories/Lists/List.v index ea07a849..fe18686e 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) := @@ -69,7 +69,7 @@ Section Facts. Variable A : Type. - (** *** Genereric facts *) + (** *** Generic facts *) (** Discrimination *) Theorem nil_cons : forall (x:A) (l:list A), [] <> x :: l. @@ -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 := @@ -622,9 +622,9 @@ Section Elts. Qed. - (****************************************) - (** ** Counting occurences of a element *) - (****************************************) + (******************************************) + (** ** Counting occurrences of an element *) + (******************************************) Fixpoint count_occ (l : list A) (x : A) : nat := match l with @@ -2202,7 +2202,7 @@ Section ForallPairs. Proof. induction 1. inversion 1. - simpl; destruct 1; destruct 1; repeat subst; auto. + simpl; destruct 1; destruct 1; subst; auto. right; left. apply -> Forall_forall; eauto. right; right. apply -> Forall_forall; eauto. Qed. |