diff --git a/theories/nmap.v b/theories/nmap.v
index 8ab9fa8767c49043bd6da90559752c3749748036..7e56c562ad7b5db69bb5e1937a6526afb5ff3aab 100644
--- a/theories/nmap.v
+++ b/theories/nmap.v
@@ -35,7 +35,7 @@ Instance Npartial_alter {A} : PartialAlter N A (Nmap A) := λ f i t,
 Instance Nto_list {A} : FinMapToList N A (Nmap A) := λ t,
   match t with
   | NMap o t =>
-     default [] o (λ x, [(0,x)]) ++ (prod_map Npos id <$> map_to_list t)
+     from_option (λ x, [(0,x)]) [] o ++ (prod_map Npos id <$> map_to_list t)
   end.
 Instance Nomap: OMap Nmap := λ A B f t,
   match t with NMap o t => NMap (o ≫= f) (omap f t) end.
diff --git a/theories/option.v b/theories/option.v
index fa3fbd61ea6e27ae8ec702dc873cfd972a9f368d..6d82eed02f9e102eadb923901314f52f6eadb739 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -26,10 +26,6 @@ Definition from_option {A B} (f : A → B) (y : B) (mx : option A) : B :=
 Instance: Params (@from_option) 3.
 Arguments from_option {_ _} _ _ !_ / : assert.
 
-(* The eliminator again, but with the arguments in different order, which is
-sometimes more convenient. *)
-Notation default y mx f := (from_option f y mx) (only parsing).
-
 (** An alternative, but equivalent, definition of equality on the option
 data type. This theorem is useful to prove that two options are the same. *)
 Lemma option_eq {A} (mx my: option A): mx = my ↔ ∀ x, mx = Some x ↔ my = Some x.
diff --git a/theories/pmap.v b/theories/pmap.v
index 0eba03ef9cbab4060cb01f01c1058a0459e8adf4..519641c22a88393dcdd9fd20642c05b68dc184d1 100644
--- a/theories/pmap.v
+++ b/theories/pmap.v
@@ -86,7 +86,7 @@ Fixpoint Pto_list_raw {A} (j : positive) (t : Pmap_raw A)
     (acc : list (positive * A)) : list (positive * A) :=
   match t with
   | PLeaf => acc
-  | PNode o l r => default [] o (λ x, [(Preverse j, x)]) ++
+  | PNode o l r => from_option (λ x, [(Preverse j, x)]) [] o ++
      Pto_list_raw (j~0) l (Pto_list_raw (j~1) r acc)
   end%list.
 Fixpoint Pomap_raw {A B} (f : A → option B) (t : Pmap_raw A) : Pmap_raw B :=
diff --git a/theories/strings.v b/theories/strings.v
index d7ba9adb9b097b1cc57cbf0730af710fa8d6ff26..2110270a720d7e11135b716955b188caaf538d69 100644
--- a/theories/strings.v
+++ b/theories/strings.v
@@ -57,7 +57,7 @@ Fixpoint words_go (cur : option string) (s : string) : list string :=
   | "" => option_list (string_rev <$> cur)
   | String a s =>
      if is_space a then option_list (string_rev <$> cur) ++ words_go None s
-     else words_go (Some (default (String a "") cur (String a))) s
+     else words_go (Some (from_option (String a) (String a "") cur)) s
   end.
 Definition words : string → list string := words_go None.
 
diff --git a/theories/zmap.v b/theories/zmap.v
index 241b1d3c8bb9ea4b172f7ba0168139ab7d7c3377..31177c02e0b52170ca2d8b3d848e383f34b82ed9 100644
--- a/theories/zmap.v
+++ b/theories/zmap.v
@@ -35,7 +35,7 @@ Instance Zpartial_alter {A} : PartialAlter Z A (Zmap A) := λ f i t,
   end.
 Instance Zto_list {A} : FinMapToList Z A (Zmap A) := λ t,
   match t with
-  | ZMap o t t' => default [] o (λ x, [(0,x)]) ++
+  | ZMap o t t' => from_option (λ x, [(0,x)]) [] o ++
      (prod_map Zpos id <$> map_to_list t) ++
      (prod_map Zneg id <$> map_to_list t')
   end.