diff --git a/compiler/heptagon/transformations/completion.ml b/compiler/heptagon/transformations/completion.ml
index 88ce10a..ba013d0 100644
--- a/compiler/heptagon/transformations/completion.ml
+++ b/compiler/heptagon/transformations/completion.ml
@@ -86,7 +86,8 @@ let eqdesc funs _ ed = match ed with
       let ed, defnames =
         Hept_mapfold.eqdesc funs_collect Env.empty ed in
       (* add missing defnames *)
-      Hept_mapfold.eqdesc funs defnames ed
+      let ed, defnames = Hept_mapfold.eqdesc funs defnames ed in
+      ed, Env.empty
   | _ -> raise Errors.Fallback
 
 let funs = { Hept_mapfold.defaults with eqdesc = eqdesc; block = block; }
diff --git a/compiler/heptagon/transformations/inline.ml b/compiler/heptagon/transformations/inline.ml
index b303060..63e269d 100644
--- a/compiler/heptagon/transformations/inline.ml
+++ b/compiler/heptagon/transformations/inline.ml
@@ -36,7 +36,9 @@ open Heptagon
 open Hept_utils
 open Hept_mapfold
 
-let to_be_inlined s = !Compiler_options.flatten || (List.mem s !Compiler_options.inline)
+let to_be_inlined s =
+  (!Compiler_options.flatten && not (s.qual = Pervasives))
+  || (List.mem s !Compiler_options.inline)
 
 let fresh = Idents.gen_var "inline"