diff --git a/lib/AstToCFlat.ml b/lib/AstToCFlat.ml
index 40fc613ca..3ebb67d2b 100644
--- a/lib/AstToCFlat.ml
+++ b/lib/AstToCFlat.ml
@@ -202,7 +202,7 @@ let align array_size pos =
 
 (* Helper *)
 let fields_of_struct =
-  List.map (fun (name, (t, _mut)) -> Option.must name, t)
+  List.map (fun (name, (t, _mut)) -> Option.get name, t)
 
 (* A TQualified can either be a struct or an enum. Same for TAnonymous. *)
 let is_enum env t =
@@ -537,9 +537,9 @@ let write_static (env: env) (lid: lident) (e: expr): string * CFlat.expr list =
         write_le dst ofs e.typ (Z.of_int (LidMap.find lid env.enums));
         []
     | EFlat fields ->
-        let layout = Option.must (layout_of env e) in
+        let layout = Option.get (layout_of env e) in
         KList.map_flatten (fun (fname, e) ->
-          let fname = Option.must fname in
+          let fname = Option.get fname in
           let fofs = fst (List.assoc fname layout.fields) in
           write_scalar dst (ofs + fofs) e
         ) fields
@@ -607,7 +607,7 @@ let rec write_at (env: env)
             (* KPrint.bprintf "    >>> write_at: literal\n"; *)
             let locals, writes =
               fold (fun locals (fname, e) ->
-                let fname = Option.must fname in
+                let fname = Option.get fname in
                 let fofs = fst (List.assoc fname layout.fields) in
                 (* Recursively write each field of the struct at its offset. *)
                 write_at locals (ofs + fofs, e)
@@ -800,7 +800,7 @@ and mk_expr (env: env) (locals: locals) (e: expr): locals * CF.expr =
 
   | EAddrOf ({ node = EField (e1, f); _ }) ->
       (* This is the "address-of" operation from the paper. *)
-      let ofs = fst (List.assoc f (Option.must (layout_of env e1)).fields) in
+      let ofs = fst (List.assoc f (Option.get (layout_of env e1)).fields) in
       let locals, e1 = mk_expr env locals (with_type (TBuf (e1.typ, true)) (EAddrOf e1)) in
       locals, mk_add32 e1 (mk_uint32 ofs)
 
diff --git a/lib/AstToCStar.ml b/lib/AstToCStar.ml
index 4c55cf04e..f0cf76762 100644
--- a/lib/AstToCStar.ml
+++ b/lib/AstToCStar.ml
@@ -402,7 +402,7 @@ and mk_expr env in_stmt e =
       CStar.Cast (mk_expr env e, mk_type env t)
   | EAbort (t, s) ->
       let t = match t with Some t -> t | None -> e.typ in
-      CStar.EAbort (mk_type env t, Option.or_empty s)
+      CStar.EAbort (mk_type env t, Option.value ~default:"" s)
   | EUnit ->
       CStar.Cast (zero, CStar.Pointer CStar.Void)
   | EAny ->
@@ -627,7 +627,7 @@ and mk_stmts env e ret_type =
         fatal_error "[AstToCStar.collect EMatch]: not implemented"
 
     | EAbort (_, s) ->
-        env, CStar.Abort (Option.or_empty s) :: acc
+        env, CStar.Abort (Option.value ~default:"" s) :: acc
 
     | ESwitch (e, branches) ->
         let default, branches =
diff --git a/lib/AstToMiniRust.ml b/lib/AstToMiniRust.ml
index eb8f30dd1..bf9a653fb 100644
--- a/lib/AstToMiniRust.ml
+++ b/lib/AstToMiniRust.ml
@@ -35,7 +35,7 @@ module H = struct
     | _ -> None
 
   let wrapping_operator o =
-    Option.must (wrapping_operator_opt o)
+    Option.get (wrapping_operator_opt o)
 
   let is_wrapping_operator o =
     wrapping_operator_opt o <> None
diff --git a/lib/Bundles.ml b/lib/Bundles.ml
index 60fa3bed8..78a7c132f 100644
--- a/lib/Bundles.ml
+++ b/lib/Bundles.ml
@@ -132,7 +132,7 @@ let direct_dependencies file_of file =
   let prepend lid =
     match file_of lid with
     | Some f when f <> fst file ->
-        let dep = (Option.must !current_decl, fst file, lid, f) in
+        let dep = (Option.get !current_decl, fst file, lid, f) in
         Hashtbl.replace deps f dep
     | _ ->
         ()
diff --git a/lib/CFlatToWasm.ml b/lib/CFlatToWasm.ml
index 222e41d96..d5ae3d1a5 100644
--- a/lib/CFlatToWasm.ml
+++ b/lib/CFlatToWasm.ml
@@ -625,10 +625,10 @@ let rec mk_callop2 env (w, o) e1 e2 =
   mk_expr env e2 @
   if is_binop (w, o) then
     mk_binop_conversion (w, o) @
-    [ dummy_phrase (W.Ast.Binary (mk_value size (Option.must (mk_binop (w, o))))) ] @
+    [ dummy_phrase (W.Ast.Binary (mk_value size (Option.get (mk_binop (w, o))))) ] @
     mk_mask w
   else if is_cmpop (w, o) then
-    [ dummy_phrase (W.Ast.Compare (mk_value size (Option.must (mk_cmpop (w, o))))) ] @
+    [ dummy_phrase (W.Ast.Compare (mk_value size (Option.get (mk_cmpop (w, o))))) ] @
     mk_mask w
   else
     failwith "todo mk_callop2"
diff --git a/lib/CStarToC11.ml b/lib/CStarToC11.ml
index 5a302653a..d5fdc24b2 100644
--- a/lib/CStarToC11.ml
+++ b/lib/CStarToC11.ml
@@ -430,7 +430,7 @@ and mk_alloc_cast m t e =
 and mk_malloc m t s =
   match t with
   | Qualified lid when Helpers.is_aligned_type lid ->
-      let sz = Option.must (mk_alignment m t) in
+      let sz = Option.get (mk_alignment m t) in
       mk_alloc_cast m t (C.Call (C.Name "KRML_ALIGNED_MALLOC", [ sz; mk_sizeof_mul m t s ]))
   | _ ->
       mk_alloc_cast m t (C.Call (C.Name "KRML_HOST_MALLOC", [ mk_sizeof_mul m t s ]))
@@ -979,7 +979,7 @@ and mk_expr m (e: expr): C.expr =
   | Struct (typ, fields) ->
       if typ = None then
         failwith ("Expected a type annotation for: \n" ^ show_expr e);
-      let typ = Option.must typ in
+      let typ = Option.get typ in
       mk_compound_literal m typ fields
 
   | Field (BufRead (e, Constant (_, "0")), field) ->
diff --git a/lib/Checker.ml b/lib/Checker.ml
index f357a5617..6e2a00157 100644
--- a/lib/Checker.ml
+++ b/lib/Checker.ml
@@ -236,7 +236,7 @@ and check_fields_opt env fieldexprs fieldtyps =
   if List.length fieldexprs > List.length fieldtyps then
     checker_error env "some fields are superfluous (expr) in %a" pexpr (with_unit (EFlat fieldexprs));
   List.iter (fun (field, expr) ->
-    let field = Option.must field in
+    let field = Option.get field in
     let t, _ = KList.assoc_opt field fieldtyps in
     check env t expr
   ) fieldexprs
@@ -794,7 +794,7 @@ and infer_and_check_eq: 'a. env -> ('a -> typ) -> 'a list -> typ =
     | Some t_base -> check_eqtype env t_base t
     | None -> t_base := Some t
   ) l;
-  Option.must !t_base
+  Option.get !t_base
 
 and find_field env t field =
   match expand_abbrev env t with
@@ -863,7 +863,7 @@ and check_valid_path env e =
   match e.node with
   | EField (e, f) ->
       let t1 = check_valid_path env e in
-      fst (Option.must (find_field env t1 f))
+      fst (Option.get (find_field env t1 f))
 
   | EBufRead _
   | EBound _ ->
diff --git a/lib/Diagnostics.ml b/lib/Diagnostics.ml
index d08e4625b..51fb59c4c 100644
--- a/lib/Diagnostics.ml
+++ b/lib/Diagnostics.ml
@@ -26,7 +26,7 @@ let types_depth files =
     | Abbrev t ->
         depth_of_type p t
     | Flat fields ->
-        incr (KList.max (List.map (fun (f, (t, _)) -> depth_of_type (Option.must f :: p) t) fields))
+        incr (KList.max (List.map (fun (f, (t, _)) -> depth_of_type (Option.get f :: p) t) fields))
     | Forward _
     | Variant _ ->
         failwith "impossible"
diff --git a/lib/Monomorphization.ml b/lib/Monomorphization.ml
index 27f2a6534..1c47a3927 100644
--- a/lib/Monomorphization.ml
+++ b/lib/Monomorphization.ml
@@ -678,7 +678,7 @@ let equalities files =
                 (* Either a conjunction of equalities, or a disjunction of inequalities. *)
                 let def () =
                   let sub_equalities = List.map (fun (f, (t_field, _)) ->
-                    let f = Option.must f in
+                    let f = Option.get f in
                     (* __eq__ x.f y.f *)
                     mk_rec_equality t_field
                       (EField (with_type t (EBound 0), f))
diff --git a/lib/PrintAst.ml b/lib/PrintAst.ml
index 5d0117c7c..d7feede95 100644
--- a/lib/PrintAst.ml
+++ b/lib/PrintAst.ml
@@ -102,7 +102,7 @@ and print_fields_t fields =
 
 and print_fields_opt_t fields =
   separate_map (semi ^^ break1) (fun (ident, (typ, mut)) ->
-    let ident = if ident = None then empty else string (Option.must ident) in
+    let ident = if ident = None then empty else string (Option.get ident) in
     let mut = if mut then string "mutable " else empty in
     group (group (mut ^^ ident ^^ colon) ^/^ print_typ typ)
   ) fields
diff --git a/lib/Simplify.ml b/lib/Simplify.ml
index f6b0ba7bf..4fa8fff33 100644
--- a/lib/Simplify.ml
+++ b/lib/Simplify.ml
@@ -546,7 +546,7 @@ let functional_updates = object (self)
         ) fields in
       if List.length the_field = 1 then
         let the_field, the_expr = List.hd the_field in
-        let the_field = Option.must the_field in
+        let the_field = Option.get the_field in
         let the_expr = self#visit_expr env (snd (open_binder b the_expr)) in
         make_mut <- (assert_tlid e1.typ, the_field) :: make_mut;
         k (EAssign (with_type the_expr.typ (EField (e1, the_field)), the_expr))
@@ -654,7 +654,7 @@ let misc_cosmetic = object (self)
             (* if true then Warn.fatal_error "MATCHED: %a" pexpr (with_unit (ELet (b, e1, e2))); *)
 
             let f, { typ = x_typ; _ } = List.find (fun (_, x) -> x.node = EBound 1) fields in
-            let f = Option.must f in
+            let f = Option.get f in
 
             let e3 = snd (DeBruijn.open_binder b e3) in
             let e4 = snd (DeBruijn.open_binder b (snd (DeBruijn.open_binder b' e4))) in
@@ -670,7 +670,7 @@ let misc_cosmetic = object (self)
                 with_type (TBuf (x_typ, false)) (EAddrOf (
                   with_type x_typ (EField (e4, f))))])) ::
               List.filter_map (fun (f', e) ->
-                let f' = Option.must f' in
+                let f' = Option.get f' in
                 if f = f' then
                   None
                 else
@@ -700,7 +700,7 @@ let misc_cosmetic = object (self)
             (* if true then Warn.fatal_error "MATCHED: %a" pexpr (with_unit (ELet (b, e1, e2))); *)
 
             let f, { typ = x_typ; _ } = List.find (fun (_, x) -> x.node = EBound 1) fields in
-            let f = Option.must f in
+            let f = Option.get f in
 
             let e3 = snd (DeBruijn.open_binder b e3) in
             let e4 = snd (DeBruijn.open_binder b (snd (DeBruijn.open_binder b' e4))) in
@@ -718,7 +718,7 @@ let misc_cosmetic = object (self)
                 with_type (TBuf (x_typ, false)) (EAddrOf (
                   with_type x_typ (EField (e4, f))))])) ::
               List.filter_map (fun (f', e) ->
-                let f' = Option.must f' in
+                let f' = Option.get f' in
                 if f = f' then
                   None
                 else
diff --git a/lib/Structs.ml b/lib/Structs.ml
index 4b0936ffa..ab2b5c65b 100644
--- a/lib/Structs.ml
+++ b/lib/Structs.ml
@@ -228,9 +228,9 @@ let pass_by_ref (should_rewrite: _ -> policy) = object (self)
       if ret_is_struct then
         let assign_into_ret e =
           if ret_is_array then
-            with_type TUnit (EAssign (Option.must ret_atom, e))
+            with_type TUnit (EAssign (Option.get ret_atom, e))
           else
-            with_type TUnit (EBufWrite (Option.must ret_atom, Helpers.zerou32, e))
+            with_type TUnit (EBufWrite (Option.get ret_atom, Helpers.zerou32, e))
         in
         (* Step 4.1: early-returns `return e` become `dst := e; return` *)
         let body = (object
@@ -747,7 +747,7 @@ let remove_literals = object (self)
     match e.node with
     | EFlat fields ->
         List.fold_left (fun acc (f, e) ->
-          let f = Option.must f in
+          let f = Option.get f in
           self#explode acc (f :: path) e dst
         ) acc fields
     | _ ->
diff --git a/lib/lib/Option.ml b/lib/lib/Option.ml
deleted file mode 100644
index 02f95d785..000000000
--- a/lib/lib/Option.ml
+++ /dev/null
@@ -1,20 +0,0 @@
-let must = function
-  | Some x -> x
-  | None -> raise (Invalid_argument "Option.must")
-
-let map f = function
-  | Some x -> Some (f x)
-  | None -> None
-
-let map_or f o d =
-  match o with
-  | Some x -> f x
-  | None -> d
-
-let or_empty = function
-  | Some x -> x
-  | None -> ""
-
-let is_some = function
-  | Some _ -> true
-  | _ -> false