diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Init/Datatypes.v | 6 | ||||
| -rw-r--r-- | theories/Lists/List.v | 2 | ||||
| -rw-r--r-- | theories/MSets/MSetList.v | 2 |
3 files changed, 5 insertions, 5 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 9b5d7ffb0..c8d18f766 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -153,10 +153,10 @@ Inductive option (A:Type) : Type := Arguments None [A]. -Definition option_map (A B:Type) (f:A->B) o := +Definition option_map (A B:Type) (f:A->B) (o : option A) : option B := match o with - | Some a => Some (f a) - | None => None + | Some a => @Some B (f a) + | None => @None B end. (** [sum A B], written [A + B], is the disjoint sum of [A] and [B] *) diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 2062f3861..4850b3c4c 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -1892,7 +1892,7 @@ Inductive Forall2 A B (R:A->B->Prop) : list A -> list B -> Prop := Hint Constructors Forall2. Theorem Forall2_refl : forall A B (R:A->B->Prop), Forall2 R [] []. -Proof. exact Forall2_nil. Qed. +Proof. intros; apply Forall2_nil. Qed. Theorem Forall2_app_inv_l : forall A B (R:A->B->Prop) l1 l2 l', Forall2 R (l1 ++ l2) l' -> diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v index 5c232f340..fb0d1ad9d 100644 --- a/theories/MSets/MSetList.v +++ b/theories/MSets/MSetList.v @@ -56,7 +56,7 @@ Module Ops (X:OrderedType) <: WOps X. Definition singleton (x : elt) := x :: nil. - Fixpoint remove x s := + Fixpoint remove x s : t := match s with | nil => nil | y :: l => |