diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 46b59c94de64..c2b470bdd278 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -40,8 +40,8 @@ variables:
   # The $hash is the first 10 characters of the md5 of the Dockerfile. e.g.
   # echo $(md5sum dev/ci/docker/old_ubuntu_lts/Dockerfile | head -c 10)
   # echo $(md5sum dev/ci/docker/edge_ubuntu/Dockerfile | head -c 10)
-  BASE_CACHEKEY: "old_ubuntu_lts-V2026-06-10-d4125f9d9e"
-  EDGE_CACHEKEY: "edge_ubuntu-V2026-06-10-0c389ac2f4"
+  BASE_CACHEKEY: "old_ubuntu_lts-V2026-06-17-3f4ccef838"
+  EDGE_CACHEKEY: "edge_ubuntu-V2026-06-17-d451657c63"
   BASE_IMAGE: "$CI_REGISTRY_IMAGE:$BASE_CACHEKEY"
   EDGE_IMAGE: "$CI_REGISTRY_IMAGE:$EDGE_CACHEKEY"
 
diff --git a/config/dune b/config/dune
index fb11fbee2401..ab124197513c 100644
--- a/config/dune
+++ b/config/dune
@@ -28,4 +28,4 @@
    %{project_root}/dev/header.c
    ; Needed to generate include lists for coq_makefile
    plugin_list)
- (action (chdir %{project_root} (run %{project_root}/tools/configure/configure.exe -quiet -relocatable))))
+ (action (chdir %{project_root} (run %{project_root}/tools/configure/configure.exe -quiet -relocatable -native-compiler yes))))
diff --git a/dev/ci/docker/edge_ubuntu/Dockerfile b/dev/ci/docker/edge_ubuntu/Dockerfile
index 44797ac4e68d..5d56fcf98470 100644
--- a/dev/ci/docker/edge_ubuntu/Dockerfile
+++ b/dev/ci/docker/edge_ubuntu/Dockerfile
@@ -53,7 +53,7 @@ RUN mkdir -p ~/.config/dune && printf '(lang dune 2.1)\n(jobs %s)\n' $NJOBS > ~/
 
 # Edge opam is the set of edge packages required by Coq
 ENV COMPILER="4.14.2" \
-    BASE_OPAM="zarith.1.14 ounit2.2.2.7 camlzip.1.14" \
+    BASE_OPAM="zarith.1.14 ounit2.2.2.7 camlzip.1.14 ocaml-compiler-libs" \
     CI_OPAM="ocamlgraph.2.0.0 cppo.1.8.0" \
     BASE_OPAM_EDGE="dune.3.23.1 dune-build-info.3.23.1 dune-release.2.2.1 ocamlfind.1.9.8 odoc.3.2.1" \
     CI_OPAM_EDGE="memprof-limits.0.3.0 elpi.3.7.1 ppx_import.1.12.0 cmdliner.2.1.1 sexplib.v0.16.0 ppx_sexp_conv.v0.16.0 ppx_hash.v0.16.0 ppx_compare.v0.16.0 ppx_deriving_yojson.3.9.1 yojson.2.2.2 uri.4.4.0 ppx_yojson_conv.v0.16.0 ppx_inline_test.v0.16.1 ppx_assert.v0.16.0 ppx_optcomp.v0.16.0 lsp.1.26.0 sel.0.8.0" \
@@ -68,6 +68,7 @@ RUN opam init -a --disable-sandboxing --bare && eval $(opam env) && \
     opam repo add archive git+https://github.com/ocaml/opam-repository-archive && \
     opam update && \
     opam install $BASE_OPAM $BASE_OPAM_EDGE $COQIDE_OPAM_EDGE $CI_OPAM $CI_OPAM_EDGE && \
+    opam pin add git+https://github.com/IBBXEF/malfunction#recusive_types && \
     opam clean -a -c
 
 # set the locale for the benefit of Python
diff --git a/dev/ci/docker/old_ubuntu_lts/Dockerfile b/dev/ci/docker/old_ubuntu_lts/Dockerfile
index cf915236ea7e..82369a0b5ac8 100644
--- a/dev/ci/docker/old_ubuntu_lts/Dockerfile
+++ b/dev/ci/docker/old_ubuntu_lts/Dockerfile
@@ -50,7 +50,7 @@ RUN mkdir -p ~/.config/dune && printf '(lang dune 2.1)\n(jobs %s)\n' $NJOBS > ~/
 ENV COMPILER="4.14.0"
 
 # Common OPAM packages
-ENV BASE_OPAM="zarith.1.11 ounit2.2.2.6 yojson.1.7.0 camlzip.1.10" \
+ENV BASE_OPAM="zarith.1.11 ounit2.2.2.6 yojson.1.7.0 camlzip.1.10 ocaml-compiler-libs" \
     CI_OPAM="ocamlgraph.2.0.0 cppo.1.6.9" \
     BASE_ONLY_OPAM="dune.3.21.1 stdlib-shims.0.1.0 ocamlfind.1.9.1 odoc.3.2.1 num.1.4"
 
@@ -65,6 +65,7 @@ RUN opam init -a --disable-sandboxing --compiler="$COMPILER" default https://opa
     opam repo add archive git+https://github.com/ocaml/opam-repository-archive && \
     opam update && \
     opam install $BASE_OPAM $COQIDE_OPAM $CI_OPAM $BASE_ONLY_OPAM && \
+    opam pin add git+https://github.com/IBBXEF/malfunction#recusive_types && \
     opam clean -a -c && \
     find ~ '(' -name '*.cmt' -o -name '*.cmti' ')' -delete
 
@@ -76,6 +77,7 @@ RUN opam switch create "${COMPILER}+32bit" \
     opam update && \
     i386 env CC='gcc -m32' opam install zarith.1.11 && \
     opam install $BASE_OPAM && \
+    opam pin add git+https://github.com/IBBXEF/malfunction#recusive_types && \
     opam clean -a -c && \
     find ~ '(' -name '*.cmt' -o -name '*.cmti' ')' -delete
 
diff --git a/kernel/float64.mli b/kernel/float64.mli
index 0d2fcaaac7e7..b264d68a0a0d 100644
--- a/kernel/float64.mli
+++ b/kernel/float64.mli
@@ -34,6 +34,8 @@ val to_string : t -> string
 
 val compile : t -> string
 
+val compile_mlf : t -> string
+
 val of_float : float -> t
 
 (** All NaNs are normalized to [Stdlib.nan].
diff --git a/kernel/float64_common.ml b/kernel/float64_common.ml
index a6ac22bf9d94..8769361c9146 100644
--- a/kernel/float64_common.ml
+++ b/kernel/float64_common.ml
@@ -41,6 +41,15 @@ let of_string = float_of_string
 let compile f =
   Printf.sprintf "Float64.of_float (%s)" (to_hex_string f)
 
+  (* Compiles a float to malfunction code *)
+let compile_mlf f = (* malfunction does not support writing -1.1, so we have to be careful *)
+  if Float.is_nan f then "(apply (global $Float64 $of_float) nan)"
+  else if Float.is_infinite f then begin
+    if f < 0. then Printf.sprintf "(apply (global $Float64 $of_float) neg_infinity)"
+    else Printf.sprintf "(apply (global $Float64 $of_float) infinity)"
+  end else if f < 0. then Printf.sprintf "(apply (global $Float64 $of_float) (neg.f64 %.17e))" (-. f) (* malfunction supports scientific notation *)
+  else Printf.sprintf "(apply (global $Float64 $of_float) %.17e)" f
+
 let of_float f = f
 
 let to_float f = if is_nan f then nan else f
diff --git a/kernel/float64_common.mli b/kernel/float64_common.mli
index 61c061af90b2..9f8d8d208d3a 100644
--- a/kernel/float64_common.mli
+++ b/kernel/float64_common.mli
@@ -34,6 +34,8 @@ val to_string : t -> string
 
 val compile : t -> string
 
+val compile_mlf : t -> string
+
 val of_float : float -> t
 
 (** All NaNs are normalized to [Stdlib.nan].
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 4d3abb6a5900..2b284ee914a8 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -275,7 +275,6 @@ type primitive =
   | MLand
   | MLnot
   | MLland
-  | MLmagic
   | MLsubst_instance_instance
   | MLsubst_instance_sort
   | MLparray_of_array
@@ -290,8 +289,10 @@ type primitive =
   | Get_proj
   | Get_symbols
   | Lazy
+  | Force
   | Coq_primitive of CPrimitives.t * bool (* check for accu *)
   | Mk_empty_instance
+  | Str_decode
 
 let eq_primitive p1 p2 =
   match p1, p2 with
@@ -317,7 +318,6 @@ let eq_primitive p1 p2 =
   | MLand, MLand
   | MLnot, MLnot
   | MLland, MLland
-  | MLmagic, MLmagic
   | MLsubst_instance_instance, MLsubst_instance_instance
   | MLsubst_instance_sort, MLsubst_instance_sort
   | MLparray_of_array, MLparray_of_array
@@ -332,7 +332,9 @@ let eq_primitive p1 p2 =
   | Get_proj, Get_proj
   | Get_symbols, Get_symbols
   | Lazy, Lazy
+  | Force, Force
   | Mk_empty_instance, Mk_empty_instance
+  | Str_decode, Str_decode
     -> true
 
   | Mk_fix (rp1, i1), Mk_fix (rp2, i2) -> Int.equal i1 i2 && eq_rec_pos rp1 rp2
@@ -368,7 +370,6 @@ let eq_primitive p1 p2 =
     | MLand
     | MLnot
     | MLland
-    | MLmagic
     | MLsubst_instance_instance
     | MLsubst_instance_sort
     | MLparray_of_array
@@ -383,8 +384,10 @@ let eq_primitive p1 p2 =
     | Get_proj
     | Get_symbols
     | Lazy
+    | Force
     | Coq_primitive _
-    | Mk_empty_instance), _
+    | Mk_empty_instance
+    | Str_decode), _
     -> false
 
 let primitive_hash = function
@@ -412,30 +415,31 @@ let primitive_hash = function
   | Mk_evar -> 18
   | MLand -> 19
   | MLland -> 20
-  | MLmagic -> 21
-  | Coq_primitive (prim, b) -> combinesmall 22 (combine (CPrimitives.hash prim) (Hashtbl.hash b))
-  | Mk_proj -> 23
-  | MLsubst_instance_instance -> 24
-  | MLsubst_instance_sort -> 25
-  | Mk_float -> 26
-  | Is_float -> 27
-  | Is_string -> 28
-  | Is_parray -> 29
-  | MLnot -> 30
-  | MLparray_of_array -> 31
-  | Get_value -> 32
-  | Get_sort -> 33
-  | Get_name -> 34
-  | Get_const -> 35
-  | Get_match -> 36
-  | Get_ind -> 37
-  | Get_evar -> 38
-  | Get_instance -> 39
-  | Get_proj -> 40
-  | Get_symbols -> 41
-  | Lazy -> 42
+  | Coq_primitive (prim, b) -> combinesmall 21 (combine (CPrimitives.hash prim) (Hashtbl.hash b))
+  | Mk_proj -> 22
+  | MLsubst_instance_instance -> 23
+  | MLsubst_instance_sort -> 24
+  | Mk_float -> 25
+  | Is_float -> 26
+  | Is_string -> 27
+  | Is_parray -> 28
+  | MLnot -> 29
+  | MLparray_of_array -> 30
+  | Get_value -> 31
+  | Get_sort -> 32
+  | Get_name -> 33
+  | Get_const -> 34
+  | Get_match -> 35
+  | Get_ind -> 36
+  | Get_evar -> 37
+  | Get_instance -> 38
+  | Get_proj -> 39
+  | Get_symbols -> 40
+  | Lazy -> 41
+  | Force -> 42
   | Mk_empty_instance -> 43
   | Mk_string -> 44
+  | Str_decode -> 45
 
 type mllambda =
   | MLlocal        of lname
@@ -446,8 +450,10 @@ type mllambda =
   | MLlet          of lname * mllambda * mllambda
   | MLapp          of mllambda * mllambda array
   | MLif           of mllambda * mllambda * mllambda
-  | MLmatch        of annot_sw * mllambda * mllambda * mllam_branches
+  | MLmatch        of mllambda * mllambda * mllam_branches
                               (* argument, prefix, accu branch, branches *)
+  | MLmatch_noaccu        of mllambda * mllam_branches
+                              (* argument, prefix, branches *)
   | MLconstruct    of string * inductive * int * mllambda array
                    (* prefix, inductive name, tag, arguments *)
   | MLint          of int
@@ -513,11 +519,13 @@ let rec eq_mllambda gn1 gn2 n env1 env2 t1 t2 =
       eq_mllambda gn1 gn2 n env1 env2 cond1 cond2 &&
       eq_mllambda gn1 gn2 n env1 env2 br1 br2 &&
       eq_mllambda gn1 gn2 n env1 env2 br'1 br'2
-  | MLmatch (annot1, c1, accu1, br1), MLmatch (annot2, c2, accu2, br2) ->
-      eq_annot_sw annot1 annot2 &&
+  | MLmatch (c1, accu1, br1), MLmatch (c2, accu2, br2) ->
       eq_mllambda gn1 gn2 n env1 env2 c1 c2 &&
       eq_mllambda gn1 gn2 n env1 env2 accu1 accu2 &&
       eq_mllam_branches gn1 gn2 n env1 env2 br1 br2
+  | MLmatch_noaccu (c1, br1), MLmatch_noaccu (c2, br2) ->
+      eq_mllambda gn1 gn2 n env1 env2 c1 c2 &&
+      eq_mllam_branches gn1 gn2 n env1 env2 br1 br2
   | MLconstruct (pf1, ind1, tag1, args1), MLconstruct (pf2, ind2, tag2, args2) ->
       String.equal pf1 pf2 &&
       Ind.UserOrd.equal ind1 ind2 &&
@@ -544,7 +552,7 @@ let rec eq_mllambda gn1 gn2 n env1 env2 t1 t2 =
     String.equal s1 s2 && Ind.UserOrd.equal ind1 ind2 &&
     eq_mllambda gn1 gn2 n env1 env2 ml1 ml2
   | (MLlocal _ | MLglobal _ | MLprimitive _ | MLlam _ | MLletrec _ | MLlet _ |
-    MLapp _ | MLif _ | MLmatch _ | MLconstruct _ | MLint _ | MLuint _ |
+    MLapp _ | MLif _ | MLmatch _ | MLmatch_noaccu _ | MLconstruct _ | MLint _ | MLuint _ |
     MLfloat _ | MLstring _ | MLsetref _ | MLsequence _ |
     MLarray _ | MLisaccu _), _ -> false
 
@@ -607,36 +615,38 @@ let rec hash_mllambda gn n env t =
       let hbr = hash_mllambda gn n env br in
       let hbr' = hash_mllambda gn n env br' in
       combinesmall 8 (combine3 hcond hbr hbr')
-  | MLmatch (annot, c, accu, br) ->
-      let hannot = hash_annot_sw annot in
+  | MLmatch (c, accu, br) ->
       let hc = hash_mllambda gn n env c in
       let haccu = hash_mllambda gn n env accu in
-      combinesmall 9 (hash_mllam_branches gn n env (combine3 hannot hc haccu) br)
+      combinesmall 9 (hash_mllam_branches gn n env (combine hc haccu) br)
+  | MLmatch_noaccu (c, br) ->
+      let hc = hash_mllambda gn n env c in
+      combinesmall 10 (hash_mllam_branches gn n env hc br)
   | MLconstruct (pf, ind, tag, args) ->
       let hpf = String.hash pf in
       let hcs = Ind.UserOrd.hash ind in
       let htag = Int.hash tag in
-      combinesmall 10 (hash_mllambda_array gn n env (combine3 hpf hcs htag) args)
+      combinesmall 11 (hash_mllambda_array gn n env (combine3 hpf hcs htag) args)
   | MLint i ->
-      combinesmall 11 i
+      combinesmall 12 i
   | MLuint i ->
-      combinesmall 12 (Uint63.hash i)
+      combinesmall 13 (Uint63.hash i)
   | MLsetref (id, ml) ->
       let hid = String.hash id in
       let hml = hash_mllambda gn n env ml in
-      combinesmall 13 (combine hid hml)
+      combinesmall 14 (combine hid hml)
   | MLsequence (ml, ml') ->
       let hml = hash_mllambda gn n env ml in
       let hml' = hash_mllambda gn n env ml' in
-      combinesmall 14 (combine hml hml')
+      combinesmall 15 (combine hml hml')
   | MLarray arr ->
-      combinesmall 15 (hash_mllambda_array gn n env 1 arr)
+      combinesmall 16 (hash_mllambda_array gn n env 1 arr)
   | MLisaccu (s, ind, c) ->
-      combinesmall 16 (combine (String.hash s) (combine (Ind.UserOrd.hash ind) (hash_mllambda gn n env c)))
+      combinesmall 17 (combine (String.hash s) (combine (Ind.UserOrd.hash ind) (hash_mllambda gn n env c)))
   | MLfloat f ->
-      combinesmall 17 (Float64.hash f)
+      combinesmall 18 (Float64.hash f)
   | MLstring s ->
-      combinesmall 18 (Pstring.hash s)
+      combinesmall 19 (Pstring.hash s)
 
 and hash_mllambda_letrec gn n env init defs =
   let hash_def (_,args,ml) =
@@ -691,7 +701,7 @@ let fv_lam l =
         Array.fold_right fv_arg args (aux f bind fv)
     | MLif(t,b1,b2) ->
         aux t bind (aux b1 bind (aux b2 bind fv))
-    | MLmatch(_,a,p,bs) ->
+    | MLmatch(a,p,bs) ->
       let fv = aux a bind (aux p bind fv) in
       let fv_bs (cargs, body) fv =
         let bind =
@@ -706,6 +716,21 @@ let fv_lam l =
             cargs bind in
         aux body bind fv in
       Array.fold_right fv_bs bs fv
+    | MLmatch_noaccu(p,bs) ->
+      let fv = aux p bind fv in
+      let fv_bs (cargs, body) fv =
+        let bind =
+          List.fold_right (fun pat bind ->
+              match pat with
+              | ConstPattern _ -> bind
+              | NonConstPattern(_,args) ->
+                Array.fold_right
+                  (fun o bind -> match o with
+                     | Some l -> LNset.add l bind
+                     | _ -> bind) args bind)
+            cargs bind in
+        aux body bind fv in
+      Array.fold_right fv_bs bs fv
     (* argument, accu branch, branches *)
     | MLconstruct (_,_,_,p) ->
         Array.fold_right (fun a fv -> aux a bind fv) p fv
@@ -746,7 +771,7 @@ type global =
   | Gtblfixtype of gname * lname array * mllambda array
   | Glet of gname * mllambda
   | Gletcase of
-      gname * lname array * annot_sw * mllambda * mllambda * mllam_branches
+      gname * lname array * mllambda * mllambda * mllam_branches
   | Gopen of string
   | Gtype of inductive * (tag * int) array
     (* ind name, tag and arities of constructors *)
@@ -765,13 +790,13 @@ let eq_global g1 g2 =
       Array.for_all2 (eq_mllambda gn1 gn2 (Array.length lns1) env1 env2) mls1 mls2
   | Glet (gn1, def1), Glet (gn2, def2) ->
       eq_mllambda gn1 gn2 0 LNmap.empty LNmap.empty def1 def2
-  | Gletcase (gn1,lns1,annot1,c1,accu1,br1),
-      Gletcase (gn2,lns2,annot2,c2,accu2,br2) ->
+  | Gletcase (gn1,lns1,c1,accu1,br1),
+      Gletcase (gn2,lns2,c2,accu2,br2) ->
       Int.equal (Array.length lns1) (Array.length lns2) &&
       let env1 = push_lnames 0 LNmap.empty lns1 in
       let env2 = push_lnames 0 LNmap.empty lns2 in
-      let t1 = MLmatch (annot1,c1,accu1,br1) in
-      let t2 = MLmatch (annot2,c2,accu2,br2) in
+      let t1 = MLmatch (c1,accu1,br1) in
+      let t2 = MLmatch (c2,accu2,br2) in
       eq_mllambda gn1 gn2 (Array.length lns1) env1 env2 t1 t2
   | Gopen s1, Gopen s2 -> String.equal s1 s2
   | Gtype (ind1, arr1), Gtype (ind2, arr2) ->
@@ -802,10 +827,10 @@ let hash_global g =
       combinesmall 3 hmls
   | Glet (gn, def) ->
       combinesmall 4 (hash_mllambda gn 0 LNmap.empty def)
-  | Gletcase (gn,lns,annot,c,accu,br) ->
+  | Gletcase (gn,lns,c,accu,br) ->
       let nlns = Array.length lns in
       let env = push_lnames 0 LNmap.empty lns in
-      let t = MLmatch (annot,c,accu,br) in
+      let t = MLmatch (c,accu,br) in
       combinesmall 5 (combine nlns (hash_mllambda gn nlns env t))
   | Gopen s -> combinesmall 5 (String.hash s)
   | Gtype (ind, arr) ->
@@ -898,8 +923,8 @@ let push_global_norm cenv gn params body =
 let push_global_cofix cenv gn params self =
   push_global cenv gn (Gtblcofix (gn, params, self))
 
-let push_global_case cenv gn params annot a accu bs =
-  push_global cenv gn (Gletcase (gn, params, annot, a, accu, bs))
+let push_global_case cenv gn params a accu bs =
+  push_global cenv gn (Gletcase (gn, params, a, accu, bs))
 
 let push_symbol cenv x =
   try HashtblSymbol.find cenv.symb_tbl x
@@ -1071,7 +1096,7 @@ let fv_args env fvn fvr =
       args
     end
 
-let symbols_tbl_name = Ginternal "symbols_tbl"
+let symbols_tbl_name = Ginternal "$symbols_tbl"
 
 let get_value_code i =
   MLprimitive (Get_value,
@@ -1214,13 +1239,13 @@ let ml_of_instance env u =
       let u_code =
         if has_variable then
           (* if there are variables then [instance] guaranteed non-None *)
-          let univ = MLprimitive (MLmagic, [|MLlocal (Option.get instance)|]) in
+          let univ = MLlocal (Option.get instance) in
           MLprimitive (MLsubst_instance_instance, [|univ; u_code|])
         else u_code
       in
     u_code
     in
-    [|MLprimitive (MLmagic, [|u_code|])|]
+    [|u_code|]
 
 let ml_of_sort env s =
   let i = push_symbol env.env_cenv (SymbSort s) in
@@ -1229,7 +1254,7 @@ let ml_of_sort env s =
   | UGlobal | ULocal None -> s_code
   | ULocal (Some u) ->
     (* FIXME: use a dedicated cast function *)
-    let u = MLprimitive (MLmagic, [|MLlocal u|]) in
+    let u = MLlocal u in
     MLprimitive (MLsubst_instance_sort, [|u; s_code|])
   in
   MLprimitive (Mk_sort, [|s_code|])
@@ -1269,7 +1294,7 @@ let compile_prim env decl cond paux =
           List.fold_left
             (fun ml (_, c) -> app_prim MLland [| ml; cast_to_int c|])
             (MLint 0) ci in
-        app_prim MLmagic [|cond|] in
+        cond in
       let condo = match co with
         | [] -> MLint 0
         | (CPrimitives.PTE ty, c1) :: condo ->
@@ -1302,7 +1327,7 @@ let compile_prim env decl cond paux =
   else
     add_decl decl (compile_cond cond paux)
 
- let rec ml_of_lam env l t =
+let rec ml_of_lam env l t =
   match node t with
   | Lrel(id ,i) -> get_rel env id i
   | Lvar id -> get_var env id
@@ -1331,7 +1356,7 @@ let compile_prim env decl cond paux =
      let prefix = env.env_const_prefix c in
      let args = ml_of_instance env u in
      let ans = mkMLapp (MLglobal(Gconstant (prefix, c))) args in
-     if env.env_const_lazy c then MLapp (MLglobal (Ginternal "Lazy.force"), [|ans|])
+     if env.env_const_lazy c then MLprimitive (Force, [|ans|])
      else ans
   | Lproj (p, c) ->
     let ind = Projection.Repr.inductive p in
@@ -1394,7 +1419,7 @@ let compile_prim env decl cond paux =
 (*      let body = MLlam([|a_uid|], MLmatch(annot, la_uid, accu, bs)) in
       let case = generalize_fv env_c body in *)
       let cn = push_global_case env.env_cenv cn (Array.append (fv_params env_c) [|a_uid|])
-        annot la_uid accu (merge_branches br)
+        la_uid accu (merge_branches br)
       in
       (* Final result *)
       let arg = ml_of_lam env l a in
@@ -1525,18 +1550,18 @@ let compile_prim env decl cond paux =
         let unit = fresh_lname env.env_cenv Anonymous in
         let args = Array.map (fun id -> MLlocal id) t_params.(i) in
         let mk_let i lname cont =
-          MLlet (lname, MLprimitive (Array_get, [|MLglobal knot; MLint i|]), cont)
+          MLlet (lname, MLprimitive (Array_get, [|MLint i; MLglobal knot|]), cont) (* in malfunction, the index is first *)
         in
         let self = Array.map (fun id -> MLlocal id) lf in
         let body = mkMLapp (MLglobal g) (Array.concat [fv_args'; self; args]) in
-        let body = MLprimitive (MLmagic, [|MLlam ([|unit|], Array.fold_right_i mk_let lf body)|]) in
+        let body = MLlam ([|unit|], Array.fold_right_i mk_let lf body) in
         let typs = mk_type in
         let self = mk_norm in
         mkMLlam t_params.(i) (MLprimitive ((Mk_cofix i), [| typs; self; body; MLarray args |]))
       in
       (* Tie the knot *)
       let knot = push_global_cofix env.env_cenv knot fv_params (Array.mapi map t_norm_f) in
-      MLprimitive (Array_get, [|MLapp (MLglobal knot, fv_args); MLint start|])
+      MLprimitive (Array_get, [|MLint start; MLapp (MLglobal knot, fv_args)|]) (* in malfunction, the index is first *)
 
   | Lint tag -> MLprimitive (Mk_int, [|MLint tag|])
 
@@ -1602,9 +1627,12 @@ let subst s l =
       | MLlet(id,def,body) -> MLlet(id,aux def, aux body)
       | MLapp(f,args) -> MLapp(aux f, Array.map aux args)
       | MLif(t,b1,b2) -> MLif(aux t, aux b1, aux b2)
-      | MLmatch(annot,a,accu,bs) ->
+      | MLmatch(a,accu,bs) ->
+          let auxb (cargs,body) = (cargs,aux body) in
+          MLmatch(a,aux accu, Array.map auxb bs)
+      | MLmatch_noaccu(a,bs) ->
           let auxb (cargs,body) = (cargs,aux body) in
-          MLmatch(annot,a,aux accu, Array.map auxb bs)
+          MLmatch_noaccu(a, Array.map auxb bs)
       | MLconstruct(prefix,c,tag,args) -> MLconstruct(prefix,c,tag,Array.map aux args)
       | MLsetref(s,l1) -> MLsetref(s,aux l1)
       | MLsequence(l1,l2) -> MLsequence(aux l1, aux l2)
@@ -1652,13 +1680,13 @@ let all_lam n bs =
     | _ -> false in
   Array.for_all f bs
 
-let commutative_cut annot a accu bs args =
+let commutative_cut a accu bs args =
   let mkb (c,b) =
      match b with
      | MLlam(params, body) ->
          (c, Array.fold_left2 (fun body x v -> MLlet(x,v,body)) body params args)
      | _ -> assert false in
-  MLmatch(annot, a, mkMLapp accu args, Array.map mkb bs)
+  MLmatch( a, mkMLapp accu args, Array.map mkb bs)
 
 let optimize gdef l =
   let rec optimize s l =
@@ -1695,9 +1723,9 @@ let optimize gdef l =
         | _ ->
             let f = optimize s f in
             match f with
-            | MLmatch (annot,a,accu,bs) ->
+            | MLmatch (a,accu,bs) ->
               if all_lam (Array.length args) bs then
-                commutative_cut annot a accu bs args
+                commutative_cut a accu bs args
               else MLapp(f, args)
             | _ -> MLapp(f, args)
 
@@ -1709,13 +1737,16 @@ let optimize gdef l =
         let b1 = optimize s b1 in
         let b2 = optimize s b2 in
         begin match t, b2 with
-        | MLisaccu (_, _, l1), MLmatch(annot, l2, _, bs)
-            when eq_mllambda l1 l2 -> MLmatch(annot, l1, b1, bs)
+        | MLisaccu (_, _, l1), MLmatch(l2, _, bs)
+            when eq_mllambda l1 l2 -> MLmatch(l1, b1, bs)
         | _, _ -> MLif(t, b1, b2)
         end
-    | MLmatch(annot,a,accu,bs) ->
+    | MLmatch(a,accu,bs) ->
+        let opt_b (cargs,body) = (cargs,optimize s body) in
+        MLmatch(optimize s a, subst s accu, Array.map opt_b bs)
+    | MLmatch_noaccu(a,bs) ->
         let opt_b (cargs,body) = (cargs,optimize s body) in
-        MLmatch(annot, optimize s a, subst s accu, Array.map opt_b bs)
+        MLmatch_noaccu(optimize s a, Array.map opt_b bs)
     | MLconstruct(prefix,c,tag,args) ->
         MLconstruct(prefix,c,tag,Array.map (optimize s) args)
     | MLsetref(r,l) -> MLsetref(r, optimize s l)
@@ -1731,9 +1762,9 @@ let optimize_stk stk =
     | Glet (Gnorm (_,i), body) ->
         let (gnorm, gcase) = gdef in
         (Int.Map.add i (decompose_MLlam body) gnorm, gcase)
-    | Gletcase(Gcase (_,i), params, annot,a,accu,bs) ->
+    | Gletcase(Gcase (_,i), params,a,accu,bs) ->
         let (gnorm,gcase) = gdef in
-        (gnorm, Int.Map.add i (params,MLmatch(annot,a,accu,bs)) gcase)
+        (gnorm, Int.Map.add i (params,MLmatch(a,accu,bs)) gcase)
     | Gletcase _ -> assert false
     | _ -> gdef in
   let gdef = List.fold_left add_global empty_gdef stk in
@@ -1792,39 +1823,45 @@ let string_of_mind mind = string_of_kn (MutInd.user mind)
 let string_of_ind (mind,i) = string_of_kn (MutInd.user mind) ^ "_" ^ string_of_int i
 
 let string_of_gname g =
-  match g with
-  | Gind (prefix, (mind, i)) ->
-      Format.sprintf "%sindaccu_%s_%i" prefix (string_of_mind mind) i
-  | Gconstant (prefix, c) ->
-      Format.sprintf "%sconst_%s" prefix (string_of_con c)
-  | Gproj (prefix, (mind, n), i) ->
-      Format.sprintf "%sproj_%s_%i_%i" prefix (string_of_mind mind) n i
-  | Gcase (l,i) ->
-      Format.sprintf "case_%s_%i" (string_of_label_def l) i
-  | Gpred (l,i) ->
-      Format.sprintf "pred_%s_%i" (string_of_label_def l) i
-  | Gfixtype (l,i) ->
-      Format.sprintf "fixtype_%s_%i" (string_of_label_def l) i
-  | Gnorm (l,i) ->
-      Format.sprintf "norm_%s_%i" (string_of_label_def l) i
-  | Ginternal s -> Format.sprintf "%s" s
-  | Gnormtbl (l,i) ->
-      Format.sprintf "normtbl_%s_%i" (string_of_label_def l) i
-  | Grel i ->
-      Format.sprintf "rel_%i" i
-  | Gnamed id ->
-      Format.sprintf "named_%s" (string_of_id id)
+  let ret = match g with
+    | Gind (prefix, (mind, i)) ->
+        Format.sprintf "$%sindaccu_%s_%i" prefix (string_of_mind mind) i
+    | Gconstant (prefix, c) ->
+        Format.sprintf "$%sconst_%s" prefix (string_of_con c)
+    | Gproj (prefix, (mind, n), i) ->
+        Format.sprintf "$%sproj_%s_%i_%i" prefix (string_of_mind mind) n i
+    | Gcase (l,i) ->
+        Format.sprintf "$case_%s_%i" (string_of_label_def l) i
+    | Gpred (l,i) ->
+        Format.sprintf "$pred_%s_%i" (string_of_label_def l) i
+    | Gfixtype (l,i) ->
+        Format.sprintf "$fixtype_%s_%i" (string_of_label_def l) i
+    | Gnorm (l,i) ->
+        Format.sprintf "$norm_%s_%i" (string_of_label_def l) i
+    | Ginternal s -> Format.sprintf "%s" s
+    | Gnormtbl (l,i) ->
+        Format.sprintf "$normtbl_%s_%i" (string_of_label_def l) i
+    | Grel i ->
+        Format.sprintf "$rel_%i" i
+    | Gnamed id ->
+        Format.sprintf "$named_%s" (string_of_id id) in
+  if String.contains ret '.' then (* the global name comes from a module *)
+    let ret = String.split_on_char '.' ret in
+    let ret = String.concat " $" ret in 
+    Format.sprintf "(global %s)" ret
+  else ret
 
 let pp_gname fmt g =
   Format.fprintf fmt "%s" (string_of_gname g)
 
 let pp_lname fmt ln =
-  Format.fprintf fmt "x_%s_%i" (string_of_name ln.lname) ln.luid
+  Format.fprintf fmt "$x_%s_%i" (string_of_name ln.lname) ln.luid
 
 let pp_ldecls fmt ids =
   let len = Array.length ids in
+  if len = 0 then Format.fprintf fmt "$_" else (* argument list cannot be empty in malfunction *)
   for i = 0 to len - 1 do
-    Format.fprintf fmt " (%a : Nativevalues.t)" pp_lname ids.(i)
+    Format.fprintf fmt " %a" pp_lname ids.(i)
   done
 
 let string_of_construct prefix ~constant ind tag =
@@ -1834,278 +1871,298 @@ let string_of_construct prefix ~constant ind tag =
 let string_of_accu_construct prefix ind =
   Format.sprintf "%sAccu_%s" prefix (string_of_ind ind)
 
-let pp_int fmt i =
-  if i < 0 then Format.fprintf fmt "(%i)" i else Format.fprintf fmt "%i" i
-
 let pp_mllam fmt l =
 
   let rec pp_mllam fmt l =
     match l with
-    | MLlocal ln -> Format.fprintf fmt "@[%a@]" pp_lname ln
-    | MLglobal g -> Format.fprintf fmt "@[%a@]" pp_gname g
-    | MLprimitive (p, args) ->
-      Format.fprintf fmt "@[<2>%a@ %a@]" pp_primitive p (pp_args true) args
+    | MLint i when i >= 0 -> Format.fprintf fmt "%i" i
+    | MLint i -> Format.fprintf fmt "(neg %i)" (-i) (* i < 0 *)
+    | MLuint i -> Format.fprintf fmt "%s" (Uint63.compile_mlf i)
+    | MLfloat f -> Format.fprintf fmt "%s" (Float64.compile_mlf f)
+    | MLstring s -> Format.fprintf fmt "%s" (Pstring.compile_mlf s)
     | MLlam(ids,body) ->
-        Format.fprintf fmt "@[(fun%a ->@ %a)@]"
+        Format.fprintf fmt "@[<2>(lambda (%a) @ %a)@]"
           pp_ldecls ids pp_mllam body
-    | MLletrec(defs, body) ->
-        Format.fprintf fmt "@[(%a@ in@\n%a)@]" pp_letrec defs
-          pp_mllam body
+    | MLsequence(l1,l2) ->
+        Format.fprintf fmt "@[(seq (%a) (%a))@]" pp_mllam l1 pp_mllam l2
+    | MLprimitive (MLland, args) -> (* malfunction has a special operator for bitwise and *)
+      Format.fprintf fmt "(& %a)" pp_args args
+    | MLprimitive (MLnot, args) ->
+      Format.fprintf fmt "(== 0 %a)" pp_args args
+    | MLprimitive (Lazy, args) -> (* lazy values must be treated separately *)
+      Format.fprintf fmt "@[<2>(lazy%a)@]" pp_args args
+    | MLprimitive (Force, args) ->
+      Format.fprintf fmt "@[<2>(force%a)@]" pp_args args
+    | MLprimitive (Array_get, args) ->
+      Format.fprintf fmt "@[<2>(field%a)@]" pp_args args (* we compile arrays as classical blocks, so array_get is just a field access (we do not mutate arrays) *)
+    | MLprimitive (MLand, [|a; b|]) -> (* a and b are booleans *)
+      Format.fprintf fmt "(if %a %a 0)" pp_mllam a pp_mllam b
+    | MLprimitive (p, [||]) -> (* not a function and just a value *)
+      Format.fprintf fmt "%a" pp_primitive p
+    | MLprimitive (p, args) ->
+      Format.fprintf fmt "@[<2>(apply %a%a)@]" pp_primitive p pp_args args
+    | MLlocal ln -> Format.fprintf fmt "@[%a@]" pp_lname ln
+    | MLglobal g -> Format.fprintf fmt "@[%a@]" pp_gname g
+    | MLapp(f, [||]) -> (* not an application and instead simply a function *)
+        Format.fprintf fmt "%a" pp_mllam f
+    | MLapp(f, args) ->
+        Format.fprintf fmt "@[<2>(apply %a%a)@]" pp_mllam f pp_args args
     | MLlet(id,def,body) ->
-        Format.fprintf fmt "@[(@[let@ %a@ =@ %a@ in@]@\n%a)@]"
+        Format.fprintf fmt "@[(let@ (%a@ %a)@\n@[<2>%a@])@]"
           pp_lname id pp_mllam def pp_mllam body
-    | MLapp(f, args) ->
-        Format.fprintf fmt "@[<2>%a@ %a@]" pp_mllam f (pp_args true) args
     | MLif(t,l1,l2) ->
-        Format.fprintf fmt "@[(if %a then@\n  %a@\nelse@\n  %a)@]"
+        Format.fprintf fmt "@[(if %a@\n  %a@\n  %a)@]"
           pp_mllam t pp_mllam l1 pp_mllam l2
-    | MLmatch (annot, c, accu_br, br) ->
-      let ind = annot.asw_ind in
-      let prefix = annot.asw_prefix in
-      let accu = string_of_accu_construct prefix ind in
-      Format.fprintf fmt
-        "@[begin match Obj.magic (%a) with@\n| %s _ ->@\n  %a@\n%aend@]"
-        pp_mllam c accu pp_mllam accu_br (pp_branches prefix ind) br
-
-    | MLconstruct(prefix,ind,tag,args) ->
-        Format.fprintf fmt "@[<2>(Obj.magic@ @[<2>(%s%a)@] : Nativevalues.t)@]"
-          (string_of_construct prefix ~constant:false ind tag) pp_cargs args
-    | MLint i -> pp_int fmt i
-    | MLuint i -> Format.fprintf fmt "(%s)" (Uint63.compile i)
-    | MLfloat f -> Format.fprintf fmt "(%s)" (Float64.compile f)
-    | MLstring s -> Format.fprintf fmt "(%s)" (Pstring.compile s)
-    | MLsetref (s, body) ->
-        Format.fprintf fmt "@[%s@ :=@\n Some (%a)@]" s pp_mllam body
-    | MLsequence(l1,l2) ->
-        Format.fprintf fmt "@[%a;@\n%a@]" pp_mllam l1 pp_mllam l2
+    | MLletrec(defs, body) ->
+        Format.fprintf fmt "@[<2>(let (rec @[<2>%a@])@\n%a)@]" pp_letrec defs
+          pp_mllam body
     | MLarray arr ->
-      (* We need to ensure that the array does not use the flat representation
-          if ever the first argument is a float *)
-      let len = Array.length arr in
-      if Int.equal len 0 then begin
-        Format.fprintf fmt "@[(Obj.magic [||])@]"
-      end else if Int.equal len 1 then begin
-        (* We have to emulate a 1-uplet *)
-        Format.fprintf fmt "@[(Obj.magic (ref (%a)))@]" pp_mllam arr.(0)
-      end else begin
-        Format.fprintf fmt "@[(Obj.magic (";
-        for i = 0 to len - 2 do
-          Format.fprintf fmt "%a,@ " pp_mllam arr.(i)
-        done;
-        pp_mllam fmt arr.(len-1);
-        Format.fprintf fmt "))@]"
-      end;
-    | MLisaccu (prefix, ind, c) ->
-        let accu = string_of_accu_construct prefix ind in
+      Format.fprintf fmt "@[(block (tag 0)";
+      Array.iter (Format.fprintf fmt "@ %a" pp_mllam) arr;
+      Format.fprintf fmt ")@]"
+    | MLsetref (s, body) ->
+        Format.fprintf fmt "@[(store %s@ 0 @ @\n (apply (global $Option $some) %a ) )@]" s pp_mllam body
+    | MLmatch (c, accu_br, br) ->
+      Format.fprintf fmt (* accumulator is always tag 0 *)
+        "@[(let ($matched_value %a) (switch $matched_value @\n@ @ ((tag 0)@\n    %a)@\n  @[%a@]))@]"
+        pp_mllam c pp_mllam accu_br pp_branches br
+    | MLmatch_noaccu (c, br) ->
+      Format.fprintf fmt
+        "@[(let ($matched_value %a) (switch $matched_value @\n@ @ @[%a@]))@]"
+        pp_mllam c pp_branches br
+    | MLconstruct(_,_,tag,[||]) -> (* not a construct but a constant *)
+        Format.fprintf fmt "%i"
+          tag
+    | MLconstruct(_,_,tag,args) ->
+        Format.fprintf fmt "@[<2>(block (tag %i)%a)@]"
+          tag pp_args args
+    | MLisaccu (_, _, c) ->
         Format.fprintf fmt
-          "@[begin match Obj.magic (%a) with@\n| %s _ ->@\n  true@\n| _ ->@\n  false@\nend@]"
-        pp_mllam c accu
-
-  and pp_letrec fmt defs =
-    let len = Array.length defs in
-    let pp_one_rec (fn, argsn, body) =
-      Format.fprintf fmt "%a%a =@\n  %a"
-        pp_lname fn
-        pp_ldecls argsn pp_mllam body in
-    Format.fprintf fmt "@[let rec ";
-    pp_one_rec defs.(0);
-    for i = 1 to len - 1 do
-      Format.fprintf fmt "@\nand ";
-      pp_one_rec defs.(i)
-    done
-
-  and pp_blam fmt l =
-    match l with
-    | MLprimitive (_, _) | MLlam _ | MLletrec _ | MLlet _ | MLapp _ | MLif _ ->
-        Format.fprintf fmt "(%a)" pp_mllam l
-    | MLconstruct(_,_,_,args) when Array.length args > 0 ->
-        Format.fprintf fmt "(%a)" pp_mllam l
-    | _ -> pp_mllam fmt l
-
-  and pp_args sep fmt args =
-    let sep = if sep then "" else "," in
-    let len = Array.length args in
-    if len > 0 then begin
-      Format.fprintf fmt "%a" pp_blam args.(0);
-      for i = 1 to len - 1 do
-        Format.fprintf fmt "%s@ %a" sep pp_blam args.(i)
-      done
-    end
-
-  and pp_cargs fmt args =
-    let len = Array.length args in
-    match len with
-    | 0 -> ()
-    | 1 -> Format.fprintf fmt "@ %a" pp_blam args.(0)
-    | _ -> Format.fprintf fmt "@ @[<2>(%a)@]" (pp_args false) args
-
-  and pp_cparam fmt param =
-    match param with
-    | Some l -> pp_mllam fmt (MLlocal l)
-    | None -> Format.fprintf fmt "_"
-
+          "@[(switch %a@\n  ((tag 0) 1)@\n  (_ (tag _) 0))@]"
+        pp_mllam c
   and pp_cparams fmt params =
     let len = Array.length params in
-    match len with
-    | 0 -> ()
-    | 1 -> Format.fprintf fmt " %a" pp_cparam params.(0)
-    | _ ->
-        let aux fmt params =
-          Format.fprintf fmt "%a" pp_cparam params.(0);
-          for i = 1 to len - 1 do
-            Format.fprintf fmt ",%a" pp_cparam params.(i)
-          done in
-        Format.fprintf fmt "(%a)" aux params
-
-  and pp_branches prefix ind fmt bs =
-    let pp_branch (cargs,body) =
-      let pp_pat fmt = function
-        | ConstPattern i ->
-          Format.fprintf fmt "| %s "
-            (string_of_construct prefix ~constant:true ind i)
-        | NonConstPattern (tag,args) ->
-          Format.fprintf fmt "| %s%a "
-            (string_of_construct prefix ~constant:false ind tag) pp_cparams args in
-      let rec pp_pats fmt pats =
-        match pats with
-        | [] -> ()
-        | pat::pats ->
-          Format.fprintf fmt "%a%a" pp_pat pat pp_pats pats
-      in
-      Format.fprintf fmt "%a ->@\n  %a@\n" pp_pats cargs pp_mllam body
+    for i = 0 to len - 1 do
+      match params.(i) with
+      | None -> ()
+      | Some param ->
+        Format.fprintf fmt " (%a (field %i $matched_value))" pp_mllam (MLlocal param) i
+    done
+  and pp_branches fmt bs =
+    let rec pp_branch fmt (cargs,body) =
+      let pp_pat_and_block fmt = function
+        | ConstPattern i, body ->
+          Format.fprintf fmt "%i %a" i pp_mllam body
+        | NonConstPattern (tag,args), body ->
+          Format.fprintf fmt "@[<2>(tag %i) (let%a@\n%a)@]"
+            tag pp_cparams args pp_mllam body in
+      match cargs with
+      | [] -> ()
+      | pat::pats -> (* we duplicate the branches because there is no simpler alternative to due to match bindings *)
+        Format.fprintf fmt "(%a)@\n%a" pp_pat_and_block (pat, body) pp_branch (pats, body)
     in
-    Array.iter pp_branch bs
-
+    Array.iter (pp_branch fmt) bs
+  and pp_letrec fmt defs =
+    let pp_one_rec (fn, argsn, body) =
+      Format.fprintf fmt "(%a@ %a)@\n"
+        pp_lname fn
+        pp_mllam (MLlam(argsn, body)) in
+    Array.iter pp_one_rec defs
+  and pp_args fmt args =
+    if args <> [||] then
+      Array.iter (Format.fprintf fmt "@ %a" pp_mllam) args
+    else Format.fprintf fmt "@ 0" (* 0 is () in malfunction *)
   and pp_primitive fmt = function
-    | Mk_prod -> Format.fprintf fmt "mk_prod"
-    | Mk_sort -> Format.fprintf fmt "mk_sort_accu"
-    | Mk_ind -> Format.fprintf fmt "mk_ind_accu"
-    | Mk_const -> Format.fprintf fmt "mk_constant_accu"
-    | Mk_sw -> Format.fprintf fmt "mk_sw_accu"
+    | Mk_prod -> Format.fprintf fmt "(global $Nativevalues $mk_prod)"
+    | Mk_sort -> Format.fprintf fmt "(global $Nativevalues $mk_sort_accu)"
+    | Mk_ind -> Format.fprintf fmt "(global $Nativevalues $mk_ind_accu)"
+    | Mk_const -> Format.fprintf fmt "(global $Nativevalues $mk_constant_accu)"
+    | Mk_sw -> Format.fprintf fmt "(global $Nativevalues $mk_sw_accu)"
     | Mk_fix(rec_pos,start) ->
-        let pp_rec_pos fmt rec_pos =
-          Format.fprintf fmt "@[[| %i" rec_pos.(0);
-          for i = 1 to Array.length rec_pos - 1 do
-            Format.fprintf fmt ";@ %i" rec_pos.(i)
-          done;
-          Format.fprintf fmt " |]@]" in
-        Format.fprintf fmt "mk_fix_accu %a %i" pp_rec_pos rec_pos start
-    | Mk_cofix(start) -> Format.fprintf fmt "mk_cofix_accu %i" start
-    | Mk_rel i -> Format.fprintf fmt "mk_rel_accu %i" i
+        Format.fprintf fmt "@[<2>(apply (global $Nativevalues $mk_fix_accu) (block (tag 0)";
+        Array.iter (fun i -> Format.fprintf fmt "@\n%a" pp_mllam (MLint i)) rec_pos;
+        Format.fprintf fmt ")@]@\n %i)" start
+    | Mk_cofix(start) -> Format.fprintf fmt "(apply (global $Nativevalues $mk_cofix_accu) %i)" start
+    | Mk_rel i -> Format.fprintf fmt "(apply (global $Nativevalues $mk_rel_accu) %i)" i
     | Mk_var id ->
-        Format.fprintf fmt "mk_var_accu (Names.Id.of_string \"%s\")" (string_of_id id)
-    | Mk_proj -> Format.fprintf fmt "mk_proj_accu"
-    | Mk_empty_instance -> Format.fprintf fmt "UVars.Instance.empty"
-    | Is_int -> Format.fprintf fmt "is_int"
-    | Is_float -> Format.fprintf fmt "is_float"
-    | Is_string -> Format.fprintf fmt "is_string"
-    | Is_parray -> Format.fprintf fmt "is_parray"
-    | Cast_accu -> Format.fprintf fmt "cast_accu"
-    | Array_get -> Format.fprintf fmt "Array.get"
-    | Force_cofix -> Format.fprintf fmt "force_cofix"
-    | Mk_uint -> Format.fprintf fmt "mk_uint"
-    | Mk_float -> Format.fprintf fmt "mk_float"
-    | Mk_string -> Format.fprintf fmt "mk_string"
-    | Mk_int -> Format.fprintf fmt "mk_int"
-    | Val_to_int -> Format.fprintf fmt "val_to_int"
-    | Mk_evar -> Format.fprintf fmt "mk_evar_accu"
-    | MLand -> Format.fprintf fmt "(&&)"
-    | MLnot -> Format.fprintf fmt "not"
-    | MLland -> Format.fprintf fmt "(land)"
-    | MLmagic -> Format.fprintf fmt "Obj.magic"
-    | MLsubst_instance_instance -> Format.fprintf fmt "UVars.subst_instance_instance"
-    | MLsubst_instance_sort -> Format.fprintf fmt "UVars.subst_instance_sort"
-    | MLparray_of_array -> Format.fprintf fmt "parray_of_array"
+        Format.fprintf fmt "(apply (global $Nativevalues $mk_var_accu) (apply (global $Names $Id $of_string) \"%s\"))" (string_of_id id)
+    | Mk_proj -> Format.fprintf fmt "(global $Nativevalues $mk_proj_accu)"
+    | Mk_empty_instance -> Format.fprintf fmt "(global $UVars $Instance $empty)"
+    | Is_int -> Format.fprintf fmt "(global $Nativevalues $is_int)"
+    | Is_float -> Format.fprintf fmt "(global $Nativevalues $is_float)"
+    | Is_string -> Format.fprintf fmt "(global $Nativevalues $is_string)"
+    | Is_parray -> Format.fprintf fmt "(global $Nativevalues $is_parray)"
+    | Cast_accu -> Format.fprintf fmt "(global $Nativevalues $cast_accu)"
+    | Force_cofix -> Format.fprintf fmt "(global $Nativevalues $force_cofix)"
+    | Mk_uint -> Format.fprintf fmt "(global $Nativevalues $mk_uint)"
+    | Mk_float -> Format.fprintf fmt "(global $Nativevalues $mk_float)"
+    | Mk_string -> Format.fprintf fmt "(global $Nativevalues $mk_string)"
+    | Mk_int -> Format.fprintf fmt "(global $Nativevalues $mk_int)"
+    | Val_to_int -> Format.fprintf fmt "(global $Nativevalues $val_to_int)"
+    | Mk_evar -> Format.fprintf fmt "(global $Nativevalues $mk_evar_accu)"
+    | MLsubst_instance_instance -> Format.fprintf fmt "(global $UVars $subst_instance_instance)"
+    | MLsubst_instance_sort -> Format.fprintf fmt "(global $UVars $subst_instance_sort)"
+    | MLparray_of_array -> Format.fprintf fmt "(global $Nativevalues $parray_of_array)"
     | Coq_primitive (op, false) ->
-       Format.fprintf fmt "no_check_%s" (CPrimitives.to_string op)
-    | Coq_primitive (op, true) -> Format.fprintf fmt "%s" (CPrimitives.to_string op)
-    | Get_value -> Format.fprintf fmt "get_value"
-    | Get_sort -> Format.fprintf fmt "get_sort"
-    | Get_name -> Format.fprintf fmt "get_name"
-    | Get_const -> Format.fprintf fmt "get_const"
-    | Get_match -> Format.fprintf fmt "get_match"
-    | Get_ind -> Format.fprintf fmt "get_ind"
-    | Get_evar -> Format.fprintf fmt "get_evar"
-    | Get_instance -> Format.fprintf fmt "get_instance"
-    | Get_proj -> Format.fprintf fmt "get_proj"
-    | Get_symbols -> Format.fprintf fmt "get_symbols"
-    | Lazy -> Format.fprintf fmt "lazy"
+       Format.fprintf fmt "(global $Nativevalues $no_check_%s)" (CPrimitives.to_string op)
+    | Coq_primitive (op, true) -> Format.fprintf fmt "(global $Nativevalues $%s)" (CPrimitives.to_string op)
+    | Get_value -> Format.fprintf fmt "(global $Nativecode $get_value)"
+    | Get_sort -> Format.fprintf fmt "(global $Nativecode $get_sort)"
+    | Get_name -> Format.fprintf fmt "(global $Nativecode $get_name)"
+    | Get_const -> Format.fprintf fmt "(global $Nativecode $get_const)"
+    | Get_match -> Format.fprintf fmt "(global $Nativecode $get_match)"
+    | Get_ind -> Format.fprintf fmt "(global $Nativecode $get_ind)"
+    | Get_evar -> Format.fprintf fmt "(global $Nativecode $get_evar)"
+    | Get_instance -> Format.fprintf fmt "(global $Nativecode $get_instance)"
+    | Get_proj -> Format.fprintf fmt "(global $Nativecode $get_proj)"
+    | Get_symbols -> Format.fprintf fmt "(global $Nativelib $get_symbols)"
+    | Str_decode -> Format.fprintf fmt "(global $Nativevalues $str_decode)"
+    | MLand
+    | Array_get
+    | MLnot
+    | MLland
+    | Force
+    | Lazy -> assert false (* theses cases has been treated separately in pp_mllam *)
   in
   Format.fprintf fmt "@[%a@]" pp_mllam l
 
 let pp_array fmt t =
-  let len = Array.length t in
-  Format.fprintf fmt "@[<2>[|";
-  for i = 0 to len - 2 do
-    Format.fprintf fmt "%a;@ " pp_mllam t.(i)
-  done;
-  if len > 0 then
-    Format.fprintf fmt "%a" pp_mllam t.(len - 1);
-  Format.fprintf fmt "|]@]"
+  Format.fprintf fmt "(block (tag 0)";
+  Array.iter (Format.fprintf fmt "@ %a" pp_mllam) t;
+  Format.fprintf fmt ")"
 
 let pp_cofix fmt (gn, s) =
-  let pp_dummy fmt len =
-    let dummy = String.concat "; " (List.make len "0") in
-    Format.fprintf fmt "@[(Obj.magic [|%s|] : Nativevalues.t array)@]" dummy
+  let subst_gname gn v l =
+    let rec aux l =
+      match l with
+      | MLglobal id when eq_gname gn id -> v
+      | MLglobal _ | MLlocal _ | MLint _ | MLuint _ | MLfloat _ | MLstring _ -> l
+      | MLprimitive (p, args) -> MLprimitive (p, Array.map aux args)
+      | MLlam(params,body) -> MLlam(params, aux body)
+      | MLletrec(defs,body) ->
+        let arec (f,params,body) = (f,params,aux body) in
+        MLletrec(Array.map arec defs, aux body)
+      | MLlet(id,def,body) -> MLlet(id,aux def, aux body)
+      | MLapp(f,args) -> MLapp(aux f, Array.map aux args)
+      | MLif(t,b1,b2) -> MLif(aux t, aux b1, aux b2)
+      | MLmatch(a,accu,bs) ->
+          let auxb (cargs,body) = (cargs,aux body) in
+          MLmatch(a,aux accu, Array.map auxb bs)
+      | MLmatch_noaccu(a,bs) ->
+          let auxb (cargs,body) = (cargs,aux body) in
+          MLmatch_noaccu(a, Array.map auxb bs)
+      | MLconstruct(prefix,c,tag,args) -> MLconstruct(prefix,c,tag,Array.map aux args)
+      | MLsetref(s,l1) -> MLsetref(s,aux l1)
+      | MLsequence(l1,l2) -> MLsequence(aux l1, aux l2)
+      | MLarray arr -> MLarray (Array.map aux arr)
+      | MLisaccu (s, ind, l) -> MLisaccu (s, ind, aux l)
+    in
+    aux l
+  in let s = Array.map (subst_gname gn (MLprimitive(Force, [|MLglobal gn|])) ) s in
+  Format.fprintf fmt "@[(let (rec (%a (lazy %a))) (force %a))@]" pp_gname gn pp_array s pp_gname gn
+
+let pp_type_decl fmt ind lar =
+  let rec aux s arity =
+    if Int.equal arity 0 then s else aux (s^" * t") (arity-1) in
+  let pp_const_sig fmt (tag,arity) =
+    if arity > 0 then
+      let sig_str = aux "of t" (arity-1) in
+      let cstr = string_of_construct "" ~constant:false ind tag in
+      Format.fprintf fmt "  | %s %s@\n" cstr sig_str
+    else
+      let cstr = string_of_construct "" ~constant:true ind tag in
+      Format.fprintf fmt "  | %s@\n" cstr
   in
-  let pp_knot fmt n =
-    for i = 0 to n - 1 do
-      Format.fprintf fmt "@[<2>let () = (%a).(%i) <-@ Obj.magic @[<2>(%a)@] in@]@\n" pp_gname gn i pp_mllam s.(i)
-    done
+  let pp_const_sigs fmt lar =
+    Format.fprintf fmt "  | %s of t@\n" (string_of_accu_construct "" ind);
+    Array.iter (pp_const_sig fmt) lar
   in
-  let len = Array.length s in
-  Format.fprintf fmt "@[let %a = %a in@\n%a%a@]" pp_gname gn pp_dummy len pp_knot len pp_gname gn
-
-let type_of_global gn c = match gn with
-  | Ginternal "symbols_tbl" -> ""
-  | _ -> match c with
-    | MLprimitive (Lazy, _) -> " : Nativevalues.t Lazy.t"
-    | MLlam ([|_|], MLprimitive (Lazy, _)) -> " : Nativevalues.t -> Nativevalues.t Lazy.t"
-    | MLprimitive ((Mk_ind | Mk_const), [|_|]) -> " : UVars.Instance.t -> Nativevalues.t"
-    | MLsetref (_,_) -> " : unit"
-    | _ -> " : Nativevalues.t"
+  Format.fprintf fmt "@[type ind_%s =@\n%a@]@\n@." (string_of_ind ind) pp_const_sigs lar
 
 let pp_global fmt g =
   match g with
   | Glet (gn, c) ->
-      Format.fprintf fmt "@[let %a%s = let Refl = Nativevalues.t_eq in@\n  %a@]@\n@." pp_gname gn
-        (type_of_global gn c)
-        pp_mllam c
-  | Gopen s ->
-      Format.fprintf fmt "@[open %s@]@." s
-  | Gtype (ind, lar) ->
+      Format.fprintf fmt "@[( %a  %a )@]@\n@." pp_gname gn pp_mllam c
+  | Gtype (ind, lar) -> (* types are not needed in malfunction, we will leave them as comments *)
     let rec aux s arity =
       if Int.equal arity 0 then s else aux (s^" * Nativevalues.t") (arity-1) in
     let pp_const_sig fmt (tag,arity) =
       if arity > 0 then
         let sig_str = aux "of Nativevalues.t" (arity-1) in
         let cstr = string_of_construct "" ~constant:false ind tag in
-        Format.fprintf fmt "  | %s %s@\n" cstr sig_str
+        Format.fprintf fmt ";  | %s %s@\n" cstr sig_str
       else
         let cstr = string_of_construct "" ~constant:true ind tag in
-        Format.fprintf fmt "  | %s@\n" cstr
+        Format.fprintf fmt ";  | %s@\n" cstr
     in
     let pp_const_sigs fmt lar =
-      Format.fprintf fmt "  | %s of Nativevalues.t@\n" (string_of_accu_construct "" ind);
+      Format.fprintf fmt ";  | %s of Nativevalues.t@\n" (string_of_accu_construct "" ind);
       Array.iter (pp_const_sig fmt) lar
     in
-    Format.fprintf fmt "@[type ind_%s =@\n%a@]@\n@." (string_of_ind ind) pp_const_sigs lar
+    Format.fprintf fmt "@[;type ind_%s =@\n%a@]@\n@." (string_of_ind ind) pp_const_sigs lar
+  | Gopen _ ->
+      () (* open do not exist in malfunction, and there is no interest in leaving them as comments *)
+  | Gletcase(gn,[||],a,accu,bs) -> (* simple biding and not a function *)
+      Format.fprintf fmt "@[; Hash = %i@\n(%a %a)@]@\n@." (* no need to be recursive as we are sane and do not create recursive values other than functions *)
+      (hash_global g)
+        pp_gname gn
+        pp_mllam (MLmatch(a,accu,bs))
+  | Gletcase(gn,params,a,accu,bs) -> (* a function *)
+      Format.fprintf fmt "@[; Hash = %i@\n(rec (%a (lambda (%a)@\n  %a)))@]@\n@."
+      (hash_global g)
+        pp_gname gn pp_ldecls params
+        pp_mllam (MLmatch(a,accu,bs))
+  | Gtblfixtype (g, [||], t) -> (* not a function but a definition *)
+      Format.fprintf fmt "@[<2>(%a %a)@]@\n@." pp_gname g
+        pp_array t
   | Gtblfixtype (g, params, t) ->
-      Format.fprintf fmt "@[let %a %a : Nativevalues.t array = let Refl = Nativevalues.t_eq in@\n  %a@]@\n@." pp_gname g
+      Format.fprintf fmt "@[<2>(%a (lambda (%a)@\n%a))@]@\n@." pp_gname g
         pp_ldecls params pp_array t
+  | Gtblnorm (g, [||], t) -> (* not a function but a definition *)
+      Format.fprintf fmt "@[<2>(%a %a)@]@\n@." pp_gname g
+        pp_array t
   | Gtblnorm (g, params, t) ->
-      Format.fprintf fmt "@[let %a %a : Nativevalues.t array = let Refl = Nativevalues.t_eq in@\n  %a@]@\n@." pp_gname g
+      Format.fprintf fmt "@[<2>(%a (lambda (%a)@\n%a))@]@\n@." pp_gname g
         pp_ldecls params pp_array t
+  | Gtblcofix (g, [||], s) -> (* not a function but a definition *)
+      Format.fprintf fmt "@[(%a %a)@]@\n@." pp_gname g
+        pp_cofix (g, s)
   | Gtblcofix (g, params, s) ->
-      Format.fprintf fmt "@[let %a%a : Nativevalues.t array = let Refl = Nativevalues.t_eq in@\n  %a@]@\n@." pp_gname g
-        pp_ldecls params pp_cofix (g, s);
-  | Gletcase(gn,params,annot,a,accu,bs) ->
-      Format.fprintf fmt "@[(* Hash = %i *)@\nlet rec %a %a : Nativevalues.t = let Refl = Nativevalues.t_eq in@\n  %a@]@\n@."
-      (hash_global g)
-        pp_gname gn pp_ldecls params
-        pp_mllam (MLmatch(annot,a,accu,bs))
+      Format.fprintf fmt "@[(%a (lambda (%a)@\n  %a))@]@\n@." pp_gname g
+        pp_ldecls params pp_cofix (g, s)
   | Gcomment s ->
-      Format.fprintf fmt "@[(* %s *)@]@." s
+      List.iter (fun line -> Format.fprintf fmt ";@[ %s @]@." line) (String.split_on_char '\n' s)
+
+(* needed to know the names of the values to export *)
+let global_to_mlf_name g =
+  match g with
+  | Gtblfixtype (gn,_,_)
+  | Gtblnorm (gn,_,_)
+  | Gtblcofix (gn,_,_)
+  | Gletcase(gn,_,_,_,_)
+  | Glet (gn,_) ->
+    let gn = string_of_gname gn in
+    if gn = "_" || gn = "" then None else Some gn
+  | Gtype _
+  | Gcomment _
+  | Gopen _ -> None
+
+let pp_global_interface fmt g =
+  match g with
+  | Gtblnorm (_,_,_)
+  | Gtblcofix (_,_,_)
+  | Gtblfixtype (_,_,_)
+  | Gletcase (_,_,_,_,_)
+  | Glet (_,_) ->
+    begin match global_to_mlf_name g with
+    | None -> ()
+    | Some ident ->
+      let ident = String.sub ident 1 ((String.length ident) - 1) in (* we remove the $ before the local variable *)
+      Format.fprintf fmt "val %s : t@." ident
+    end
+  | Gcomment _
+  | Gopen _ -> ()
+  | Gtype (ind, lar) -> pp_type_decl fmt ind lar
 
 (** Compilation of elements in environment **)
 let rec compile_with_fv ?(wrap = fun t -> t) cenv env sigma univ auxdefs l t =
@@ -2236,8 +2293,6 @@ let compile_mind cenv mb mind stack =
     let add_proj proj_arg acc _pb =
       let tbl = ob.mind_reloc_tbl in
       (* Building info *)
-      let asw = { asw_ind = ind; asw_prefix = "";
-                  asw_reloc = tbl } in
       let c_uid = fresh_lname cenv Anonymous in
       let cf_uid = fresh_lname cenv Anonymous in
       let tag, arity = tbl.(0) in
@@ -2249,7 +2304,7 @@ let compile_mind cenv mb mind stack =
       let i = push_symbol cenv (SymbProj (ind, proj_arg)) in
       let accu = MLprimitive (Cast_accu, [|MLlocal cf_uid|]) in
       let accu_br = MLprimitive (Mk_proj, [|get_proj_code i;accu|]) in
-      let code = MLmatch(asw,MLlocal cf_uid,accu_br,[|[NonConstPattern (tag,cargs)],MLlocal ci_uid|]) in
+      let code = MLmatch(MLlocal cf_uid,accu_br,[|[NonConstPattern (tag,cargs)],MLlocal ci_uid|]) in
       let force_c =
         if mb.mind_finite <> CoFinite
         then MLlocal c_uid
@@ -2392,16 +2447,16 @@ let mk_conv_code env sigma prefix t1 t2 =
   let code2 = lambda_of_constr env sigma t2 in
   let (gl,code1) = compile_with_fv cenv env sigma UGlobal gl None code1 in
   let (gl,code2) = compile_with_fv cenv env sigma UGlobal gl None code2 in
-  let t1 = mk_internal_let "t1" code1 in
-  let t2 = mk_internal_let "t2" code2 in
-  let g1 = MLglobal (Ginternal "t1") in
-  let g2 = MLglobal (Ginternal "t2") in
-  let setref1 = Glet(Ginternal "_", MLsetref("rt1",g1)) in
-  let setref2 = Glet(Ginternal "_", MLsetref("rt2",g2)) in
+  let t1 = mk_internal_let "$t1" code1 in
+  let t2 = mk_internal_let "$t2" code2 in
+  let g1 = MLglobal (Ginternal "$t1") in
+  let g2 = MLglobal (Ginternal "$t2") in
+  let setref1 = Glet(Ginternal "_", MLsetref("(global $Nativelib $rt1)",g1)) in
+  let setref2 = Glet(Ginternal "_", MLsetref("(global $Nativelib $rt2)",g2)) in
   let gl = List.rev (setref2 :: setref1 :: t2 :: t1 :: gl) in
-  let header = Glet(Ginternal "symbols_tbl",
+  let header = Glet(Ginternal "$symbols_tbl",
     MLprimitive (Get_symbols,
-      [|MLglobal (Ginternal "()")|])) in
+      [|MLglobal (Ginternal "0")|])) in
   let symbols = get_cenv_symbols cenv in
   header::gl, symbols, (mind_updates, const_updates)
 
@@ -2413,19 +2468,18 @@ let mk_norm_code env sigma prefix t =
   in
   let code = lambda_of_constr env sigma t in
   let (gl,code) = compile_with_fv cenv env sigma UGlobal gl None code in
-  let t1 = mk_internal_let "t1" code in
-  let g1 = MLglobal (Ginternal "t1") in
-  let setref = Glet(Ginternal "_", MLsetref("rt1",g1)) in
+  let t1 = mk_internal_let "$t1" code in
+  let g1 = MLglobal (Ginternal "$t1") in
+  let setref = Glet(Ginternal "_", MLsetref("(global $Nativelib $rt1)",g1)) in
   let gl = List.rev (setref :: t1 :: gl) in
-  let header = Glet(Ginternal "symbols_tbl",
+  let header = Glet(Ginternal "$symbols_tbl",
     MLprimitive (Get_symbols,
-      [|MLglobal (Ginternal "()")|])) in
+      [|MLglobal (Ginternal "0")|])) in
   let symbols = get_cenv_symbols cenv in
   header::gl, symbols, (mind_updates, const_updates)
 
 let mk_library_header (symbols : Nativevalues.symbols) =
-  let symbols = Format.sprintf "(str_decode \"%s\")" (str_encode symbols) in
-  [Glet(Ginternal "symbols_tbl", MLglobal (Ginternal symbols))]
+  [Glet(Ginternal "$symbols_tbl", MLprimitive (Str_decode, [|MLglobal (Ginternal ("\"" ^ (str_encode symbols) ^ "\""))|]))]
 
 let update_location r =
   r.upd_info := Linked r.upd_prefix
diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli
index d3eb9750f457..7a5133c6a796 100644
--- a/kernel/nativecode.mli
+++ b/kernel/nativecode.mli
@@ -30,6 +30,10 @@ val keep_debug_files : unit -> bool
 
 val pp_global : Format.formatter -> global -> unit
 
+val global_to_mlf_name : global -> string option
+
+val pp_global_interface : Format.formatter -> global -> unit
+
 val mk_open : string -> global
 
 val get_value : symbols -> int -> Nativevalues.t
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 0b40d61b78e9..83216e242b01 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -189,7 +189,7 @@ let warn_no_native_compiler =
 
 let native_conv_gen (type err) pb sigma env (state, check) t1 t2 =
   Nativelib.link_libraries ();
-  let ml_filename, prefix = Nativelib.get_ml_filename () in
+  let ml_filename, prefix = Nativelib.get_mlf_filename () in
   let code, symbols, upds = mk_conv_code env sigma prefix t1 t2 in
   let fn = Nativelib.compile ml_filename code ~profile:false in
   debug_native_compiler (fun () -> Pp.str "Running test...");
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index 4a2c2c731b18..56104f8cf5f9 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -92,32 +92,41 @@ let rt2 = ref None
 
 let get_symbols () = !rsymbols
 
-let get_ml_filename () =
+let get_mlf_filename () =
   let temp_dir = force_temp_dir() in
   let filename = Filename.temp_file ~temp_dir "Coq_native" source_ext in
   let prefix = Filename.chop_extension (Filename.basename filename) ^ "." in
   filename, prefix
 
-let write_ml_code fn ?(header=[]) code =
+let write_code fn ?(header=[]) code =
   let header = open_header@header in
   let ch_out = open_out fn in
   let fmt = Format.formatter_of_out_channel ch_out in
+  Format.fprintf fmt "@[(module@]@\n";
   List.iter (pp_global fmt) (header@code);
-  close_out ch_out
+  Format.fprintf fmt "@[(export";
+  List.iter (Format.fprintf fmt " %s") (List.map_filter global_to_mlf_name code);
+  Format.fprintf fmt "))@]@.";
+  close_out ch_out;
+  let ch_mli_out = open_out ((Filename.chop_extension fn)^".mli") in
+  let fmt = Format.formatter_of_out_channel ch_mli_out in
+  Format.fprintf fmt "type t\n";
+  List.iter (pp_global_interface fmt) code;
+  close_out ch_mli_out
 
-let error_native_compiler_failed e =
+let error_native_compiler_failed e head =
   let msg = match e with
-  | Inl (Unix.WEXITED 127) -> Pp.(strbrk "The OCaml compiler was not found. Make sure it is installed, together with findlib.")
+  | Inl (Unix.WEXITED 127) -> Pp.(strbrk head ++ str "The OCaml compiler was not found. Make sure it is installed, together with findlib.")
   | Inl (Unix.WEXITED n) ->
-     Pp.(strbrk "Native compiler exited with status" ++ str" " ++ int n
+     Pp.(strbrk head ++ str "Native compiler exited with status" ++ str" " ++ int n
          ++ strbrk (if n = 2 then " (in case of stack overflow, increasing stack size (typically with \"ulimit -s\") often helps)" else ""))
-  | Inl (Unix.WSIGNALED n) -> Pp.(strbrk "Native compiler killed by signal" ++ str" " ++ int n)
-  | Inl (Unix.WSTOPPED n) -> Pp.(strbrk "Native compiler stopped by signal" ++ str" " ++ int n)
-  | Inr e -> Pp.(strbrk "Native compiler failed with error: " ++ strbrk (Unix.error_message e))
+  | Inl (Unix.WSIGNALED n) -> Pp.(strbrk head ++ str "Native compiler killed by signal" ++ str" " ++ int n)
+  | Inl (Unix.WSTOPPED n) -> Pp.(strbrk head ++ str "Native compiler stopped by signal" ++ str" " ++ int n)
+  | Inr e -> Pp.(strbrk head ++ str "Native compiler failed with error: " ++ strbrk (Unix.error_message e))
   in
   CErrors.user_err msg
 
-let call_compiler ?profile:(profile=false) ml_filename =
+let call_compiler ?profile:(profile=false) mlf_filename =
   (* The below path is computed from Require statements, by uniquizing
      the paths, see [Library.get_used_load_paths] This is in general
      hacky and we should do a bit better once we move loadpath to its
@@ -127,47 +136,63 @@ let call_compiler ?profile:(profile=false) ml_filename =
   (* To ease the build we also consider the current dir, but at some point the build system should manage both *)
   let install_load_path = List.map (fun dn -> dn / dft_output_dir) require_load_path @ require_load_path in
   let include_dirs = List.flatten (List.map (fun x -> ["-I"; x]) (get_include_dirs () @ install_load_path)) in
-  let f = Filename.chop_extension ml_filename in
+  let f = Filename.chop_extension mlf_filename in
   let link_filename = f ^ ".cmo" in
   let link_filename = Dynlink.adapt_filename link_filename in
   let remove f = if Sys.file_exists f then Sys.remove f in
   remove link_filename;
   remove (f ^ ".cmi");
-  let initial_args =
-    if Dynlink.is_native then
-      ["opt"; "-shared"]
-     else
-      ["ocamlc"; "-c"]
-  in
   let profile_args =
     if profile then
       ["-g"]
     else
       []
   in
-  let flambda_args = if Sys.(backend_type = Native) then ["-Oclassic"] else [] in
+  (* let flambda_args = if Sys.(backend_type = Native) then ["-Oclassic"] else [] in *)
   let args =
-    initial_args @
+      ["cmx"; mlf_filename] @
       profile_args @
-        flambda_args @
+        (* flambda_args @ *)
       ("-o"::link_filename
        ::"-rectypes"
-       ::"-w"::"a"
-       ::include_dirs) @
-    ["-impl"; ml_filename] in
+       ::"-I"::(Filename.dirname mlf_filename)
+       (* ::"-w"::"a" *)
+       ::include_dirs) in
+  let ocamlc_args = ["ocamlc"; "-opaque"; "-c"; f^".mli"]@include_dirs in
+  let ocamlopt_args = ["opt"; "-shared"; "-o"; f^".cmxs"; f^".cmx"] in
+  let malfunction = "malfunction" in
   let ocamlfind = Boot.Env.ocamlfind () in
-  debug_native_compiler (fun () -> Pp.str (ocamlfind ^ " " ^ (String.concat " " args)));
-  try
-    let res = CUnix.sys_command ocamlfind args in
+  begin try
+    debug_native_compiler (fun () -> Pp.str (ocamlfind ^ " " ^ (String.concat " " ocamlc_args)));
+    let res = CUnix.sys_command ocamlfind ocamlc_args in
+    match res with
+    | Unix.WEXITED 0 -> ()
+    | Unix.WEXITED _n | Unix.WSIGNALED _n | Unix.WSTOPPED _n ->
+      error_native_compiler_failed (Inl res) "During .cmi generation: "
+  with Unix.Unix_error (e,_,_) ->
+    error_native_compiler_failed (Inr e) "During .cmi generation: "
+  end; begin try
+    debug_native_compiler (fun () -> Pp.str (malfunction ^ " " ^ (String.concat " " args)));
+    let res = CUnix.sys_command malfunction args in
+    match res with
+    | Unix.WEXITED 0 -> ()
+    | Unix.WEXITED _n | Unix.WSIGNALED _n | Unix.WSTOPPED _n ->
+      error_native_compiler_failed (Inl res) "During .mlf compilation: "
+  with Unix.Unix_error (e,_,_) ->
+    error_native_compiler_failed (Inr e) "During .mlf compilation: "
+  end; begin try
+    debug_native_compiler (fun () -> Pp.str (ocamlfind ^ " " ^ (String.concat " " ocamlopt_args)));
+    let res = if Dynlink.is_native then CUnix.sys_command ocamlfind ocamlopt_args else Unix.WEXITED 0 in
     match res with
     | Unix.WEXITED 0 -> link_filename
     | Unix.WEXITED _n | Unix.WSIGNALED _n | Unix.WSTOPPED _n ->
-      error_native_compiler_failed (Inl res)
+      error_native_compiler_failed (Inl res) "During .cmxs generation"
   with Unix.Unix_error (e,_,_) ->
-    error_native_compiler_failed (Inr e)
+    error_native_compiler_failed (Inr e) "During .cmxs generation"
+  end
 
 let compile fn code ~profile:profile =
-  write_ml_code fn code;
+  write_code fn code;
   let r = call_compiler ~profile fn in
   (* NB: to prevent reusing the same filename we MUST NOT remove the file until exit
      cf #15263 *)
@@ -187,7 +212,7 @@ let compile_library (code, symb) fn =
     with Unix.Unix_error (Unix.EEXIST, _, _) -> ()
   in
   let fn = dirname / basename in
-  write_ml_code fn ~header code;
+  write_code fn ~header code;
   let _ = call_compiler fn in
   delay_cleanup_file fn
 
diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli
index 650047464281..b58c414d31a6 100644
--- a/kernel/nativelib.mli
+++ b/kernel/nativelib.mli
@@ -22,7 +22,7 @@ val get_load_paths : (unit -> string list) ref
 
 val load_obj : (string -> unit) ref
 
-val get_ml_filename : unit -> string * string
+val get_mlf_filename : unit -> string * string
 
 (** [compile file code ~profile] will compile native [code] to [file],
    and return the name of the object file; this name depends on
diff --git a/kernel/pstring.ml b/kernel/pstring.ml
index aff724116f05..0b833d89729c 100644
--- a/kernel/pstring.ml
+++ b/kernel/pstring.ml
@@ -76,3 +76,6 @@ let unsafe_of_string : string -> t = fun s -> s
 
 let compile : t -> string =
   Printf.sprintf "Pstring.unsafe_of_string %S"
+
+let compile_mlf : t -> string =
+  Printf.sprintf "(apply (global $Pstring $unsafe_of_string) %S)"
diff --git a/kernel/pstring.mli b/kernel/pstring.mli
index 120a6359fd87..49fc45a97812 100644
--- a/kernel/pstring.mli
+++ b/kernel/pstring.mli
@@ -66,3 +66,6 @@ val unsafe_of_string : string -> t
 
 (** [compile s] outputs an OCaml expression producing primitive string [s]. *)
 val compile : t -> string
+
+(** [compile_mlf s] outputs a malfunction expression producing primitive string [s]. *)
+val compile_mlf : t -> string
diff --git a/kernel/uint63.mli b/kernel/uint63.mli
index e77bd78eea37..995885d21d3f 100644
--- a/kernel/uint63.mli
+++ b/kernel/uint63.mli
@@ -36,6 +36,8 @@ val to_string : t -> string
 
 val compile : t -> string
 
+val compile_mlf : t -> string
+
 (* constants *)
 val zero    : t
 val one : t
diff --git a/kernel/uint63_31.ml b/kernel/uint63_31.ml
index 1c6a4489a23b..820e332f82ce 100644
--- a/kernel/uint63_31.ml
+++ b/kernel/uint63_31.ml
@@ -45,6 +45,11 @@ let to_string i = Int64.to_string i
 (* Compiles an unsigned int to OCaml code *)
 let compile i = Printf.sprintf "Uint63.of_int64 (%LiL)" i
 
+(* Compiles an unsigned int to malfunction code *)
+let compile_mlf i =
+  if Int64.compare i 0L >= 0 then Printf.sprintf "(apply (global &Uint63 &of_int64) %Li.i64)" i (* the internal value (a signed integer) is positive *)
+  else Printf.sprintf "(apply (global &Uint63 &of_int64) (neg.i64 %Li.i64))" (Int64.neg i) (* the internal value is negative and we must take it into account *)
+
     (* comparison *)
 let lt x y =
   Int64.compare x y < 0
diff --git a/kernel/uint63_63.ml b/kernel/uint63_63.ml
index e376a4a91937..99347be4c135 100644
--- a/kernel/uint63_63.ml
+++ b/kernel/uint63_63.ml
@@ -43,6 +43,11 @@ let to_string i = Int64.to_string (to_uint64 i)
 (* Compiles an unsigned int to OCaml code *)
 let compile i = Printf.sprintf "Uint63.of_int (%i)" i
 
+(* Compiles an unsigned int to malfunction code *)
+let compile_mlf i =
+  if i >= 0 then Printf.sprintf "(apply (global $Uint63 $of_int) %i)" i
+  else Printf.sprintf "(apply (global $Uint63 $of_int) (neg %i))" (-i)
+
 let zero = 0
 let one = 1
 
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index fea696a3867a..d65d09c47f93 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -497,7 +497,7 @@ let native_norm env sigma c ty =
   let ty = EConstr.Unsafe.to_constr ty in
     let profile = get_profiling_enabled () in
     let print_timing = get_timing_enabled () in
-    let ml_filename, prefix = Nativelib.get_ml_filename () in
+    let ml_filename, prefix = Nativelib.get_mlf_filename () in
     let tnc0 = Unix.gettimeofday () in
     let code, symbols, upd = mk_norm_code env (evars_of_evar_map sigma) prefix c in
     let tnc1 = Unix.gettimeofday () in