Try a new way of handling template universe levels

1 files changed, 3 insertions, 3 deletions

diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 9b5d7ffb08..c8d18f7661 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] *)