Remove some assumed types and add more support for builtin definitions

24 files changed, 763 insertions, 808 deletions

diff --git a/compiler/Assumed.ml b/compiler/Assumed.ml
index b1ec0660..94fb7a72 100644
--- a/compiler/Assumed.ml
+++ b/compiler/Assumed.ml
@@ -80,8 +80,6 @@ module Sig = struct
   let mk_slice_ty (ty : T.sty) : T.sty =
     Adt (Assumed Slice, mk_generic_args [] [ ty ] [])
 
-  let range_ty : T.sty = Adt (Assumed Range, mk_generic_args [] [ usize_ty ] [])
-
   let mk_sig generics regions_hierarchy inputs output : A.fun_sig =
     let preds : T.predicates =
       { regions_outlive = []; types_outlive = []; trait_type_constraints = [] }
@@ -95,19 +93,6 @@ module Sig = struct
       output;
     }
 
-  (** [fn<T>(&'a mut T, T) -> T] *)
-  let mem_replace_sig : A.fun_sig =
-    (* The signature fields *)
-    let regions = [ region_param_0 ] (* <'a> *) in
-    let regions_hierarchy = [ region_group_0 ] (* [{<'a>}] *) in
-    let types = [ type_param_0 ] (* <T> *) in
-    let generics = mk_generic_params regions types [] in
-    let inputs =
-      [ mk_ref_ty rvar_0 tvar_0 true (* &'a mut T *); tvar_0 (* T *) ]
-    in
-    let output = tvar_0 (* T *) in
-    mk_sig generics regions_hierarchy inputs output
-
   (** [fn<T>(T) -> Box<T>] *)
   let box_new_sig : A.fun_sig =
     let generics = mk_generic_params [] [ type_param_0 ] [] (* <T> *) in
@@ -124,101 +109,6 @@ module Sig = struct
     let output = mk_unit_ty (* () *) in
     mk_sig generics regions_hierarchy inputs output
 
-  (** Helper for [Box::deref_shared] and [Box::deref_mut].
-      Returns:
-      [fn<'a, T>(&'a (mut) Box<T>) -> &'a (mut) T]
-  *)
-  let box_deref_gen_sig (is_mut : bool) : A.fun_sig =
-    let generics =
-      mk_generic_params [ region_param_0 ] [ type_param_0 ] [] (* <'a, T> *)
-    in
-    let regions_hierarchy = [ region_group_0 ] (* <'a> *) in
-    let inputs =
-      [ mk_ref_ty rvar_0 (mk_box_ty tvar_0) is_mut (* &'a (mut) Box<T> *) ]
-    in
-    let output = mk_ref_ty rvar_0 tvar_0 is_mut (* &'a (mut) T *) in
-    mk_sig generics regions_hierarchy inputs output
-
-  (** [fn<'a, T>(&'a Box<T>) -> &'a T] *)
-  let box_deref_shared_sig = box_deref_gen_sig false
-
-  (** [fn<'a, T>(&'a mut Box<T>) -> &'a mut T] *)
-  let box_deref_mut_sig = box_deref_gen_sig true
-
-  (** [fn<T>() -> Vec<T>] *)
-  let vec_new_sig : A.fun_sig =
-    let generics = mk_generic_params [] [ type_param_0 ] [] (* <T> *) in
-    let regions_hierarchy = [] in
-    let inputs = [] in
-    let output = mk_vec_ty tvar_0 (* Vec<T> *) in
-    mk_sig generics regions_hierarchy inputs output
-
-  (** [fn<T>(&'a mut Vec<T>, T)] *)
-  let vec_push_sig : A.fun_sig =
-    let generics =
-      mk_generic_params [ region_param_0 ] [ type_param_0 ] [] (* <'a, T> *)
-    in
-    let regions_hierarchy = [ region_group_0 ] (* <'a> *) in
-    let inputs =
-      [
-        mk_ref_ty rvar_0 (mk_vec_ty tvar_0) true (* &'a mut Vec<T> *);
-        tvar_0 (* T *);
-      ]
-    in
-    let output = mk_unit_ty (* () *) in
-    mk_sig generics regions_hierarchy inputs output
-
-  (** [fn<T>(&'a mut Vec<T>, usize, T)] *)
-  let vec_insert_sig : A.fun_sig =
-    let generics =
-      mk_generic_params [ region_param_0 ] [ type_param_0 ] [] (* <'a, T> *)
-    in
-    let regions_hierarchy = [ region_group_0 ] (* <'a> *) in
-    let inputs =
-      [
-        mk_ref_ty rvar_0 (mk_vec_ty tvar_0) true (* &'a mut Vec<T> *);
-        mk_usize_ty (* usize *);
-        tvar_0 (* T *);
-      ]
-    in
-    let output = mk_unit_ty (* () *) in
-    mk_sig generics regions_hierarchy inputs output
-
-  (** [fn<T>(&'a Vec<T>) -> usize] *)
-  let vec_len_sig : A.fun_sig =
-    let generics =
-      mk_generic_params [ region_param_0 ] [ type_param_0 ] [] (* <'a, T> *)
-    in
-    let regions_hierarchy = [ region_group_0 ] (* <'a> *) in
-    let inputs =
-      [ mk_ref_ty rvar_0 (mk_vec_ty tvar_0) false (* &'a Vec<T> *) ]
-    in
-    let output = mk_usize_ty (* usize *) in
-    mk_sig generics regions_hierarchy inputs output
-
-  (** Helper:
-      [fn<T>(&'a (mut) Vec<T>, usize) -> &'a (mut) T]
-   *)
-  let vec_index_gen_sig (is_mut : bool) : A.fun_sig =
-    let generics =
-      mk_generic_params [ region_param_0 ] [ type_param_0 ] [] (* <'a, T> *)
-    in
-    let regions_hierarchy = [ region_group_0 ] (* <'a> *) in
-    let inputs =
-      [
-        mk_ref_ty rvar_0 (mk_vec_ty tvar_0) is_mut (* &'a (mut) Vec<T> *);
-        mk_usize_ty (* usize *);
-      ]
-    in
-    let output = mk_ref_ty rvar_0 tvar_0 is_mut (* &'a (mut) T *) in
-    mk_sig generics regions_hierarchy inputs output
-
-  (** [fn<T>(&'a Vec<T>, usize) -> &'a T] *)
-  let vec_index_shared_sig : A.fun_sig = vec_index_gen_sig false
-
-  (** [fn<T>(&'a mut Vec<T>, usize) -> &'a mut T] *)
-  let vec_index_mut_sig : A.fun_sig = vec_index_gen_sig true
-
   (** Array/slice functions *)
 
   (** Small helper.
@@ -281,23 +171,6 @@ module Sig = struct
     let cgs = [ cg_param_0 ] in
     mk_array_slice_borrow_sig cgs input_ty None output_ty is_mut
 
-  let mk_array_slice_subslice_sig (is_array : bool) (is_mut : bool) : A.fun_sig
-      =
-    (* Array<T, N> *)
-    let input_ty id =
-      if is_array then mk_array_ty (T.TypeVar id) cgvar_0
-      else mk_slice_ty (T.TypeVar id)
-    in
-    (* Range *)
-    let index_ty = range_ty in
-    (* Slice<T> *)
-    let output_ty id = mk_slice_ty (T.TypeVar id) in
-    let cgs = if is_array then [ cg_param_0 ] else [] in
-    mk_array_slice_borrow_sig cgs input_ty (Some index_ty) output_ty is_mut
-
-  let array_subslice_sig (is_mut : bool) =
-    mk_array_slice_subslice_sig true is_mut
-
   let array_repeat_sig =
     let generics =
       (* <T, N> *)
@@ -311,9 +184,6 @@ module Sig = struct
     in
     mk_sig generics regions_hierarchy inputs output
 
-  let slice_subslice_sig (is_mut : bool) =
-    mk_array_slice_subslice_sig false is_mut
-
   (** Helper:
       [fn<T>(&'a [T]) -> usize]
    *)
@@ -329,7 +199,25 @@ module Sig = struct
     mk_sig generics regions_hierarchy inputs output
 end
 
-type assumed_info = A.assumed_fun_id * A.fun_sig * bool * name
+type raw_assumed_fun_info =
+  A.assumed_fun_id * A.fun_sig * bool * name * bool list option
+
+type assumed_fun_info = {
+  fun_id : A.assumed_fun_id;
+  fun_sig : A.fun_sig;
+  can_fail : bool;
+  name : name;
+  keep_types : bool list option;
+      (** We may want to filter some type arguments.
+
+          For instance, all the `Vec` functions (and the `Vec` type itself) take
+          an `Allocator` type as argument, that we ignore.
+       *)
+}
+
+let mk_assumed_fun_info (raw : raw_assumed_fun_info) : assumed_fun_info =
+  let fun_id, fun_sig, can_fail, name, keep_types = raw in
+  { fun_id; fun_sig; can_fail; name; keep_types }
 
 (** The list of assumed functions and all their information:
     - their signature
@@ -342,96 +230,72 @@ type assumed_info = A.assumed_fun_id * A.fun_sig * bool * name
     a [usize], we have to make sure that vectors are bounded by the max usize.
     As a consequence, [Vec::push] is monadic.
  *)
-let assumed_infos : assumed_info list =
-  let deref_pre = [ "core"; "ops"; "deref" ] in
-  let vec_pre = [ "alloc"; "vec"; "Vec" ] in
-  let index_pre = [ "core"; "ops"; "index" ] in
+let raw_assumed_fun_infos : raw_assumed_fun_info list =
   [
-    (Replace, Sig.mem_replace_sig, false, to_name [ "core"; "mem"; "replace" ]);
-    (BoxNew, Sig.box_new_sig, false, to_name [ "alloc"; "boxed"; "Box"; "new" ]);
+    ( BoxNew,
+      Sig.box_new_sig,
+      false,
+      to_name [ "alloc"; "boxed"; "Box"; "new" ],
+      Some [ true; false ] );
+    (* BoxFree shouldn't be used *)
     ( BoxFree,
       Sig.box_free_sig,
       false,
-      to_name [ "alloc"; "boxed"; "Box"; "free" ] );
-    ( BoxDeref,
-      Sig.box_deref_shared_sig,
-      false,
-      to_name (deref_pre @ [ "Deref"; "deref" ]) );
-    ( BoxDerefMut,
-      Sig.box_deref_mut_sig,
-      false,
-      to_name (deref_pre @ [ "DerefMut"; "deref_mut" ]) );
-    (VecNew, Sig.vec_new_sig, false, to_name (vec_pre @ [ "new" ]));
-    (VecPush, Sig.vec_push_sig, true, to_name (vec_pre @ [ "push" ]));
-    (VecInsert, Sig.vec_insert_sig, true, to_name (vec_pre @ [ "insert" ]));
-    (VecLen, Sig.vec_len_sig, false, to_name (vec_pre @ [ "len" ]));
-    ( VecIndex,
-      Sig.vec_index_shared_sig,
-      true,
-      to_name (index_pre @ [ "Index"; "index" ]) );
-    ( VecIndexMut,
-      Sig.vec_index_mut_sig,
-      true,
-      to_name (index_pre @ [ "IndexMut"; "index_mut" ]) );
+      to_name [ "alloc"; "boxed"; "Box"; "free" ],
+      Some [ true; false ] );
     (* Array Index *)
     ( ArrayIndexShared,
       Sig.array_index_sig false,
       true,
-      to_name [ "@ArrayIndexShared" ] );
-    (ArrayIndexMut, Sig.array_index_sig true, true, to_name [ "@ArrayIndexMut" ]);
+      to_name [ "@ArrayIndexShared" ],
+      None );
+    ( ArrayIndexMut,
+      Sig.array_index_sig true,
+      true,
+      to_name [ "@ArrayIndexMut" ],
+      None );
     (* Array to slice*)
     ( ArrayToSliceShared,
       Sig.array_to_slice_sig false,
       true,
-      to_name [ "@ArrayToSliceShared" ] );
+      to_name [ "@ArrayToSliceShared" ],
+      None );
     ( ArrayToSliceMut,
       Sig.array_to_slice_sig true,
       true,
-      to_name [ "@ArrayToSliceMut" ] );
-    (* Array Subslice *)
-    ( ArraySubsliceShared,
-      Sig.array_subslice_sig false,
-      true,
-      to_name [ "@ArraySubsliceShared" ] );
-    ( ArraySubsliceMut,
-      Sig.array_subslice_sig true,
-      true,
-      to_name [ "@ArraySubsliceMut" ] );
+      to_name [ "@ArrayToSliceMut" ],
+      None );
     (* Array Repeat *)
-    (ArrayRepeat, Sig.array_repeat_sig, false, to_name [ "@ArrayRepeat" ]);
+    (ArrayRepeat, Sig.array_repeat_sig, false, to_name [ "@ArrayRepeat" ], None);
     (* Slice Index *)
     ( SliceIndexShared,
       Sig.slice_index_sig false,
       true,
-      to_name [ "@SliceIndexShared" ] );
-    (SliceIndexMut, Sig.slice_index_sig true, true, to_name [ "@SliceIndexMut" ]);
-    (* Slice Subslice *)
-    ( SliceSubsliceShared,
-      Sig.slice_subslice_sig false,
+      to_name [ "@SliceIndexShared" ],
+      None );
+    ( SliceIndexMut,
+      Sig.slice_index_sig true,
       true,
-      to_name [ "@SliceSubsliceShared" ] );
-    ( SliceSubsliceMut,
-      Sig.slice_subslice_sig true,
-      true,
-      to_name [ "@SliceSubsliceMut" ] );
-    (SliceLen, Sig.slice_len_sig, false, to_name [ "@SliceLen" ]);
+      to_name [ "@SliceIndexMut" ],
+      None );
+    (SliceLen, Sig.slice_len_sig, false, to_name [ "@SliceLen" ], None);
   ]
 
-let get_assumed_info (id : A.assumed_fun_id) : assumed_info =
-  match List.find_opt (fun (id', _, _, _) -> id = id') assumed_infos with
+let assumed_fun_infos : assumed_fun_info list =
+  List.map mk_assumed_fun_info raw_assumed_fun_infos
+
+let get_assumed_fun_info (id : A.assumed_fun_id) : assumed_fun_info =
+  match List.find_opt (fun x -> id = x.fun_id) assumed_fun_infos with
   | Some info -> info
   | None ->
       raise
-        (Failure ("get_assumed_info: not found: " ^ A.show_assumed_fun_id id))
+        (Failure ("get_assumed_fun_info: not found: " ^ A.show_assumed_fun_id id))
 
-let get_assumed_sig (id : A.assumed_fun_id) : A.fun_sig =
-  let _, sg, _, _ = get_assumed_info id in
-  sg
+let get_assumed_fun_sig (id : A.assumed_fun_id) : A.fun_sig =
+  (get_assumed_fun_info id).fun_sig
 
-let get_assumed_name (id : A.assumed_fun_id) : fun_name =
-  let _, _, _, name = get_assumed_info id in
-  name
+let get_assumed_fun_name (id : A.assumed_fun_id) : fun_name =
+  (get_assumed_fun_info id).name
 
-let assumed_can_fail (id : A.assumed_fun_id) : bool =
-  let _, _, b, _ = get_assumed_info id in
-  b
+let assumed_fun_can_fail (id : A.assumed_fun_id) : bool =
+  (get_assumed_fun_info id).can_fail
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 688f6ce3..30c4c27d 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -225,12 +225,9 @@ let assumed_adts () : (assumed_ty * string) list =
         (Result, "Result");
         (Error, "Error");
         (Fuel, "Nat");
-        (Option, "Option");
-        (Vec, "Vec");
         (Array, "Array");
         (Slice, "Slice");
         (Str, "Str");
-        (Range, "Range");
       ]
   | Coq | FStar ->
       [
@@ -238,12 +235,9 @@ let assumed_adts () : (assumed_ty * string) list =
         (Result, "result");
         (Error, "error");
         (Fuel, "nat");
-        (Option, "option");
-        (Vec, "vec");
         (Array, "array");
         (Slice, "slice");
         (Str, "str");
-        (Range, "range");
       ]
   | HOL4 ->
       [
@@ -251,20 +245,17 @@ let assumed_adts () : (assumed_ty * string) list =
         (Result, "result");
         (Error, "error");
         (Fuel, "num");
-        (Option, "option");
-        (Vec, "vec");
         (Array, "array");
         (Slice, "slice");
         (Str, "str");
-        (Range, "range");
       ]
 
 let assumed_struct_constructors () : (assumed_ty * string) list =
   match !backend with
-  | Lean -> [ (Range, "Range.mk"); (Array, "Array.make") ]
-  | Coq -> [ (Range, "mk_range"); (Array, "mk_array") ]
-  | FStar -> [ (Range, "Mkrange"); (Array, "mk_array") ]
-  | HOL4 -> [ (Range, "mk_range"); (Array, "mk_array") ]
+  | Lean -> [ (Array, "Array.make") ]
+  | Coq -> [ (Array, "mk_array") ]
+  | FStar -> [ (Array, "mk_array") ]
+  | HOL4 -> [ (Array, "mk_array") ]
 
 let assumed_variants () : (assumed_ty * VariantId.id * string) list =
   match !backend with
@@ -276,8 +267,6 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list =
         (Error, error_out_of_fuel_id, "OutOfFuel");
         (* No Fuel::Zero on purpose *)
         (* No Fuel::Succ on purpose *)
-        (Option, option_some_id, "Some");
-        (Option, option_none_id, "None");
       ]
   | Coq ->
       [
@@ -287,8 +276,6 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list =
         (Error, error_out_of_fuel_id, "OutOfFuel");
         (Fuel, fuel_zero_id, "O");
         (Fuel, fuel_succ_id, "S");
-        (Option, option_some_id, "Some");
-        (Option, option_none_id, "None");
       ]
   | Lean ->
       [
@@ -297,8 +284,6 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list =
         (Error, error_failure_id, "panic");
         (* No Fuel::Zero on purpose *)
         (* No Fuel::Succ on purpose *)
-        (Option, option_some_id, "some");
-        (Option, option_none_id, "none");
       ]
   | HOL4 ->
       [
@@ -307,8 +292,6 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list =
         (Error, error_failure_id, "Failure");
         (* No Fuel::Zero on purpose *)
         (* No Fuel::Succ on purpose *)
-        (Option, option_some_id, "SOME");
-        (Option, option_none_id, "NONE");
       ]
 
 let assumed_llbc_functions () :
@@ -317,66 +300,30 @@ let assumed_llbc_functions () :
   match !backend with
   | FStar | Coq | HOL4 ->
       [
-        (Replace, None, "mem_replace_fwd");
-        (Replace, rg0, "mem_replace_back");
-        (VecNew, None, "vec_new");
-        (VecPush, None, "vec_push_fwd") (* Shouldn't be used *);
-        (VecPush, rg0, "vec_push_back");
-        (VecInsert, None, "vec_insert_fwd") (* Shouldn't be used *);
-        (VecInsert, rg0, "vec_insert_back");
-        (VecLen, None, "vec_len");
-        (VecIndex, None, "vec_index_fwd");
-        (VecIndex, rg0, "vec_index_back") (* shouldn't be used *);
-        (VecIndexMut, None, "vec_index_mut_fwd");
-        (VecIndexMut, rg0, "vec_index_mut_back");
         (ArrayIndexShared, None, "array_index_shared");
         (ArrayIndexMut, None, "array_index_mut_fwd");
         (ArrayIndexMut, rg0, "array_index_mut_back");
         (ArrayToSliceShared, None, "array_to_slice_shared");
         (ArrayToSliceMut, None, "array_to_slice_mut_fwd");
         (ArrayToSliceMut, rg0, "array_to_slice_mut_back");
-        (ArraySubsliceShared, None, "array_subslice_shared");
-        (ArraySubsliceMut, None, "array_subslice_mut_fwd");
-        (ArraySubsliceMut, rg0, "array_subslice_mut_back");
         (ArrayRepeat, None, "array_repeat");
         (SliceIndexShared, None, "slice_index_shared");
         (SliceIndexMut, None, "slice_index_mut_fwd");
         (SliceIndexMut, rg0, "slice_index_mut_back");
-        (SliceSubsliceShared, None, "slice_subslice_shared");
-        (SliceSubsliceMut, None, "slice_subslice_mut_fwd");
-        (SliceSubsliceMut, rg0, "slice_subslice_mut_back");
         (SliceLen, None, "slice_len");
       ]
   | Lean ->
       [
-        (Replace, None, "mem.replace");
-        (Replace, rg0, "mem.replace_back");
-        (VecNew, None, "Vec.new");
-        (VecPush, None, "Vec.push_fwd") (* Shouldn't be used *);
-        (VecPush, rg0, "Vec.push");
-        (VecInsert, None, "Vec.insert_fwd") (* Shouldn't be used *);
-        (VecInsert, rg0, "Vec.insert");
-        (VecLen, None, "Vec.len");
-        (VecIndex, None, "Vec.index_shared");
-        (VecIndex, rg0, "Vec.index_shared_back") (* shouldn't be used *);
-        (VecIndexMut, None, "Vec.index_mut");
-        (VecIndexMut, rg0, "Vec.index_mut_back");
         (ArrayIndexShared, None, "Array.index_shared");
         (ArrayIndexMut, None, "Array.index_mut");
         (ArrayIndexMut, rg0, "Array.index_mut_back");
         (ArrayToSliceShared, None, "Array.to_slice_shared");
         (ArrayToSliceMut, None, "Array.to_slice_mut");
         (ArrayToSliceMut, rg0, "Array.to_slice_mut_back");
-        (ArraySubsliceShared, None, "Array.subslice_shared");
-        (ArraySubsliceMut, None, "Array.subslice_mut");
-        (ArraySubsliceMut, rg0, "Array.subslice_mut_back");
         (ArrayRepeat, None, "Array.repeat");
         (SliceIndexShared, None, "Slice.index_shared");
         (SliceIndexMut, None, "Slice.index_mut");
         (SliceIndexMut, rg0, "Slice.index_mut_back");
-        (SliceSubsliceShared, None, "Slice.subslice_shared");
-        (SliceSubsliceMut, None, "Slice.subslice_mut");
-        (SliceSubsliceMut, rg0, "Slice.subslice_mut_back");
         (SliceLen, None, "Slice.len");
       ]
 
@@ -850,12 +797,9 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
             | Assumed Result -> "r"
             | Assumed Error -> ConstStrings.error_basename
             | Assumed Fuel -> ConstStrings.fuel_basename
-            | Assumed Option -> "opt"
-            | Assumed Vec -> "v"
             | Assumed Array -> "a"
             | Assumed Slice -> "s"
             | Assumed Str -> "s"
-            | Assumed Range -> "r"
             | Assumed State -> ConstStrings.state_basename
             | AdtId adt_id ->
                 let def = TypeDeclId.Map.find adt_id ctx.type_ctx.type_decls in
@@ -1397,8 +1341,18 @@ and extract_trait_instance_id (ctx : extraction_ctx) (fmt : F.formatter)
  *)
 let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
     extraction_ctx =
+  (* Lookup the builtin information, if there is *)
+  let open ExtractBuiltin in
+  let sname = name_to_simple_name def.name in
+  let info = SimpleNameMap.find_opt sname (builtin_types_map ()) in
   (* Compute and register the type def name *)
-  let ctx = ctx_add_type_decl def ctx in
+  let def_name =
+    match info with
+    | None -> ctx.fmt.type_name def.name
+    | Some info -> info.rust_name
+  in
+  let is_opaque = def.kind = Opaque in
+  let ctx = ctx_add is_opaque (TypeId (AdtId def.def_id)) def_name ctx in
   (* Compute and register:
    * - the variant names, if this is an enumeration
    * - the field names, if this is a structure
@@ -1406,18 +1360,73 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
   let ctx =
     match def.kind with
     | Struct fields ->
+        (* Compute the names *)
+        let field_names, cons_name =
+          match info with
+          | None ->
+              let field_names =
+                FieldId.mapi
+                  (fun fid (field : field) ->
+                    (fid, ctx.fmt.field_name def.name fid field.field_name))
+                  fields
+              in
+              let cons_name = ctx.fmt.struct_constructor def.name in
+              (field_names, cons_name)
+          | Some { body_info = Some (Struct (cons_name, field_names)); _ } ->
+              let field_names =
+                FieldId.mapi
+                  (fun fid (_, name) -> (fid, name))
+                  (List.combine fields field_names)
+              in
+              (field_names, cons_name)
+          | _ -> raise (Failure "Invalid builtin information")
+        in
         (* Add the fields *)
         let ctx =
-          fst
-            (ctx_add_fields def (FieldId.mapi (fun id f -> (id, f)) fields) ctx)
+          List.fold_left
+            (fun ctx (fid, name) ->
+              ctx_add is_opaque (FieldId (AdtId def.def_id, fid)) name ctx)
+            ctx field_names
         in
         (* Add the constructor name *)
-        fst (ctx_add_struct def ctx)
+        ctx_add is_opaque (StructId (AdtId def.def_id)) cons_name ctx
     | Enum variants ->
-        fst
-          (ctx_add_variants def
-             (VariantId.mapi (fun id v -> (id, v)) variants)
-             ctx)
+        let variant_names =
+          match info with
+          | None ->
+              VariantId.mapi
+                (fun variant_id (variant : variant) ->
+                  let name =
+                    ctx.fmt.variant_name def.name variant.variant_name
+                  in
+                  (* Add the type name prefix for Lean *)
+                  let name =
+                    if !Config.backend = Lean then
+                      let type_name = ctx.fmt.type_name def.name in
+                      type_name ^ "." ^ name
+                    else name
+                  in
+                  (variant_id, name))
+                variants
+          | Some { body_info = Some (Enum variant_infos); _ } ->
+              (* We need to compute the map from variant to variant *)
+              let variant_map =
+                StringMap.of_list
+                  (List.map
+                     (fun (info : builtin_enum_variant_info) ->
+                       (info.rust_variant_name, info.extract_variant_name))
+                     variant_infos)
+              in
+              VariantId.mapi
+                (fun variant_id (variant : variant) ->
+                  (variant_id, StringMap.find variant.variant_name variant_map))
+                variants
+          | _ -> raise (Failure "Invalid builtin information")
+        in
+        List.fold_left
+          (fun ctx (vid, vname) ->
+            ctx_add is_opaque (VariantId (AdtId def.def_id, vid)) vname ctx)
+          ctx variant_names
     | Opaque ->
         (* Nothing to do *)
         ctx
diff --git a/compiler/ExtractAssumed.ml b/compiler/ExtractAssumed.ml
deleted file mode 100644
index 7f094b24..00000000
--- a/compiler/ExtractAssumed.ml
+++ /dev/null
@@ -1,61 +0,0 @@
-(** This file declares external identifiers that we catch to map them to
-    definitions coming from the standard libraries in our backends. *)
-
-open Names
-
-type simple_name = string list [@@deriving show, ord]
-
-let name_to_simple_name (s : name) : simple_name =
-  (* We simply ignore the disambiguators *)
-  List.filter_map (function Ident id -> Some id | Disambiguator _ -> None) s
-
-(** Small helper which cuts a string at the occurrences of "::" *)
-let string_to_simple_name (s : string) : simple_name =
-  (* No function to split by using string separator?? *)
-  let name = String.split_on_char ':' s in
-  List.filter (fun s -> s <> "") name
-
-module SimpleNameOrd = struct
-  type t = simple_name
-
-  let compare = compare_simple_name
-  let to_string = show_simple_name
-  let pp_t = pp_simple_name
-  let show_t = show_simple_name
-end
-
-module SimpleNameMap = Collections.MakeMap (SimpleNameOrd)
-
-let assumed_globals : (string * string) list =
-  [
-    (* Min *)
-    ("core::num::usize::MIN", "core_usize_min");
-    ("core::num::u8::MIN", "core_u8_min");
-    ("core::num::u16::MIN", "core_u16_min");
-    ("core::num::u32::MIN", "core_u32_min");
-    ("core::num::u64::MIN", "core_u64_min");
-    ("core::num::u128::MIN", "core_u128_min");
-    ("core::num::isize::MIN", "core_isize_min");
-    ("core::num::i8::MIN", "core_i8_min");
-    ("core::num::i16::MIN", "core_i16_min");
-    ("core::num::i32::MIN", "core_i32_min");
-    ("core::num::i64::MIN", "core_i64_min");
-    ("core::num::i128::MIN", "core_i128_min");
-    (* Max *)
-    ("core::num::usize::MAX", "core_usize_max");
-    ("core::num::u8::MAX", "core_u8_max");
-    ("core::num::u16::MAX", "core_u16_max");
-    ("core::num::u32::MAX", "core_u32_max");
-    ("core::num::u64::MAX", "core_u64_max");
-    ("core::num::u128::MAX", "core_u128_max");
-    ("core::num::isize::MAX", "core_isize_max");
-    ("core::num::i8::MAX", "core_i8_max");
-    ("core::num::i16::MAX", "core_i16_max");
-    ("core::num::i32::MAX", "core_i32_max");
-    ("core::num::i64::MAX", "core_i64_max");
-    ("core::num::i128::MAX", "core_i128_max");
-  ]
-
-let assumed_globals_map : string SimpleNameMap.t =
-  SimpleNameMap.of_list
-    (List.map (fun (x, y) -> (string_to_simple_name x, y)) assumed_globals)
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index a921515b..54f69735 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -5,7 +5,7 @@ open TranslateCore
 module C = Contexts
 module RegionVarId = T.RegionVarId
 module F = Format
-open ExtractAssumed
+open ExtractBuiltin
 
 (** The local logger *)
 let log = L.pure_to_extract_log
@@ -803,15 +803,11 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
             if variant_id = error_failure_id then "@error::Failure"
             else if variant_id = error_out_of_fuel_id then "@error::OutOfFuel"
             else raise (Failure "Unreachable")
-        | Assumed Option ->
-            if variant_id = option_some_id then "@option::Some"
-            else if variant_id = option_none_id then "@option::None"
-            else raise (Failure "Unreachable")
         | Assumed Fuel ->
             if variant_id = fuel_zero_id then "@fuel::0"
             else if variant_id = fuel_succ_id then "@fuel::Succ"
             else raise (Failure "Unreachable")
-        | Assumed (State | Vec | Array | Slice | Str | Range) ->
+        | Assumed (State | Array | Slice | Str) ->
             raise
               (Failure
                  ("Unreachable: variant id ("
@@ -830,9 +826,7 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string =
       let field_name =
         match id with
         | Tuple -> raise (Failure "Unreachable")
-        | Assumed
-            ( State | Result | Error | Fuel | Option | Vec | Array | Slice | Str
-            | Range ) ->
+        | Assumed (State | Result | Error | Fuel | Array | Slice | Str) ->
             (* We can't directly have access to the fields of those types *)
             raise (Failure "Unreachable")
         | AdtId id -> (
@@ -1186,65 +1180,6 @@ let ctx_add_generic_params (generics : generic_params) (ctx : extraction_ctx) :
   let ctx, tcs = ctx_add_local_trait_clauses trait_clauses ctx in
   (ctx, tys, cgs, tcs)
 
-let ctx_add_type_decl_struct (def : type_decl) (ctx : extraction_ctx) :
-    extraction_ctx * string =
-  assert (match def.kind with Struct _ -> true | _ -> false);
-  let is_opaque = false in
-  let cons_name = ctx.fmt.struct_constructor def.name in
-  let ctx = ctx_add is_opaque (StructId (AdtId def.def_id)) cons_name ctx in
-  (ctx, cons_name)
-
-let ctx_add_type_decl (def : type_decl) (ctx : extraction_ctx) : extraction_ctx
-    =
-  let is_opaque = def.kind = Opaque in
-  let def_name = ctx.fmt.type_name def.name in
-  let ctx = ctx_add is_opaque (TypeId (AdtId def.def_id)) def_name ctx in
-  ctx
-
-let ctx_add_field (def : type_decl) (field_id : FieldId.id) (field : field)
-    (ctx : extraction_ctx) : extraction_ctx * string =
-  let is_opaque = false in
-  let name = ctx.fmt.field_name def.name field_id field.field_name in
-  let ctx = ctx_add is_opaque (FieldId (AdtId def.def_id, field_id)) name ctx in
-  (ctx, name)
-
-let ctx_add_fields (def : type_decl) (fields : (FieldId.id * field) list)
-    (ctx : extraction_ctx) : extraction_ctx * string list =
-  List.fold_left_map
-    (fun ctx (vid, v) -> ctx_add_field def vid v ctx)
-    ctx fields
-
-let ctx_add_variant (def : type_decl) (variant_id : VariantId.id)
-    (variant : variant) (ctx : extraction_ctx) : extraction_ctx * string =
-  let is_opaque = false in
-  let name = ctx.fmt.variant_name def.name variant.variant_name in
-  (* Add the type name prefix for Lean *)
-  let name =
-    if !Config.backend = Lean then
-      let type_name = ctx.fmt.type_name def.name in
-      type_name ^ "." ^ name
-    else name
-  in
-  let ctx =
-    ctx_add is_opaque (VariantId (AdtId def.def_id, variant_id)) name ctx
-  in
-  (ctx, name)
-
-let ctx_add_variants (def : type_decl)
-    (variants : (VariantId.id * variant) list) (ctx : extraction_ctx) :
-    extraction_ctx * string list =
-  List.fold_left_map
-    (fun ctx (vid, v) -> ctx_add_variant def vid v ctx)
-    ctx variants
-
-let ctx_add_struct (def : type_decl) (ctx : extraction_ctx) :
-    extraction_ctx * string =
-  assert (match def.kind with Struct _ -> true | _ -> false);
-  let is_opaque = false in
-  let name = ctx.fmt.struct_constructor def.name in
-  let ctx = ctx_add is_opaque (StructId (AdtId def.def_id)) name ctx in
-  (ctx, name)
-
 let ctx_add_decreases_proof (def : fun_decl) (ctx : extraction_ctx) :
     extraction_ctx =
   let is_opaque = false in
@@ -1277,7 +1212,7 @@ let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) :
      to a custom definition in our standard library (for instance, happens
      with "core::num::usize::MAX") *)
   let sname = name_to_simple_name def.name in
-  match SimpleNameMap.find_opt sname assumed_globals_map with
+  match SimpleNameMap.find_opt sname builtin_globals_map with
   | Some name ->
       (* Yes: register the custom binding *)
       ctx_add is_opaque decl name ctx
diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
new file mode 100644
index 00000000..cf5cc70d
--- /dev/null
+++ b/compiler/ExtractBuiltin.ml
@@ -0,0 +1,468 @@
+(** This file declares external identifiers that we catch to map them to
+    definitions coming from the standard libraries in our backends. *)
+
+open Names
+open Config
+
+type simple_name = string list [@@deriving show, ord]
+
+let name_to_simple_name (s : name) : simple_name =
+  (* We simply ignore the disambiguators *)
+  List.filter_map (function Ident id -> Some id | Disambiguator _ -> None) s
+
+(** Small helper which cuts a string at the occurrences of "::" *)
+let string_to_simple_name (s : string) : simple_name =
+  (* No function to split by using string separator?? *)
+  let name = String.split_on_char ':' s in
+  List.filter (fun s -> s <> "") name
+
+module SimpleNameOrd = struct
+  type t = simple_name
+
+  let compare = compare_simple_name
+  let to_string = show_simple_name
+  let pp_t = pp_simple_name
+  let show_t = show_simple_name
+end
+
+module SimpleNameMap = Collections.MakeMap (SimpleNameOrd)
+
+(** Small utility to memoize some computations *)
+let mk_memoized (f : unit -> 'a) : unit -> 'a =
+  let r = ref None in
+  let g () =
+    match !r with
+    | Some x -> x
+    | None ->
+        let x = f () in
+        r := Some x;
+        x
+  in
+  g
+
+let builtin_globals : (string * string) list =
+  [
+    (* Min *)
+    ("core::num::usize::MIN", "core_usize_min");
+    ("core::num::u8::MIN", "core_u8_min");
+    ("core::num::u16::MIN", "core_u16_min");
+    ("core::num::u32::MIN", "core_u32_min");
+    ("core::num::u64::MIN", "core_u64_min");
+    ("core::num::u128::MIN", "core_u128_min");
+    ("core::num::isize::MIN", "core_isize_min");
+    ("core::num::i8::MIN", "core_i8_min");
+    ("core::num::i16::MIN", "core_i16_min");
+    ("core::num::i32::MIN", "core_i32_min");
+    ("core::num::i64::MIN", "core_i64_min");
+    ("core::num::i128::MIN", "core_i128_min");
+    (* Max *)
+    ("core::num::usize::MAX", "core_usize_max");
+    ("core::num::u8::MAX", "core_u8_max");
+    ("core::num::u16::MAX", "core_u16_max");
+    ("core::num::u32::MAX", "core_u32_max");
+    ("core::num::u64::MAX", "core_u64_max");
+    ("core::num::u128::MAX", "core_u128_max");
+    ("core::num::isize::MAX", "core_isize_max");
+    ("core::num::i8::MAX", "core_i8_max");
+    ("core::num::i16::MAX", "core_i16_max");
+    ("core::num::i32::MAX", "core_i32_max");
+    ("core::num::i64::MAX", "core_i64_max");
+    ("core::num::i128::MAX", "core_i128_max");
+  ]
+
+let builtin_globals_map : string SimpleNameMap.t =
+  SimpleNameMap.of_list
+    (List.map (fun (x, y) -> (string_to_simple_name x, y)) builtin_globals)
+
+type builtin_variant_info = { fields : (string * string) list }
+
+type builtin_enum_variant_info = {
+  rust_variant_name : string;
+  extract_variant_name : string;
+  fields : string list option;
+}
+
+type builtin_type_body_info =
+  | Struct of string * string list
+    (* The constructor name and the map for the field names *)
+  | Enum of builtin_enum_variant_info list
+(* For every variant, a map for the field names *)
+
+type builtin_type_info = {
+  rust_name : string;
+  extract_name : string;
+  keep_params : bool list option;
+      (** We might want to filter some of the type parameters.
+
+          For instance, `Vec` type takes a type parameter for the allocator,
+          which we want to ignore.
+       *)
+  body_info : builtin_type_body_info option;
+}
+
+(** The assumed types.
+
+    The optional list of booleans is filtering information for the type
+    parameters. For instance, in the case of the `Vec` functions, there is
+    a type parameter for the allocator to use, which we want to filter.
+ *)
+let builtin_types () : builtin_type_info list =
+  [
+    (* Alloc *)
+    {
+      rust_name = "alloc::alloc::Global";
+      extract_name =
+        (match !backend with
+        | Lean -> "AllocGlobal"
+        | Coq | FStar | HOL4 -> "alloc_global");
+      keep_params = None;
+      body_info = None;
+    };
+    (* Vec *)
+    {
+      rust_name = "alloc::vec::Vec";
+      extract_name =
+        (match !backend with Lean -> "Vec" | Coq | FStar | HOL4 -> "vec");
+      keep_params = Some [ true; false ];
+      body_info = None;
+    };
+    (* Option *)
+    {
+      rust_name = "core::option::Option";
+      extract_name =
+        (match !backend with
+        | Lean -> "Option"
+        | Coq | FStar | HOL4 -> "option");
+      keep_params = None;
+      body_info =
+        Some
+          (Enum
+             [
+               {
+                 rust_variant_name = "None";
+                 extract_variant_name =
+                   (match !backend with
+                   | FStar | Coq -> "None"
+                   | Lean -> "none"
+                   | HOL4 -> "NONE");
+                 fields = None;
+               };
+               {
+                 rust_variant_name = "Some";
+                 extract_variant_name =
+                   (match !backend with
+                   | FStar | Coq -> "Some"
+                   | Lean -> "some"
+                   | HOL4 -> "SOME");
+                 fields = None;
+               };
+             ]);
+    };
+    (* Range *)
+    {
+      rust_name = "core::ops::range::Range";
+      extract_name =
+        (match !backend with Lean -> "Range" | Coq | FStar | HOL4 -> "range");
+      keep_params = None;
+      body_info =
+        Some
+          (Struct
+             ( (match !backend with
+               | Lean -> "Range.mk"
+               | Coq | HOL4 -> "mk_range"
+               | FStar -> "Mkrange"),
+               [ "start"; "end_" ] ));
+    };
+  ]
+
+let mk_builtin_types_map () =
+  SimpleNameMap.of_list
+    (List.map
+       (fun info -> (string_to_simple_name info.rust_name, info))
+       (builtin_types ()))
+
+let builtin_types_map = mk_memoized mk_builtin_types_map
+
+type builtin_fun_info = {
+  rg : Types.RegionGroupId.id option;
+  extract_name : string;
+}
+
+(** The assumed functions.
+
+    The optional list of booleans is filtering information for the type
+    parameters. For instance, in the case of the `Vec` functions, there is
+    a type parameter for the allocator to use, which we want to filter.
+ *)
+let builtin_funs () : (string * bool list option * builtin_fun_info list) list =
+  let rg0 = Some Types.RegionGroupId.zero in
+  [
+    ( "core::mem::replace",
+      None,
+      [
+        {
+          rg = None;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "mem_replace_fwd"
+            | Lean -> "mem.replace");
+        };
+        {
+          rg = rg0;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "mem_replace_back"
+            | Lean -> "mem.replace_back");
+        };
+      ] );
+    ( "alloc::vec::Vec::new",
+      Some [ true; false ],
+      [
+        {
+          rg = None;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "vec_new"
+            | Lean -> "Vec.new");
+        };
+        {
+          rg = rg0;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "vec_new_back"
+            | Lean -> "Vec.new_back");
+        };
+      ] );
+    ( "alloc::vec::Vec::push",
+      Some [ true; false ],
+      [
+        (* The forward function shouldn't be used *)
+        {
+          rg = None;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "vec_push_fwd"
+            | Lean -> "Vec.push_fwd");
+        };
+        {
+          rg = rg0;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "vec_push_back"
+            | Lean -> "Vec.push");
+        };
+      ] );
+    ( "alloc::vec::Vec::insert",
+      Some [ true; false ],
+      [
+        (* The forward function shouldn't be used *)
+        {
+          rg = None;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "vec_insert_fwd"
+            | Lean -> "Vec.insert_fwd");
+        };
+        {
+          rg = rg0;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "vec_insert_back"
+            | Lean -> "Vec.insert");
+        };
+      ] );
+    ( "alloc::vec::Vec::len",
+      Some [ true; false ],
+      [
+        {
+          rg = None;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "vec_len"
+            | Lean -> "Vec.len");
+        };
+      ] );
+    ( "alloc::vec::Vec::index",
+      Some [ true; false ],
+      [
+        {
+          rg = None;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "vec_index_fwd"
+            | Lean -> "Vec.index_shared");
+        };
+        (* The backward function shouldn't be used *)
+        {
+          rg = rg0;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "vec_index_back"
+            | Lean -> "Vec.index_shared_back");
+        };
+      ] );
+    ( "alloc::vec::Vec::index_mut",
+      Some [ true; false ],
+      [
+        {
+          rg = None;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "vec_index_mut_fwd"
+            | Lean -> "Vec.index_mut");
+        };
+        (* The backward function shouldn't be used *)
+        {
+          rg = rg0;
+          extract_name =
+            (match !backend with
+            | FStar | Coq | HOL4 -> "vec_index_mut_back"
+            | Lean -> "Vec.index_mut_back");
+        };
+      ] );
+  ]
+
+let mk_builtin_funs_map () =
+  SimpleNameMap.of_list
+    (List.map
+       (fun (name, filter, info) ->
+         (string_to_simple_name name, (filter, info)))
+       (builtin_funs ()))
+
+let builtin_funs_map () = mk_memoized mk_builtin_funs_map
+
+type builtin_trait_info = {
+  rust_name : string;
+  extract_name : string;
+  parent_clauses : string list;
+  consts : (string * string) list;
+  types : (string * string * string list) list;
+      (** Every type has:
+          - a Rust name
+          - an extraction name
+          - a list of clauses *)
+  funs : (string * Types.RegionGroupId.id option * string) list;
+}
+
+let builtin_traits () =
+  let rg0 = Some Types.RegionGroupId.zero in
+  [
+    {
+      (* Deref *)
+      rust_name = "core::ops::deref::Deref";
+      extract_name =
+        (match !backend with
+        | Coq | FStar | HOL4 -> "core_ops_deref_Deref"
+        | Lean -> "core.ops.deref.Deref");
+      parent_clauses = [];
+      consts = [];
+      types =
+        [
+          ( "Target",
+            (match !backend with
+            | Coq | FStar | HOL4 -> "core_ops_deref_Deref_Target"
+            | Lean -> "Target"),
+            [] );
+        ];
+      funs =
+        [
+          ( "deref",
+            None,
+            match !backend with
+            | Coq | FStar | HOL4 -> "core_ops_deref_Deref_deref"
+            | Lean -> "deref" );
+        ];
+    };
+    {
+      (* DerefMut *)
+      rust_name = "core::ops::deref::DerefMut";
+      extract_name =
+        (match !backend with
+        | Coq | FStar | HOL4 -> "core_ops_deref_DerefMut"
+        | Lean -> "core.ops.deref.DerefMut");
+      parent_clauses =
+        [
+          (match !backend with
+          | Coq | FStar | HOL4 -> "deref_inst"
+          | Lean -> "DerefInst");
+        ];
+      consts = [];
+      types = [];
+      funs =
+        [
+          ( "deref_mut",
+            None,
+            match !backend with
+            | Coq | FStar | HOL4 -> "core_ops_deref_DerefMut_deref_mut"
+            | Lean -> "deref_mut" );
+          ( "deref_mut",
+            rg0,
+            match !backend with
+            | Coq | FStar | HOL4 -> "core_ops_deref_DerefMut_deref_mut_back"
+            | Lean -> "deref_mut_back" );
+        ];
+    };
+    {
+      (* Index *)
+      rust_name = "core::ops::index::Index";
+      extract_name =
+        (match !backend with
+        | Coq | FStar | HOL4 -> "core_ops_index_Index"
+        | Lean -> "core.ops.index.Index");
+      parent_clauses = [];
+      consts = [];
+      types =
+        [
+          ( "Output",
+            (match !backend with
+            | Coq | FStar | HOL4 -> "core_ops_index_Index_Output"
+            | Lean -> "Output"),
+            [] );
+        ];
+      funs =
+        [
+          ( "index",
+            None,
+            match !backend with
+            | Coq | FStar | HOL4 -> "core_ops_index_Index_index"
+            | Lean -> "index" );
+        ];
+    };
+    {
+      (* IndexMut *)
+      rust_name = "core::ops::index::IndexMut";
+      extract_name =
+        (match !backend with
+        | Coq | FStar | HOL4 -> "core_ops_index_IndexMut"
+        | Lean -> "core.ops.index.IndexMut");
+      parent_clauses =
+        [
+          (match !backend with
+          | Coq | FStar | HOL4 -> "index_inst"
+          | Lean -> "IndexInst");
+        ];
+      consts = [];
+      types = [];
+      funs =
+        [
+          ( "index_mut",
+            None,
+            match !backend with
+            | Coq | FStar | HOL4 -> "core_ops_index_IndexMut_mut"
+            | Lean -> "index_mut" );
+          ( "index_mut",
+            rg0,
+            match !backend with
+            | Coq | FStar | HOL4 -> "core_ops_index_IndexMut_mut_back"
+            | Lean -> "index_mut_back" );
+        ];
+    };
+  ]
+
+let mk_builtin_traits_map () =
+  SimpleNameMap.of_list
+    (List.map
+       (fun info -> (string_to_simple_name info.rust_name, info))
+       (builtin_traits ()))
+
+let builtin_traits_map () = mk_memoized mk_builtin_traits_map
diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml
index a09a6d05..5e849ba7 100644
--- a/compiler/FunsAnalysis.ml
+++ b/compiler/FunsAnalysis.ml
@@ -88,7 +88,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
                   can_diverge := !can_diverge || info.can_diverge
             | FunId (Assumed id) ->
                 (* None of the assumed functions can diverge nor are considered stateful *)
-                can_fail := !can_fail || Assumed.assumed_can_fail id
+                can_fail := !can_fail || Assumed.assumed_fun_can_fail id
             | TraitMethod _ ->
                 (* We consider trait functions can fail, diverge, and are not stateful *)
                 can_fail := true;
diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml
index c1041fa3..167e3d58 100644
--- a/compiler/InterpreterExpansion.ml
+++ b/compiler/InterpreterExpansion.ml
@@ -241,17 +241,6 @@ let compute_expanded_symbolic_non_assumed_adt_value (expand_enumerations : bool)
   (* Initialize all the expanded values of all the variants *)
   List.map initialize variants_fields_types
 
-(** Compute the expansion of an Option value.
- *)
-let compute_expanded_symbolic_option_value (expand_enumerations : bool)
-    (kind : V.sv_kind) (ty : T.rty) : V.symbolic_expansion list =
-  assert expand_enumerations;
-  let some_se =
-    V.SeAdt (Some T.option_some_id, [ mk_fresh_symbolic_value kind ty ])
-  in
-  let none_se = V.SeAdt (Some T.option_none_id, []) in
-  [ none_se; some_se ]
-
 let compute_expanded_symbolic_tuple_value (kind : V.sv_kind)
     (field_types : T.rty list) : V.symbolic_expansion =
   (* Generate the field values *)
@@ -286,8 +275,6 @@ let compute_expanded_symbolic_adt_value (expand_enumerations : bool)
         def_id generics ctx
   | T.Tuple, [], _ ->
       [ compute_expanded_symbolic_tuple_value kind generics.types ]
-  | T.Assumed T.Option, [], [ ty ] ->
-      compute_expanded_symbolic_option_value expand_enumerations kind ty
   | T.Assumed T.Box, [], [ boxed_ty ] ->
       [ compute_expanded_symbolic_box_value kind boxed_ty ]
   | _ ->
@@ -704,7 +691,7 @@ let greedy_expand_symbolics_with_borrows (config : C.config) : cm_fun =
         | T.Adt ((Tuple | Assumed Box), _) | T.Ref (_, _, _) ->
             (* Ok *)
             expand_symbolic_value_no_branching config sv None
-        | T.Adt (Assumed (Vec | Option | Array | Slice | Str | Range), _) ->
+        | T.Adt (Assumed (Array | Slice | Str), _) ->
             (* We can't expand those *)
             raise
               (Failure
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index a42c552a..341e97eb 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -142,10 +142,10 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config)
   | V.Adt av ->
       (* Sanity check *)
       (match v.V.ty with
-      | T.Adt (T.Assumed (T.Box | Vec), _) ->
+      | T.Adt (T.Assumed T.Box, _) ->
           raise (Failure "Can't copy an assumed value other than Option")
       | T.Adt (T.AdtId _, _) -> assert allow_adt_copy
-      | T.Adt ((T.Assumed Option | T.Tuple), _) -> () (* Ok *)
+      | T.Adt (T.Tuple, _) -> () (* Ok *)
       | T.Adt
           ( T.Assumed (Slice | T.Array),
             {
@@ -722,70 +722,38 @@ let eval_rvalue_aggregate (config : C.config)
    fun ctx ->
     (* Match on the aggregate kind *)
     match aggregate_kind with
-    | E.AggregatedTuple ->
-        let tys = List.map (fun (v : V.typed_value) -> v.V.ty) values in
-        let v = V.Adt { variant_id = None; field_values = values } in
-        let generics = TypesUtils.mk_generic_args [] tys [] [] in
-        let ty = T.Adt (T.Tuple, generics) in
-        let aggregated : V.typed_value = { V.value = v; ty } in
-        (* Call the continuation *)
-        cf aggregated ctx
-    | E.AggregatedOption (variant_id, ty) ->
-        (* Sanity check *)
-        if variant_id = T.option_none_id then assert (values = [])
-        else if variant_id = T.option_some_id then
-          assert (List.length values = 1)
-        else raise (Failure "Unreachable");
-        (* Construt the value *)
-        let generics = TypesUtils.mk_generic_args [] [ ty ] [] [] in
-        let aty = T.Adt (T.Assumed T.Option, generics) in
-        let av : V.adt_value =
-          { V.variant_id = Some variant_id; V.field_values = values }
-        in
-        let aggregated : V.typed_value = { V.value = Adt av; ty = aty } in
-        (* Call the continuation *)
-        cf aggregated ctx
-    | E.AggregatedAdt (def_id, opt_variant_id, generics) ->
-        (* Sanity checks *)
-        let type_decl = C.ctx_lookup_type_decl ctx def_id in
-        assert (
-          List.length type_decl.generics.regions = List.length generics.regions);
-        let expected_field_types =
-          Assoc.ctx_adt_get_inst_norm_field_etypes ctx def_id opt_variant_id
-            generics
-        in
-        assert (
-          expected_field_types
-          = List.map (fun (v : V.typed_value) -> v.V.ty) values);
-        (* Construct the value *)
-        let av : V.adt_value =
-          { V.variant_id = opt_variant_id; V.field_values = values }
-        in
-        let aty = T.Adt (T.AdtId def_id, generics) in
-        let aggregated : V.typed_value = { V.value = Adt av; ty = aty } in
-        (* Call the continuation *)
-        cf aggregated ctx
-    | E.AggregatedRange ety ->
-        (* There should be two fields exactly *)
-        let v0, v1 =
-          match values with
-          | [ v0; v1 ] -> (v0, v1)
-          | _ -> raise (Failure "Unreachable")
-        in
-        (* Ranges are parametric over the type of indices. For now we only
-           support scalars, which can be of any type *)
-        assert (literal_type_is_integer (ty_as_literal ety));
-        assert (v0.ty = ety);
-        assert (v1.ty = ety);
-        (* Construct the value *)
-        let av : V.adt_value =
-          { V.variant_id = None; V.field_values = values }
-        in
-        let generics = TypesUtils.mk_generic_args_from_types [ ety ] in
-        let aty = T.Adt (T.Assumed T.Range, generics) in
-        let aggregated : V.typed_value = { V.value = Adt av; ty = aty } in
-        (* Call the continuation *)
-        cf aggregated ctx
+    | E.AggregatedAdt (type_id, opt_variant_id, generics) -> (
+        match type_id with
+        | Tuple ->
+            let tys = List.map (fun (v : V.typed_value) -> v.V.ty) values in
+            let v = V.Adt { variant_id = None; field_values = values } in
+            let generics = TypesUtils.mk_generic_args [] tys [] [] in
+            let ty = T.Adt (T.Tuple, generics) in
+            let aggregated : V.typed_value = { V.value = v; ty } in
+            (* Call the continuation *)
+            cf aggregated ctx
+        | AdtId def_id ->
+            (* Sanity checks *)
+            let type_decl = C.ctx_lookup_type_decl ctx def_id in
+            assert (
+              List.length type_decl.generics.regions
+              = List.length generics.regions);
+            let expected_field_types =
+              Assoc.ctx_adt_get_inst_norm_field_etypes ctx def_id opt_variant_id
+                generics
+            in
+            assert (
+              expected_field_types
+              = List.map (fun (v : V.typed_value) -> v.V.ty) values);
+            (* Construct the value *)
+            let av : V.adt_value =
+              { V.variant_id = opt_variant_id; V.field_values = values }
+            in
+            let aty = T.Adt (T.AdtId def_id, generics) in
+            let aggregated : V.typed_value = { V.value = Adt av; ty = aty } in
+            (* Call the continuation *)
+            cf aggregated ctx
+        | Assumed _ -> raise (Failure "Unreachable"))
     | E.AggregatedArray (ety, cg) -> (
         (* Sanity check: all the values have the proper type *)
         assert (List.for_all (fun (v : V.typed_value) -> v.V.ty = ety) values);
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index 465d0028..2a277c91 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -96,7 +96,7 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
   | pe :: p' -> (
       (* Match on the projection element and the value *)
       match (pe, v.V.value, v.V.ty) with
-      | ( Field (((ProjAdt (_, _) | ProjOption _) as proj_kind), field_id),
+      | ( Field ((ProjAdt (_, _) as proj_kind), field_id),
           V.Adt adt,
           T.Adt (type_id, _) ) -> (
           (* Check consistency *)
@@ -104,8 +104,6 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
           | ProjAdt (def_id, opt_variant_id), T.AdtId def_id' ->
               assert (def_id = def_id');
               assert (opt_variant_id = adt.variant_id)
-          | ProjOption variant_id, T.Assumed T.Option ->
-              assert (Some variant_id = adt.variant_id)
           | _ -> raise (Failure "Unreachable"));
           (* Actually project *)
           let fv = T.FieldId.nth adt.field_values field_id in
@@ -136,7 +134,7 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
               Ok (ctx, { res with updated })
           (* If we reach Bottom, it may mean we need to expand an uninitialized
            * enumeration value *))
-      | Field ((ProjAdt (_, _) | ProjTuple _ | ProjOption _), _), V.Bottom, _ ->
+      | Field ((ProjAdt (_, _) | ProjTuple _), _), V.Bottom, _ ->
           Error (FailBottom (1 + List.length p', pe, v.ty))
       (* Symbolic value: needs to be expanded *)
       | _, Symbolic sp, _ ->
@@ -376,20 +374,6 @@ let compute_expanded_bottom_adt_value (ctx : C.eval_ctx)
   let ty = T.Adt (T.AdtId def_id, generics) in
   { V.value = av; V.ty }
 
-let compute_expanded_bottom_option_value (variant_id : T.VariantId.id)
-    (param_ty : T.ety) : V.typed_value =
-  (* Note that the variant can be [Some] or [None]: we expand bottom values
-   * when writing to fields or setting discriminants *)
-  let field_values =
-    if variant_id = T.option_some_id then [ mk_bottom param_ty ]
-    else if variant_id = T.option_none_id then []
-    else raise (Failure "Unreachable")
-  in
-  let av = V.Adt { variant_id = Some variant_id; field_values } in
-  let generics = TypesUtils.mk_generic_args [] [ param_ty ] [] [] in
-  let ty = T.Adt (T.Assumed T.Option, generics) in
-  { V.value = av; ty }
-
 let compute_expanded_bottom_tuple_value (field_types : T.ety list) :
     V.typed_value =
   (* Generate the field values *)
@@ -451,17 +435,6 @@ let expand_bottom_value_from_projection (access : access_kind) (p : E.place)
         T.Adt (T.AdtId def_id', generics) ) ->
         assert (def_id = def_id');
         compute_expanded_bottom_adt_value ctx def_id opt_variant_id generics
-    (* Option *)
-    | ( Field (ProjOption variant_id, _),
-        T.Adt
-          ( T.Assumed T.Option,
-            {
-              T.regions = [];
-              types = [ ty ];
-              const_generics = [];
-              trait_refs = [];
-            } ) ) ->
-        compute_expanded_bottom_option_value variant_id ty
     (* Tuples *)
     | ( Field (ProjTuple arity, _),
         T.Adt
diff --git a/compiler/InterpreterPaths.mli b/compiler/InterpreterPaths.mli
index 041b0a97..0ff8063f 100644
--- a/compiler/InterpreterPaths.mli
+++ b/compiler/InterpreterPaths.mli
@@ -63,10 +63,6 @@ val compute_expanded_bottom_adt_value :
   T.egeneric_args ->
   V.typed_value
 
-(** Compute an expanded [Option] ⊥ value *)
-val compute_expanded_bottom_option_value :
-  T.VariantId.id -> T.ety -> V.typed_value
-
 (** Drop (end) outer loans at a given place, which should be seen as an l-value
     (we will write to it later, but need to drop the loans before writing).
 
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 9f35c6f2..2aced79f 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -10,7 +10,6 @@ open TypesUtils
 open ValuesUtils
 module Inv = Invariants
 module S = SynthesizeSymbolic
-open Utils
 open Cps
 open InterpreterUtils
 open InterpreterProjectors
@@ -233,8 +232,7 @@ let set_discriminant (config : C.config) (p : E.place)
   let update_value cf (v : V.typed_value) : m_fun =
    fun ctx ->
     match (v.V.ty, v.V.value) with
-    | T.Adt (((T.AdtId _ | T.Assumed T.Option) as type_id), generics), V.Adt av
-      -> (
+    | T.Adt ((T.AdtId _ as type_id), generics), V.Adt av -> (
         (* There are two situations:
            - either the discriminant is already the proper one (in which case we
              don't do anything)
@@ -253,24 +251,15 @@ let set_discriminant (config : C.config) (p : E.place)
                 | T.AdtId def_id ->
                     compute_expanded_bottom_adt_value ctx def_id
                       (Some variant_id) generics
-                | T.Assumed T.Option ->
-                    assert (generics.regions = []);
-                    compute_expanded_bottom_option_value variant_id
-                      (Collections.List.to_cons_nil generics.types)
                 | _ -> raise (Failure "Unreachable")
               in
               assign_to_place config bottom_v p (cf Unit) ctx)
-    | T.Adt (((T.AdtId _ | T.Assumed T.Option) as type_id), generics), V.Bottom
-      ->
+    | T.Adt ((T.AdtId _ as type_id), generics), V.Bottom ->
         let bottom_v =
           match type_id with
           | T.AdtId def_id ->
               compute_expanded_bottom_adt_value ctx def_id (Some variant_id)
                 generics
-          | T.Assumed T.Option ->
-              assert (generics.regions = []);
-              compute_expanded_bottom_option_value variant_id
-                (Collections.List.to_cons_nil generics.types)
           | _ -> raise (Failure "Unreachable")
         in
         assign_to_place config bottom_v p (cf Unit) ctx
@@ -313,7 +302,7 @@ let get_assumed_function_return_type (ctx : C.eval_ctx) (fid : A.assumed_fun_id)
       mk_unit_ty
   | _ ->
       (* Retrieve the function's signature *)
-      let sg = Assumed.get_assumed_sig fid in
+      let sg = Assumed.get_assumed_fun_sig fid in
       (* Instantiate the return type  *)
       (* There shouldn't be any reference to Self *)
       let tr_self : T.erased_region T.trait_instance_id =
@@ -427,11 +416,6 @@ let pop_frame_assign (config : C.config) (dest : E.place) : cm_fun =
   comp cf_pop cf_assign
 
 (** Auxiliary function - see {!eval_assumed_function_call} *)
-let eval_replace_concrete (_config : C.config) (_generics : T.egeneric_args) :
-    cm_fun =
- fun _cf _ctx -> raise Unimplemented
-
-(** Auxiliary function - see {!eval_assumed_function_call} *)
 let eval_box_new_concrete (config : C.config) (generics : T.egeneric_args) :
     cm_fun =
  fun cf ctx ->
@@ -475,67 +459,6 @@ let eval_box_new_concrete (config : C.config) (generics : T.egeneric_args) :
       comp cf_move cf_create cf ctx
   | _ -> raise (Failure "Inconsistent state")
 
-(** Auxiliary function which factorizes code to evaluate [std::Deref::deref]
-    and [std::DerefMut::deref_mut] - see {!eval_assumed_function_call} *)
-let eval_box_deref_mut_or_shared_concrete (config : C.config)
-    (generics : T.egeneric_args) (is_mut : bool) : cm_fun =
- fun cf ctx ->
-  (* Check the arguments *)
-  match
-    (generics.regions, generics.types, generics.const_generics, ctx.env)
-  with
-  | ( [],
-      [ boxed_ty ],
-      [],
-      Var (VarBinder input_var, input_value)
-      :: Var (_ret_var, _)
-      :: C.Frame :: _ ) ->
-      (* Required type checking. We must have:
-         - input_value.ty = & (mut) Box<ty>
-         - boxed_ty = ty
-         for some ty
-      *)
-      (let _, input_ty, ref_kind = ty_get_ref input_value.V.ty in
-       assert (match ref_kind with T.Shared -> not is_mut | T.Mut -> is_mut);
-       let input_ty = ty_get_box input_ty in
-       assert (input_ty = boxed_ty));
-
-      (* Borrow the boxed value *)
-      let p =
-        { E.var_id = input_var.C.index; projection = [ E.Deref; E.DerefBox ] }
-      in
-      let borrow_kind = if is_mut then E.Mut else E.Shared in
-      let rv = E.RvRef (p, borrow_kind) in
-      let cf_borrow = eval_rvalue_not_global config rv in
-
-      (* Move the borrow to its destination *)
-      let cf_move cf res : m_fun =
-        match res with
-        | Error EPanic ->
-            (* We can't get there by borrowing a value *)
-            raise (Failure "Unreachable")
-        | Ok borrowed_value ->
-            (* Move and continue *)
-            let destp = mk_place_from_var_id E.VarId.zero in
-            assign_to_place config borrowed_value destp cf
-      in
-
-      (* Compose and apply *)
-      comp cf_borrow cf_move cf ctx
-  | _ -> raise (Failure "Inconsistent state")
-
-(** Auxiliary function - see {!eval_assumed_function_call} *)
-let eval_box_deref_concrete (config : C.config) (generics : T.egeneric_args) :
-    cm_fun =
-  let is_mut = false in
-  eval_box_deref_mut_or_shared_concrete config generics is_mut
-
-(** Auxiliary function - see {!eval_assumed_function_call} *)
-let eval_box_deref_mut_concrete (config : C.config) (generics : T.egeneric_args)
-    : cm_fun =
-  let is_mut = true in
-  eval_box_deref_mut_or_shared_concrete config generics is_mut
-
 (** Auxiliary function - see {!eval_assumed_function_call}.
 
     [Box::free] is not handled the same way as the other assumed functions:
@@ -575,11 +498,6 @@ let eval_box_free (config : C.config) (generics : T.egeneric_args)
       cc cf ctx
   | _ -> raise (Failure "Inconsistent state")
 
-(** Auxiliary function - see {!eval_assumed_function_call} *)
-let eval_vec_function_concrete (_config : C.config) (_fid : A.assumed_fun_id)
-    (_generics : T.egeneric_args) : cm_fun =
- fun _cf _ctx -> raise Unimplemented
-
 (** Evaluate a non-local function call in concrete mode *)
 let eval_assumed_function_call_concrete (config : C.config)
     (fid : A.assumed_fun_id) (call : A.call) : cm_fun =
@@ -636,18 +554,12 @@ let eval_assumed_function_call_concrete (config : C.config)
          * access to a body. *)
         let cf_eval_body : cm_fun =
           match fid with
-          | Replace -> eval_replace_concrete config generics
           | BoxNew -> eval_box_new_concrete config generics
-          | BoxDeref -> eval_box_deref_concrete config generics
-          | BoxDerefMut -> eval_box_deref_mut_concrete config generics
           | BoxFree ->
               (* Should have been treated above *) raise (Failure "Unreachable")
-          | VecNew | VecPush | VecInsert | VecLen | VecIndex | VecIndexMut ->
-              eval_vec_function_concrete config fid generics
           | ArrayIndexShared | ArrayIndexMut | ArrayToSliceShared
-          | ArrayToSliceMut | ArraySubsliceShared | ArraySubsliceMut
-          | ArrayRepeat | SliceIndexShared | SliceIndexMut | SliceSubsliceShared
-          | SliceSubsliceMut | SliceLen ->
+          | ArrayToSliceMut | ArrayRepeat | SliceIndexShared | SliceIndexMut
+          | SliceLen ->
               raise (Failure "Unimplemented")
         in
 
@@ -1531,7 +1443,7 @@ and eval_assumed_function_call_symbolic (config : C.config)
             (* There shouldn't be any reference to Self *)
             let tr_self = T.UnknownTrait __FUNCTION__ in
             instantiate_fun_sig ctx generics tr_self
-              (Assumed.get_assumed_sig fid)
+              (Assumed.get_assumed_fun_sig fid)
       in
 
       (* Evaluate the function call *)
diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml
index 9ac5ce13..5c8ec7af 100644
--- a/compiler/Invariants.ml
+++ b/compiler/Invariants.ml
@@ -447,7 +447,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
               fields_with_types
         (* Assumed type case *)
         | V.Adt av, T.Adt (T.Assumed aty_id, generics) -> (
-            assert (av.V.variant_id = None || aty_id = T.Option);
+            assert (av.V.variant_id = None);
             match
               ( aty_id,
                 av.V.field_values,
@@ -456,19 +456,8 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
                 generics.const_generics )
             with
             (* Box *)
-            | T.Box, [ inner_value ], [], [ inner_ty ], []
-            | T.Option, [ inner_value ], [], [ inner_ty ], [] ->
+            | T.Box, [ inner_value ], [], [ inner_ty ], [] ->
                 assert (inner_value.V.ty = inner_ty)
-            | T.Option, _, [], [ _ ], [] ->
-                (* Option::None: nothing to check *)
-                ()
-            | T.Vec, fvs, [], [ vec_ty ], [] ->
-                List.iter
-                  (fun (v : V.typed_value) -> assert (v.ty = vec_ty))
-                  fvs
-            | T.Range, [ v0; v1 ], [], [ inner_ty ], [] ->
-                assert (v0.V.ty = inner_ty);
-                assert (v1.V.ty = inner_ty)
             | T.Array, inner_values, _, [ inner_ty ], [ cg ] ->
                 (* *)
                 assert (
diff --git a/compiler/LlbcAstUtils.ml b/compiler/LlbcAstUtils.ml
index a982af30..2553127a 100644
--- a/compiler/LlbcAstUtils.ml
+++ b/compiler/LlbcAstUtils.ml
@@ -5,13 +5,13 @@ let lookup_fun_sig (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) :
     fun_sig =
   match fun_id with
   | Regular id -> (FunDeclId.Map.find id fun_decls).signature
-  | Assumed aid -> Assumed.get_assumed_sig aid
+  | Assumed aid -> Assumed.get_assumed_fun_sig aid
 
 let lookup_fun_name (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) :
     Names.fun_name =
   match fun_id with
   | Regular id -> (FunDeclId.Map.find id fun_decls).name
-  | Assumed aid -> Assumed.get_assumed_name aid
+  | Assumed aid -> Assumed.get_assumed_fun_name aid
 
 (** Return the opaque declarations found in the crate.
 
@@ -22,7 +22,7 @@ let lookup_fun_name (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) :
  *)
 let crate_get_opaque_decls (k : crate) (filter_assumed : bool) :
     T.type_decl list * fun_decl list =
-  let open ExtractAssumed in
+  let open ExtractBuiltin in
   let is_opaque_fun (d : fun_decl) : bool =
     let sname = name_to_simple_name d.name in
     d.body = None
@@ -30,7 +30,7 @@ let crate_get_opaque_decls (k : crate) (filter_assumed : bool) :
        (which don't have a body but must not be considered as opaque) *)
     && (match d.kind with TraitMethodDecl _ -> false | _ -> true)
     && ((not filter_assumed)
-       || not (SimpleNameMap.mem sname assumed_globals_map))
+       || not (SimpleNameMap.mem sname builtin_globals_map))
   in
   let is_opaque_type (d : T.type_decl) : bool = d.kind = T.Opaque in
   (* Note that by checking the function bodies we also the globals *)
diff --git a/compiler/PrePasses.ml b/compiler/PrePasses.ml
index 1058fab0..ee06fa07 100644
--- a/compiler/PrePasses.ml
+++ b/compiler/PrePasses.ml
@@ -108,7 +108,7 @@ let remove_useless_cf_merges (crate : A.crate) (f : A.fun_decl) : A.fun_decl =
     | Assign (_, rv) -> (
         match rv with
         | Use _ | RvRef _ -> not must_end_with_exit
-        | Aggregate (AggregatedTuple, []) -> not must_end_with_exit
+        | Aggregate (AggregatedAdt (Tuple, _, _), []) -> not must_end_with_exit
         | _ -> false)
     | FakeRead _ | Drop _ | Nop -> not must_end_with_exit
     | Panic | Return -> true
diff --git a/compiler/Print.ml b/compiler/Print.ml
index 1d5ddc50..aeacfbf0 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -127,17 +127,6 @@ module Values = struct
             (* Assumed type *)
             match (aty, field_values) with
             | Box, [ bv ] -> "@Box(" ^ bv ^ ")"
-            | Option, _ ->
-                if av.variant_id = Some T.option_some_id then
-                  "@Option::Some("
-                  ^ Collections.List.to_cons_nil field_values
-                  ^ ")"
-                else if av.variant_id = Some T.option_none_id then (
-                  assert (field_values = []);
-                  "@Option::None")
-                else raise (Failure "Unreachable")
-            | Range, _ -> "@Range{ " ^ String.concat ", " field_values ^ "}"
-            | Vec, _ -> "@Vec[" ^ String.concat ", " field_values ^ "]"
             | Array, _ ->
                 (* Happens when we aggregate values *)
                 "@Array[" ^ String.concat ", " field_values ^ "]"
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index be7b3cb4..6396fe96 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -195,12 +195,9 @@ let assumed_ty_to_string (aty : assumed_ty) : string =
   | Result -> "Result"
   | Error -> "Error"
   | Fuel -> "Fuel"
-  | Option -> "Option"
-  | Vec -> "Vec"
   | Array -> "Array"
   | Slice -> "Slice"
   | Str -> "Str"
-  | Range -> "Range"
 
 let type_id_to_string (fmt : type_formatter) (id : type_id) : string =
   match id with
@@ -354,10 +351,6 @@ let rec mprojection_to_string (fmt : ast_formatter) (inside : string)
   | pe :: p' -> (
       let s = mprojection_to_string fmt inside p' in
       match pe.pkind with
-      | E.ProjOption variant_id ->
-          assert (variant_id = T.option_some_id);
-          assert (pe.field_id = T.FieldId.zero);
-          "(" ^ s ^ "as Option::Some)." ^ T.FieldId.to_string pe.field_id
       | E.ProjTuple _ -> "(" ^ s ^ ")." ^ T.FieldId.to_string pe.field_id
       | E.ProjAdt (adt_id, opt_variant_id) -> (
           let field_name =
@@ -395,8 +388,6 @@ let adt_variant_to_string (fmt : value_formatter) (adt_id : type_id)
       | State | Array | Slice | Str ->
           (* Those types are opaque: we can't get there *)
           raise (Failure "Unreachable")
-      | Vec -> "@Vec"
-      | Range -> "@Range"
       | Result ->
           let variant_id = Option.get variant_id in
           if variant_id = result_return_id then "@Result::Return"
@@ -412,13 +403,7 @@ let adt_variant_to_string (fmt : value_formatter) (adt_id : type_id)
           let variant_id = Option.get variant_id in
           if variant_id = fuel_zero_id then "@Fuel::Zero"
           else if variant_id = fuel_succ_id then "@Fuel::Succ"
-          else raise (Failure "Unreachable: improper variant id for fuel type")
-      | Option ->
-          let variant_id = Option.get variant_id in
-          if variant_id = option_some_id then "@Option::Some "
-          else if variant_id = option_none_id then "@Option::None"
-          else
-            raise (Failure "Unreachable: improper variant id for result type"))
+          else raise (Failure "Unreachable: improper variant id for fuel type"))
 
 let adt_field_to_string (fmt : value_formatter) (adt_id : type_id)
     (field_id : FieldId.id) : string =
@@ -435,11 +420,10 @@ let adt_field_to_string (fmt : value_formatter) (adt_id : type_id)
   | Assumed aty -> (
       (* Assumed type *)
       match aty with
-      | Range -> FieldId.to_string field_id
-      | State | Fuel | Vec | Array | Slice | Str ->
+      | State | Fuel | Array | Slice | Str ->
           (* Opaque types: we can't get there *)
           raise (Failure "Unreachable")
-      | Result | Error | Option ->
+      | Result | Error ->
           (* Enumerations: we can't get there *)
           raise (Failure "Unreachable"))
 
@@ -510,31 +494,13 @@ let adt_g_value_to_string (fmt : value_formatter)
             | [ v ] -> "@Fuel::Succ " ^ v
             | _ -> raise (Failure "@Fuel::Succ takes exactly one value")
           else raise (Failure "Unreachable: improper variant id for fuel type")
-      | Option ->
-          let variant_id = Option.get variant_id in
-          if variant_id = option_some_id then
-            match field_values with
-            | [ v ] -> "@Option::Some " ^ v
-            | _ -> raise (Failure "Option::Some takes exactly one value")
-          else if variant_id = option_none_id then (
-            assert (field_values = []);
-            "@Option::None")
-          else
-            raise (Failure "Unreachable: improper variant id for result type")
-      | Vec | Array | Slice | Str ->
-          assert (variant_id = None);
-          let field_values =
-            List.mapi (fun i v -> string_of_int i ^ " -> " ^ v) field_values
-          in
-          let id = assumed_ty_to_string aty in
-          id ^ " [" ^ String.concat "; " field_values ^ "]"
-      | Range ->
+      | Array | Slice | Str ->
           assert (variant_id = None);
           let field_values =
             List.mapi (fun i v -> string_of_int i ^ " -> " ^ v) field_values
           in
           let id = assumed_ty_to_string aty in
-          id ^ " {" ^ String.concat "; " field_values ^ "}")
+          id ^ " [" ^ String.concat "; " field_values ^ "]")
   | _ ->
       let fmt = value_to_type_formatter fmt in
       raise
@@ -593,29 +559,16 @@ let fun_suffix (lp_id : LoopId.id option) (rg_id : T.RegionGroupId.id option) :
 
 let llbc_assumed_fun_id_to_string (fid : A.assumed_fun_id) : string =
   match fid with
-  | Replace -> "core::mem::replace"
   | BoxNew -> "alloc::boxed::Box::new"
-  | BoxDeref -> "core::ops::deref::Deref::deref"
-  | BoxDerefMut -> "core::ops::deref::DerefMut::deref_mut"
   | BoxFree -> "alloc::alloc::box_free"
-  | VecNew -> "alloc::vec::Vec::new"
-  | VecPush -> "alloc::vec::Vec::push"
-  | VecInsert -> "alloc::vec::Vec::insert"
-  | VecLen -> "alloc::vec::Vec::len"
-  | VecIndex -> "core::ops::index::Index<alloc::vec::Vec>::index"
-  | VecIndexMut -> "core::ops::index::IndexMut<alloc::vec::Vec>::index_mut"
   | ArrayIndexShared -> "@ArrayIndexShared"
   | ArrayIndexMut -> "@ArrayIndexMut"
   | ArrayToSliceShared -> "@ArrayToSliceShared"
   | ArrayToSliceMut -> "@ArrayToSliceMut"
-  | ArraySubsliceShared -> "@ArraySubsliceShared"
-  | ArraySubsliceMut -> "@ArraySubsliceMut"
   | ArrayRepeat -> "@ArrayRepeat"
   | SliceLen -> "@SliceLen"
   | SliceIndexShared -> "@SliceIndexShared"
   | SliceIndexMut -> "@SliceIndexMut"
-  | SliceSubsliceShared -> "@SliceSubsliceShared"
-  | SliceSubsliceMut -> "@SliceSubsliceMut"
 
 let pure_assumed_fun_id_to_string (fid : pure_assumed_fun_id) : string =
   match fid with
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 47c7beb4..81e13af7 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -64,17 +64,7 @@ type fun_decl_id = A.fun_decl_id [@@deriving show, ord]
         this state is opaque to Aeneas (the user can define it, or leave it as
         assumed)
   *)
-type assumed_ty =
-  | State
-  | Result
-  | Error
-  | Fuel
-  | Vec
-  | Option
-  | Array
-  | Slice
-  | Str
-  | Range
+type assumed_ty = State | Result | Error | Fuel | Array | Slice | Str
 [@@deriving show, ord]
 
 (* TODO: we should never directly manipulate [Return] and [Fail], but rather
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index b00509a6..a326d19e 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -1513,7 +1513,7 @@ let unit_vars_to_unit (def : fun_decl) : fun_decl =
     function calls, and when translating end abstractions. Here, we can do
     something simpler, in one micro-pass.
  *)
-let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
+let eliminate_box_functions (ctx : trans_ctx) (def : fun_decl) : fun_decl =
   (* The map visitor *)
   let obj =
     object
@@ -1522,30 +1522,42 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
       method! visit_texpression env e =
         match opt_destruct_function_call e with
         | Some (fun_id, _tys, args) -> (
+            (* Below, when dealing with the arguments: we consider the very
+             * general case, where functions could be boxed (meaning we
+             * could have: [box_new f x])
+             * *)
             match fun_id with
             | Fun (FromLlbc (FunId (Assumed aid), _lp_id, rg_id)) -> (
-                (* Below, when dealing with the arguments: we consider the very
-                 * general case, where functions could be boxed (meaning we
-                 * could have: [box_new f x])
-                 * *)
                 match (aid, rg_id) with
                 | BoxNew, _ ->
                     assert (rg_id = None);
                     let arg, args = Collections.List.pop args in
                     mk_apps arg args
-                | BoxDeref, None ->
+                | BoxFree, _ ->
+                    assert (args = []);
+                    mk_unit_rvalue
+                | ( ( SliceIndexShared | SliceIndexMut | ArrayIndexShared
+                    | ArrayIndexMut | ArrayToSliceShared | ArrayToSliceMut
+                    | ArrayRepeat | SliceLen ),
+                    _ ) ->
+                    super#visit_texpression env e)
+            | Fun (FromLlbc (FunId (Regular fid), _lp_id, rg_id)) -> (
+                (* Lookup the function name *)
+                let def = FunDeclId.Map.find fid ctx.fun_ctx.fun_decls in
+                match (Names.name_to_string def.name, rg_id) with
+                | "alloc::box::Boxed::deref", None ->
                     (* [Box::deref] forward is the identity *)
                     let arg, args = Collections.List.pop args in
                     mk_apps arg args
-                | BoxDeref, Some _ ->
+                | "alloc::box::Boxed::deref", Some _ ->
                     (* [Box::deref] backward is [()] (doesn't give back anything) *)
                     assert (args = []);
                     mk_unit_rvalue
-                | BoxDerefMut, None ->
+                | "alloc::box::Boxed::deref_mut", None ->
                     (* [Box::deref_mut] forward is the identity *)
                     let arg, args = Collections.List.pop args in
                     mk_apps arg args
-                | BoxDerefMut, Some _ ->
+                | "alloc::box::Boxed::deref_mut", Some _ ->
                     (* [Box::deref_mut] back is almost the identity:
                      * let box_deref_mut (x_init : t) (x_back : t) : t = x_back
                      * *)
@@ -1555,17 +1567,7 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
                       | _ -> raise (Failure "Unreachable")
                     in
                     mk_apps arg args
-                | BoxFree, _ ->
-                    assert (args = []);
-                    mk_unit_rvalue
-                | ( ( Replace | VecNew | VecPush | VecInsert | VecLen | VecIndex
-                    | VecIndexMut | ArraySubsliceShared | ArraySubsliceMut
-                    | SliceIndexShared | SliceIndexMut | SliceSubsliceShared
-                    | SliceSubsliceMut | ArrayIndexShared | ArrayIndexMut
-                    | ArrayToSliceShared | ArrayToSliceMut | ArrayRepeat
-                    | SliceLen ),
-                    _ ) ->
-                    super#visit_texpression env e)
+                | _ -> super#visit_texpression env e)
             | _ -> super#visit_texpression env e)
         | _ -> super#visit_texpression env e
     end
diff --git a/compiler/PureTypeCheck.ml b/compiler/PureTypeCheck.ml
index b80ff72f..d31f0cf9 100644
--- a/compiler/PureTypeCheck.ml
+++ b/compiler/PureTypeCheck.ml
@@ -46,18 +46,7 @@ let get_adt_field_types (type_decls : type_decl TypeDeclId.Map.t)
           if variant_id = fuel_zero_id then []
           else if variant_id = fuel_succ_id then [ mk_fuel_ty ]
           else raise (Failure "Unreachable: improper variant id for fuel type")
-      | Option ->
-          let ty = Collections.List.to_cons_nil generics.types in
-          let variant_id = Option.get variant_id in
-          if variant_id = option_some_id then [ ty ]
-          else if variant_id = option_none_id then []
-          else
-            raise (Failure "Unreachable: improper variant id for option type")
-      | Range ->
-          let ty = Collections.List.to_cons_nil generics.types in
-          assert (variant_id = None);
-          [ ty; ty ]
-      | Vec | Array | Slice | Str ->
+      | Array | Slice | Str ->
           (* Array: when not symbolic values (for instance, because of aggregates),
              the array expressions are introduced as struct updates *)
           raise (Failure "Attempting to access the fields of an opaque type"))
diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml
index b1680282..6d9b9e15 100644
--- a/compiler/Substitute.ml
+++ b/compiler/Substitute.ml
@@ -305,19 +305,7 @@ let ctx_adt_value_get_instantiated_field_rtypes (ctx : C.eval_ctx)
       generics.types
   | T.Assumed aty -> (
       match aty with
-      | T.Box | T.Vec ->
-          assert (generics.regions = []);
-          assert (List.length generics.types = 1);
-          assert (generics.const_generics = []);
-          generics.types
-      | T.Option ->
-          assert (generics.regions = []);
-          assert (List.length generics.types = 1);
-          assert (generics.const_generics = []);
-          if adt.V.variant_id = Some T.option_some_id then generics.types
-          else if adt.V.variant_id = Some T.option_none_id then []
-          else raise (Failure "Unreachable")
-      | T.Range ->
+      | T.Box ->
           assert (generics.regions = []);
           assert (List.length generics.types = 1);
           assert (generics.const_generics = []);
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 54221cb1..9c698b51 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -405,8 +405,6 @@ let rec translate_sty (ty : T.sty) : ty =
           mk_simpl_tuple_ty generics.types
       | T.Assumed aty -> (
           match aty with
-          | T.Vec -> Adt (Assumed Vec, generics)
-          | T.Option -> Adt (Assumed Option, generics)
           | T.Box -> (
               (* Eliminate the boxes *)
               match generics.types with
@@ -418,8 +416,7 @@ let rec translate_sty (ty : T.sty) : ty =
               )
           | T.Array -> Adt (Assumed Array, generics)
           | T.Slice -> Adt (Assumed Slice, generics)
-          | T.Str -> Adt (Assumed Str, generics)
-          | T.Range -> Adt (Assumed Range, generics)))
+          | T.Str -> Adt (Assumed Str, generics)))
   | TypeVar vid -> TypeVar vid
   | Literal ty -> Literal ty
   | Never -> raise (Failure "Unreachable")
@@ -510,12 +507,9 @@ let translate_type_id (id : T.type_id) : type_id =
   | T.Assumed aty ->
       let aty =
         match aty with
-        | T.Vec -> Vec
-        | T.Option -> Option
         | T.Array -> Array
         | T.Slice -> Slice
         | T.Str -> Str
-        | T.Range -> Range
         | T.Box ->
             (* Boxes have to be eliminated: this type id shouldn't
                be translated *)
@@ -534,8 +528,7 @@ let rec translate_fwd_ty (type_infos : TA.type_infos) (ty : 'r T.ty) : ty =
       let t_generics = translate_fwd_generic_args type_infos generics in
       (* Eliminate boxes and simplify tuples *)
       match type_id with
-      | AdtId _
-      | T.Assumed (T.Vec | T.Option | T.Array | T.Slice | T.Str | T.Range) ->
+      | AdtId _ | T.Assumed (T.Array | T.Slice | T.Str) ->
           (* No general parametricity for now *)
           assert (
             not
@@ -610,8 +603,7 @@ let rec translate_back_ty (type_infos : TA.type_infos)
   match ty with
   | T.Adt (type_id, generics) -> (
       match type_id with
-      | T.AdtId _
-      | Assumed (T.Vec | T.Option | T.Array | T.Slice | T.Str | T.Range) ->
+      | T.AdtId _ | Assumed (T.Array | T.Slice | T.Str) ->
           (* Don't accept ADTs (which are not tuples) with borrows for now *)
           assert (not (TypesUtils.ty_has_borrows type_infos ty));
           let type_id = translate_type_id type_id in
@@ -815,7 +807,7 @@ let get_fun_effect_info (fun_infos : FA.fun_info A.FunDeclId.Map.t)
   | FunId (Assumed aid) ->
       assert (lid = None);
       {
-        can_fail = Assumed.assumed_can_fail aid;
+        can_fail = Assumed.assumed_fun_can_fail aid;
         stateful_group = false;
         stateful = false;
         can_diverge = false;
@@ -1221,9 +1213,7 @@ let rec typed_avalue_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx)
         (* For now, only tuples can contain borrows *)
         let adt_id, _ = TypesUtils.ty_as_adt av.ty in
         match adt_id with
-        | T.AdtId _
-        | T.Assumed
-            (T.Box | T.Vec | T.Option | T.Array | T.Slice | T.Str | T.Range) ->
+        | T.AdtId _ | T.Assumed (T.Box | T.Array | T.Slice | T.Str) ->
             assert (field_values = []);
             None
         | T.Tuple ->
@@ -1368,9 +1358,7 @@ let rec typed_avalue_to_given_back (mp : mplace option) (av : V.typed_avalue)
          * vector value upon visiting the "abstraction borrow" node *)
         let adt_id, _ = TypesUtils.ty_as_adt av.ty in
         match adt_id with
-        | T.AdtId _
-        | T.Assumed
-            (T.Box | T.Vec | T.Option | T.Array | T.Slice | T.Str | T.Range) ->
+        | T.AdtId _ | T.Assumed (T.Box | T.Array | T.Slice | T.Str) ->
             assert (field_values = []);
             (ctx, None)
         | T.Tuple ->
@@ -2441,17 +2429,12 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value)
         (mk_typed_pattern_from_var var None)
         (mk_opt_mplace_texpression scrutinee_mplace scrutinee)
         branch
-  | T.Assumed (T.Vec | T.Array | T.Slice | T.Str) ->
+  | T.Assumed (T.Array | T.Slice | T.Str) ->
       (* We can't expand those values: we can access the fields only
        * through the functions provided by the API (note that we don't
        * know how to expand values like vectors or arrays, because they have a variable number
        * of fields!) *)
       raise (Failure "Attempt to expand a non-expandable value")
-  | T.Assumed Range -> raise (Failure "Unimplemented")
-  | T.Assumed T.Option ->
-      (* We shouldn't get there in the "one-branch" case: options have
-       * two variants *)
-      raise (Failure "Unreachable")
 
 and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option)
     (sv : V.symbolic_value) (v : S.value_aggregate) (e : S.expression)
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 8e01c869..15297770 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -297,9 +297,11 @@ let translate_crate_to_pure (crate : A.crate) :
   (* Translate all the function *signatures* *)
   let assumed_sigs =
     List.map
-      (fun (id, sg, _, _) ->
-        (E.Assumed id, List.map (fun _ -> None) (sg : A.fun_sig).inputs, sg))
-      Assumed.assumed_infos
+      (fun (info : Assumed.assumed_fun_info) ->
+        ( E.Assumed info.fun_id,
+          List.map (fun _ -> None) info.fun_sig.inputs,
+          info.fun_sig ))
+      Assumed.assumed_fun_infos
   in
   let local_sigs =
     List.map
@@ -425,11 +427,15 @@ let export_type (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
         (true, kind)
   in
   (* Extract, if the config instructs to do so (depending on whether the type
-   * is opaque or not) *)
-  if
+     is opaque or not). Remark: we don't check if the definitions are builtin
+     here but in the function [export_types_group]: the reason is that if one
+     definition in the group is builtin, then we must check that all the
+     definitions are marked builtin *)
+  let extract =
     (is_opaque && config.extract_opaque)
     || ((not is_opaque) && config.extract_transparent)
-  then (
+  in
+  if extract then (
     if extract_decl then
       Extract.extract_type_decl ctx fmt type_decl_group kind def;
     if extract_extra_info then
@@ -464,41 +470,58 @@ let export_types_group (fmt : Format.formatter) (config : gen_config)
     List.map (fun id -> Pure.TypeDeclId.Map.find id ctx.trans_types) ids
   in
 
-  (* Extract the type declarations.
-
-     Because some declaration groups are delimited, we wrap the declarations
-     between [{start,end}_type_decl_group].
+  (* Check if the definition are builtin - if yes they must be ignored.
+     Note that if one definition in the group is builtin, then all the
+     definitions must be builtin *)
+  let builtin =
+    let open ExtractBuiltin in
+    let types_map = builtin_types_map () in
+    List.map
+      (fun (def : Pure.type_decl) ->
+        let sname = name_to_simple_name def.name in
+        SimpleNameMap.find_opt sname types_map <> None)
+      defs
+  in
 
-     Ex.:
-     ====
-     When targeting HOL4, the calls to [{start,end}_type_decl_group] would generate
-     the [Datatype] and [End] delimiters in the snippet of code below:
+  if List.exists (fun b -> b) builtin then
+    (* Sanity check *)
+    assert (List.for_all (fun b -> b) builtin)
+  else (
+    (* Extract the type declarations.
+
+       Because some declaration groups are delimited, we wrap the declarations
+       between [{start,end}_type_decl_group].
+
+       Ex.:
+       ====
+       When targeting HOL4, the calls to [{start,end}_type_decl_group] would generate
+       the [Datatype] and [End] delimiters in the snippet of code below:
+
+       {[
+         Datatype:
+           tree =
+             TLeaf 'a
+           | TNode node ;
+
+           node =
+             Node (tree list)
+         End
+       ]}
+    *)
+    Extract.start_type_decl_group ctx fmt is_rec defs;
+    List.iteri
+      (fun i def ->
+        let kind = kind_from_index i in
+        export_type_decl kind def)
+      defs;
+    Extract.end_type_decl_group fmt is_rec defs;
 
-     {[
-       Datatype:
-         tree =
-           TLeaf 'a
-         | TNode node ;
-
-         node =
-           Node (tree list)
-       End
-     ]}
-  *)
-  Extract.start_type_decl_group ctx fmt is_rec defs;
-  List.iteri
-    (fun i def ->
-      let kind = kind_from_index i in
-      export_type_decl kind def)
-    defs;
-  Extract.end_type_decl_group fmt is_rec defs;
-
-  (* Export the extra information (ex.: [Arguments] instructions in Coq) *)
-  List.iteri
-    (fun i def ->
-      let kind = kind_from_index i in
-      export_type_extra_info kind def)
-    defs
+    (* Export the extra information (ex.: [Arguments] instructions in Coq) *)
+    List.iteri
+      (fun i def ->
+        let kind = kind_from_index i in
+        export_type_extra_info kind def)
+      defs)
 
 (** Export a global declaration.
 
@@ -520,12 +543,12 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
     && (((not is_opaque) && config.extract_transparent)
        || (is_opaque && config.extract_opaque))
   in
-  (* Check if it is an assumed global - if yes, we ignore it because we
+  (* Check if it is a builtin global - if yes, we ignore it because we
      map the definition to one in the standard library *)
-  let open ExtractAssumed in
+  let open ExtractBuiltin in
   let sname = name_to_simple_name global.name in
   let extract =
-    extract && SimpleNameMap.find_opt sname assumed_globals_map = None
+    extract && SimpleNameMap.find_opt sname builtin_globals_map = None
   in
   if extract then
     (* We don't wrap global declaration groups between calls to functions
diff --git a/compiler/TypesAnalysis.ml b/compiler/TypesAnalysis.ml
index 4a187893..16f8c5f9 100644
--- a/compiler/TypesAnalysis.ml
+++ b/compiler/TypesAnalysis.ml
@@ -168,9 +168,7 @@ let analyze_full_ty (r_is_static : 'r -> bool) (updated : bool ref)
         in
         (* Continue exploring *)
         analyze expl_info ty_info rty
-    | Adt
-        ( (Tuple | Assumed (Box | Vec | Option | Slice | Array | Str | Range)),
-          generics ) ->
+    | Adt ((Tuple | Assumed (Box | Slice | Array | Str)), generics) ->
         (* Nothing to update: just explore the type parameters *)
         List.fold_left
           (fun ty_info ty -> analyze expl_info ty_info ty)
diff --git a/compiler/dune b/compiler/dune
index 2f5a0a44..4ec46b70 100644
--- a/compiler/dune
+++ b/compiler/dune
@@ -22,8 +22,8 @@
   Expressions
   ExpressionsUtils
   Extract
-  ExtractAssumed
   ExtractBase
+  ExtractBuiltin
   FunsAnalysis
   Identifiers
   InterpreterBorrowsCore