Try a new way of handling template universe levels

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 =>