diff --git a/Common/CExtraction.v b/Common/CExtraction.v
index 2f295591..d9c31c71 100644
--- a/Common/CExtraction.v
+++ b/Common/CExtraction.v
@@ -44,7 +44,7 @@ From Stdlib Require Import Zeuclid.
 From Stdlib Require Import Extraction.
 
 Require Import Options.
-Require Import Common HVec Exec.
+Require Import Common Effects HVec Exec.
 
 
 (** * Base defaults *)
@@ -52,6 +52,14 @@ Require Import Common HVec Exec.
 From Stdlib Require Import ExtrOcamlBasic.
 
 
+Extraction Inline fmap.
+Extraction Inline mbind.
+Extraction Inline mcall.
+Extraction Inline mchoose.
+Extraction Inline lookup_total.
+Extraction Inline mchoosel.
+Extraction Inline mret.
+
 (** * Bools *)
 
 Extract Inlined Constant Decision => "bool".
@@ -328,7 +336,9 @@ Extract Inlined Constant HexString.of_Z => "Support.hex_str_of_Z".
 
 (** * Lists *)
 
-Extract Inlined Constant map => "Stdlib.List.map".
+Extract Inlined Constant map => "Support.list_map".
+Extract Inlined Constant list_fmap => "Support.list_map".
+(* Extract Inlined Constant map => "Stdlib.List.map". *)
 Extract Inlined Constant length => "Support.lengthZ".
 
 Extraction Blacklist List.
@@ -358,7 +368,7 @@ Extract Inductive vec => list [ "[]" "( :: )" ].
 Extraction Implicit vnil [A].
 Extraction Implicit vcons [A n].
 Extraction Implicit vmap [A B n].
-Extract Inlined Constant vmap => "List.map".
+Extract Inlined Constant vmap => "Support.list_map".
 Extract Inlined Constant list_to_vec  => "(fun x -> x)".
 
 Extraction Implicit Vector.last [A n].
diff --git a/Extraction/support.ml b/Extraction/support.ml
index 49361099..3fe98c6c 100644
--- a/Extraction/support.ml
+++ b/Extraction/support.ml
@@ -91,3 +91,13 @@ let bv_extract o l z =
   else
     let o = Z.to_int o in
     Z.extract z o l
+
+let[@tail_mod_cons] rec list_map f = function
+  | [] -> []
+  | [a1] ->
+      let r1 = f a1 in
+      [r1]
+  | a1 :: a2 :: l ->
+      let r1 = f a1 in
+      let r2 = f a2 in
+      r1 :: r2 :: list_map f l