Remove the `default` notation for options

The notation was parsing-only and all it did was reorder the arguments for
from_option.  This creates just a needless divergence between what is written
and what is printed.  Also, removing it frees the name for maybe introducing a
function or notation `default` with a type like `T -> option T -> T`.

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.

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.

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

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.
 

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.