diff --git a/src/eksporti.ml b/src/eksporti.ml
index 9bd0066..d055a60 100644
--- a/src/eksporti.ml
+++ b/src/eksporti.ml
@@ -88,6 +88,4 @@ Available options for the selected mode:"
     Format.printf "%s\n" s;
     Arg.usage (Arg.align Cli.options) usage
   | e          ->
-    let module Denv = Api.Env.Default in
-    let module Derr = Api.Errors.Make(Denv) in
-    raise (Derr.graceful_fail None e)
+    raise Api.Env.(fail_env_error (dummy ()) Kernel.Basic.dloc e)
diff --git a/src/json/compile.ml b/src/json/compile.ml
index d695ff8..0de3748 100644
--- a/src/json/compile.ml
+++ b/src/json/compile.ml
@@ -5,7 +5,7 @@ open Console
 open Extras
 module B = Kernel.Basic
 module D = Api.Dep
-module E = Parsing.Entry
+module E = Parsers.Entry
 module T = Kernel.Term
 module Jt = Json_types
 
@@ -165,7 +165,7 @@ struct
       let art2exp (sys, pth) =
         let item =
           if List.mem_eq B.mident_eq mdl M.encoding then None else
-            Some(M.item_of_entry mdl e)
+            Some (M.item_of_entry denv mdl e)
         in
         let ext = List.assoc sys Systems.exts in
         let file =
@@ -173,7 +173,7 @@ struct
         in
         { Jt.system = Systems.to_string sys
         ; file
-        ; etype = Option.map (M.string_of_item sys) item }
+        ; etype = Option.map (M.string_of_item denv sys) item }
       in
       (* Add section to download Dedukti file *)
       let exp =
diff --git a/src/json/compile.mli b/src/json/compile.mli
index efad1db..94b73ab 100644
--- a/src/json/compile.mli
+++ b/src/json/compile.mli
@@ -1,5 +1,5 @@
 open Kernel
-open Parsing
+open Parsers
 
 val json_include : string ref
 (** Directory containing json files. Allows to read back already created json
diff --git a/src/json/makefile.ml b/src/json/makefile.ml
index 373ef1c..90291c4 100644
--- a/src/json/makefile.ml
+++ b/src/json/makefile.ml
@@ -26,8 +26,7 @@ let want : string list -> Key.t list =
     json files stemming from [ms]. *)
 let json : (DkTools.Mident.t -> DkTools.entry list pp) -> string ->
   (Key.t, Value.t) rule = fun pp_entries tg ->
-  let module E = Api.Env.Default in
-  let md = E.init Filename.(dirname tg </> !/tg <.> "dk") in
+  let md = DkTools.init Filename.(dirname tg </> !/tg <.> "dk") in
   let md_deps =
     Deps.deps_of_md md |> DkTools.MdSet.to_seq |> List.of_seq
   in
@@ -43,9 +42,10 @@ let json : (DkTools.Mident.t -> DkTools.entry list pp) -> string ->
     let ochan = open_out tg in
     let ofmt = Format.formatter_of_out_channel ochan in
     let entries =
-      let inchan = open_in (Api.Dep.get_file md) in
-      let r = Parsing.Parser.Parse_channel.parse md inchan in
-      close_in inchan;
+      let open Parsers.Parser in
+      let input = input_from_file (DkTools.get_file md) in
+      let r = parse input in
+      Parsers.Parser.close input;
       r
     in
     pp_entries ofmt entries;
diff --git a/src/middleware/midAgda.ml b/src/middleware/midAgda.ml
index 13e12e7..2dcabf8 100644
--- a/src/middleware/midAgda.ml
+++ b/src/middleware/midAgda.ml
@@ -1,6 +1,6 @@
 module B = Kernel.Basic
 module D = Api.Dep
-module E = Parsing.Entry
+module E = Parsers.Entry
 module R = Kernel.Rule
 module T = Kernel.Term
 module U = Core.Uri
@@ -12,7 +12,7 @@ type tx =
   | TxCons (** Constructor of a type *)
   | TxProj (** Projection *)
 
-type item = Parsing.Entry.entry
+type item = Parsers.Entry.entry
 
 exception IllTaxon
 (** Exception raised when reading an ill formed taxon. *)
diff --git a/src/middleware/midCtpicef.ml b/src/middleware/midCtpicef.ml
index 3831ef3..4eb45f6 100644
--- a/src/middleware/midCtpicef.ml
+++ b/src/middleware/midCtpicef.ml
@@ -1,7 +1,7 @@
 open Core
 module B = Kernel.Basic
 module D = Api.Dep
-module E = Parsing.Entry
+module E = Parsers.Entry
 module T = Kernel.Term
 module U = Uri
 
@@ -67,9 +67,9 @@ let label = function
 
 (* TODO: Define cic items, and how to print them on the website
    depending on the export system *)
-type item = Kernel.Basic.mident * Parsing.Entry.entry
-let item_of_entry md e = (md,e)
-let string_of_item target (md,e) = match target with
+type item = Kernel.Basic.mident * Parsers.Entry.entry
+let item_of_entry _ md e = (md,e)
+let string_of_item _ target (md,e) = match target with
   | Systems.Latex -> Ctpicef.Latex.export_to_string md e
   | sys -> Console.exit_with "Encoding ctpicef doesn't support target: %s"
              (Systems.to_string sys)
diff --git a/src/middleware/midCupicef.ml b/src/middleware/midCupicef.ml
index fec5629..feddfbb 100644
--- a/src/middleware/midCupicef.ml
+++ b/src/middleware/midCupicef.ml
@@ -1,7 +1,7 @@
 open Core
 module B = Kernel.Basic
 module D = Api.Dep
-module E = Parsing.Entry
+module E = Parsers.Entry
 module T = Kernel.Term
 module U = Uri
 
@@ -67,11 +67,11 @@ let label = function
 
 (* TODO: Define cic items, and how to print them on the website
    depending on the export system *)
-type item = Kernel.Basic.mident * Parsing.Entry.entry
-let item_of_entry  md e = (md,e)
-let string_of_item target (md,e) = match target with
+type item = Kernel.Basic.mident * Parsers.Entry.entry
+let item_of_entry _ md e = (md,e)
+let string_of_item _ target (md,e) = match target with
   | Systems.Latex -> Cupicef.Latex.export_to_string md e
   | sys -> Console.exit_with "Encoding cupicef doesn't support target: %s"
              (Systems.to_string sys)
 
-let get_exporter = Cupicef.Latex.get_exporter
+let get_exporter _ = Cupicef.Latex.get_exporter
diff --git a/src/middleware/midSttfa.ml b/src/middleware/midSttfa.ml
index ec364b3..5161ebe 100644
--- a/src/middleware/midSttfa.ml
+++ b/src/middleware/midSttfa.ml
@@ -1,6 +1,6 @@
 module B = Kernel.Basic
 module D = Api.Dep
-module E = Parsing.Entry
+module E = Parsers.Entry
 module T = Kernel.Term
 module U = Core.Uri
 
@@ -77,9 +77,9 @@ let label = function
   | TxDef -> ("body", Some("type_annotation"))
   | TxThm -> ("statement", None)
 
-let item_of_entry mident entry = Sttfa__Compile.compile_entry mident entry
+let item_of_entry denv mident entry = Sttfa__Compile.compile_entry denv mident entry
 
-let string_of_item target =
-  Sttfa.Exporter.export_to_system_as_string target
+let string_of_item denv target =
+  Sttfa.Exporter.export_to_system_as_string denv target
 
 let get_exporter = Sttfa.Exporter.get_sttfa_exporter
diff --git a/src/middleware/middleware.ml b/src/middleware/middleware.ml
index aaf0269..5d7d77b 100644
--- a/src/middleware/middleware.ml
+++ b/src/middleware/middleware.ml
@@ -27,7 +27,7 @@ module type S = sig
   val encoding : DkTools.Mident.t list
   (** List of modules that encode the theory. *)
 
-  val tx_of_entry : Parsing.Entry.entry -> tx option
+  val tx_of_entry : Parsers.Entry.entry -> tx option
   (** [tx_of_entry e] returns a taxon of an entry [e], if it is
       taxon-associated entry (ie. a declaration, not a command). *)
 
@@ -58,7 +58,7 @@ module type S = sig
   (** [label tx] returns labels for the fields {!Json_types.item.term} and
       {!Json_types.item.term_opt}. *)
 
-  val item_of_entry : DkTools.Mident.t -> DkTools.entry -> item
+  val item_of_entry : Api.Env.t -> DkTools.Mident.t -> DkTools.entry -> item
   (** [item_of_entry md entry] returns an item of the logic given an appropriate
       Dedukti entry [entry] of module [md]. *)
 
@@ -66,12 +66,12 @@ module type S = sig
       - Display the output of {!val:string_of_item} for all statements
       - Offer to download the whole file processed with {!val:get_exporter}. *)
 
-  val string_of_item : Systems.t -> item -> string
+  val string_of_item : Api.Env.t -> Systems.t -> item -> string
   (** [string_of_item system item] returns a string representation
       of [item] in the export system [system].
       This will be printed on the website in the export fields. *)
 
-  val get_exporter : Systems.t -> (module Export.S)
+  val get_exporter : Api.Env.t -> Systems.t -> (module Export.S)
   (** [get_exporter system] Generate an Exporter module to the given system.
       This allows to handle export through the Makefile system. *)
 end
@@ -90,8 +90,8 @@ struct
   let is_axiomatic _ = false
   let fields_of_def _ _ t = t,None
   let label _ = "dummy",None
-  let item_of_entry _ _ = ()
-  let string_of_item _ _ = "dummy"
+  let item_of_entry _ _ _ = ()
+  let string_of_item _ _ _ = "dummy"
   let get_exporter _ = assert false
 end
 
diff --git a/src/sttfa/compile.ml b/src/sttfa/compile.ml
index e6a3575..3d0b721 100644
--- a/src/sttfa/compile.ml
+++ b/src/sttfa/compile.ml
@@ -9,24 +9,24 @@ module CType  = Compile_type
 module CTerm  = Compile_term
 module CProof = Compile_proof
 module Term = Kernel.Term
-module Entry = Parsing.Entry
+module Entry = Parsers.Entry
 
 let log_sttfa = new_logger "stfc"
 let log_sttfa = log_sttfa.logger
 
-let compile_declaration name ty =
+let compile_declaration denv name ty =
   match ty with
   | Term.App (cst, a, []) when is_sttfa_const sttfa_etap cst ->
     (* Format.eprintf "[COMPILE] parameter: %a@." Pp.print_name name ; *)
-      let ty' = CType.compile_type empty_env a in
+      let ty' = CType.compile_type denv empty_env a in
       Parameter (of_name name, ty')
   | Term.App (cst, a, []) when is_sttfa_const sttfa_eta cst ->
     (* Format.eprintf "[COMPILE] parameter: %a@." Pp.print_name name ; *)
-      let ty' = CType.compile__type empty_env a in
+      let ty' = CType.compile__type denv empty_env a in
       Parameter (of_name name, Ty ty')
   | Term.App (cst, a, []) when is_sttfa_const sttfa_eps cst ->
     (* Format.eprintf "[COMPILE] axiom: %a@." Pp.print_name name ; *)
-      let te' = CTerm.compile_term empty_env a in
+      let te' = CTerm.compile_term denv empty_env a in
       Axiom (of_name name, te')
   | _ ->
     if Sttfadk.is_tyop ty then
@@ -36,53 +36,53 @@ let compile_declaration name ty =
       end
     else assert false
 
-let compile_definition name ty term =
+let compile_definition denv name ty term =
   match ty with
   | Term.App (cst, a, []) when is_sttfa_const sttfa_etap cst ->
-    Definition(of_name name, CType.compile_type empty_env a, CTerm.compile_term empty_env term)
+    Definition(of_name name, CType.compile_type denv empty_env a, CTerm.compile_term denv empty_env term)
   | Term.App (cst, a, []) when is_sttfa_const sttfa_eps cst ->
     (* The statement written and the one we get from the proof are beta,delta convertible. *)
-    let j, proof = CProof.compile_proof empty_env term in
-    let a' = CTerm.compile_term empty_env a in
+    let j, proof = CProof.compile_proof denv empty_env term in
+    let a' = CTerm.compile_term denv empty_env a in
     let proof' =
       if j.thm = a' then proof
       else
         Conv
           ( {j with thm=a'}
           , proof
-          , Sttfatyping.Tracer.annotate empty_env j.thm a'
+          , Sttfatyping.Tracer.annotate denv empty_env j.thm a'
           )
     in
-    Theorem (of_name name, CTerm.compile_term empty_env a, proof')
+    Theorem (of_name name, CTerm.compile_term denv empty_env a, proof')
   | _ ->
     if is_tyop ty then
       begin
         (* Format.eprintf "[COMPILE] typeop: %a@." Pp.print_name name ; *)
-        let vars,ty = CType.compile_type_definition empty_env term in
+        let vars,ty = CType.compile_type_definition denv empty_env term in
         TypeDef(of_name name, vars, ty)
       end
     else
       assert false
 
-let compile_entry : Basic.mident * Entry.entry -> item =
+let compile_entry denv : Basic.mident * Entry.entry -> item =
   fun (md, e) ->
-  let open Parsing.Entry in
-  let module Ev = Api.Env.Default in
+  let open Parsers.Entry in
+  let module Ev = Api.Env in
   let module Pp = Api.Pp.Default in
   match e with
   | Decl(l,id,sc,st,ty) ->
-    Ev.declare l id sc st ty;
+    Ev.declare denv l id sc st ty;
     log_sttfa ~lvl:6 "compiling decl [%a]" Pp.print_ident id;
-    compile_declaration (Basic.mk_name md id) ty
+    compile_declaration denv (Basic.mk_name md id) ty
   | Def(l,id,sc,f,Some ty,te) ->
-    Ev.define l id sc f te (Some ty);
+    Ev.define denv l id sc f te (Some ty);
     log_sttfa ~lvl:6 "compiling def [%a]" Pp.print_ident id;
-    compile_definition (Basic.mk_name md id) ty te
+    compile_definition denv (Basic.mk_name md id) ty te
   | Def(_)   -> exit_with "Definition without types are not supported"
   | Rules(_) -> exit_with "Rules are not part of the sttforall logic"
   | _        -> exit_with "Dedukti Commands are not supported"
 
 (** Memoized [compile_entry]. *)
-let compile_entry : Basic.mident -> Entry.entry -> item =
+let compile_entry denv : Basic.mident -> Entry.entry -> item =
   let eq (m, e) (m', e') = Kernel.Basic.mident_eq m m' && Stdlib.(=) e e' in
-  let f = memoize ~eq compile_entry in fun m e -> f (m, e)
+  let f = memoize ~eq (compile_entry denv) in fun m e -> f (m, e)
diff --git a/src/sttfa/compile_proof.ml b/src/sttfa/compile_proof.ml
index ca6f895..79f3adc 100644
--- a/src/sttfa/compile_proof.ml
+++ b/src/sttfa/compile_proof.ml
@@ -5,13 +5,13 @@ open Environ
 module CType = Compile_type
 module CTerm = Compile_term
 
-module Denv = Api.Env.Default
+module Env = Api.Env
 
 let make_judgment env hyp thm = {ty= env.ty; te= env.te; hyp; thm}
 
 let extract_te te = match te with Te _te -> _te | _ -> assert false
 
-let rec compile_proof env proof =
+let rec compile_proof denv env proof =
   match proof with
   | Term.DB (_, _, n) ->
       let var = get_dk_var env n in
@@ -20,14 +20,14 @@ let rec compile_proof env proof =
       (j, Assume(j,var))
   | Term.Lam (_, id, Some cst, _te) when is_sttfa_const sttfa_type cst ->
     let id = gen_fresh env [] id in
-    let jp, proof = compile_proof (add_ty_var_dk env id) _te in
+    let jp, proof = compile_proof denv (add_ty_var_dk env id) _te in
     let j = make_judgment env jp.hyp (ForallP (soi id, jp.thm)) in
     (j, ForallPI (j, proof, soi id))
   | Term.Lam (_, id, Some (Term.App (cst, _, _) as _ty), _te)
     when is_sttfa_const sttfa_etap cst || is_sttfa_const sttfa_eta cst ->
-      let _ty' = CType.compile_wrapped__type env _ty in
+      let _ty' = CType.compile_wrapped__type denv env _ty in
       let id = gen_fresh env [] id in
-      let jp, proof = compile_proof (add_te_var_dk env id _ty') _te in
+      let jp, proof = compile_proof denv (add_te_var_dk env id _ty') _te in
       let j =
         make_judgment env jp.hyp
           (Te (Forall (soi id, _ty', extract_te jp.thm)))
@@ -37,40 +37,40 @@ let rec compile_proof env proof =
     when is_sttfa_const sttfa_eps cst ->
     let remove_hyp _ = TeSet.filter (fun (id',_) ->
         if string_of_ident id=id' then false else true) in
-    let _te' = CTerm.compile_wrapped__term env _te in
-    let jp, proof = compile_proof (add_prf_ctx env (string_of_ident id) _te _te') prf in
+    let _te' = CTerm.compile_wrapped__term denv env _te in
+    let jp, proof = compile_proof denv (add_prf_ctx env (string_of_ident id) _te _te') prf in
     let j =
       make_judgment env (remove_hyp _te' jp.hyp)
         (Te (Impl (_te', extract_te jp.thm)))
     in
     (j, ImplI (j, proof, string_of_ident id))
   | Term.Const (lc, name) ->
-  let te = Denv.get_type lc name in
-  let te' = CTerm.compile_wrapped_term empty_env te in
+  let te = Env.get_type denv lc name in
+  let te' = CTerm.compile_wrapped_term denv empty_env te in
   let j = make_judgment env (TeSet.of_list env.prf) te' in
     (j, Lemma (of_name name, j))
   | Term.App (f, a, args) ->
-    let j,f' = compile_proof env f in
-    List.fold_left (fun (j,f') a ->compile_arg env j f' a) (j,f') (a::args)
+    let j,f' = compile_proof denv env f in
+    List.fold_left (fun (j,f') a ->compile_arg denv env j f' a) (j,f') (a::args)
   | _ -> assert false
 
-and compile_arg env j f' a =
-  let te = Sttfatyping.subst env f' a in
+and compile_arg denv env j f' a =
+  let te = Sttfatyping.subst denv env f' a in
   let j' = {j with thm = te} in
-  let j,f' = get_product env j f' in
+  let j,f' = get_product denv env j f' in
   match j.thm with
   | ForallP _ ->
-    let a' = CType.compile__type env a in
+    let a' = CType.compile__type denv env a in
     (j', ForallPE(j', f',a'))
   | Te Forall _ ->
-    let a' = CTerm.compile__term env a in
+    let a' = CTerm.compile__term denv env a in
     let proof = ForallE(j', f',a') in
-    let rws,after = Sttfatyping.Tracer.annotate_beta env j'.thm in
+    let rws,after = Sttfatyping.Tracer.annotate_beta denv env j'.thm in
     let trace = {left=rws; right = []} in
     let j' = {j with thm = after} in
     (j', Conv(j', proof, trace))
   | Te Impl(p',q') ->
-    let ja,a' = compile_proof env a in
+    let ja,a' = compile_proof denv env a in
     let _te = match ja.thm with Te _te -> _te | _ -> assert false in
     let inferred = Impl(p', q') in
     let expected = Impl(_te,q') in
@@ -78,19 +78,19 @@ and compile_arg env j f' a =
         (j', ImplE(j', f',a'))
     else
       begin
-        let trace = Sttfatyping.Tracer._annotate env inferred expected in
+        let trace = Sttfatyping.Tracer._annotate denv env inferred expected in
         let f' = Conv({j with thm = Te expected}, f', trace) in
         (j', ImplE(j',f',a'))
       end
   | Te _ -> assert false
 
-and get_product env j f' =
+and get_product denv env j f' =
   match j.thm with
   | ForallP _ | Te Forall _ | Te Impl _ -> (j,f')
   | Te tyfl ->
-    let _, ctx,redex = Sttfatyping.Tracer.get_app_redex true [] tyfl in
-    let tyfr = Sttfatyping.Tracer._reduce env ctx redex tyfl in
-    let trace = Sttfatyping.Tracer._annotate env tyfl tyfr in
+    let _, ctx,redex = Sttfatyping.Tracer.get_app_redex denv true [] tyfl in
+    let tyfr = Sttfatyping.Tracer._reduce denv env ctx redex tyfl in
+    let trace = Sttfatyping.Tracer._annotate denv env tyfl tyfr in
     let j' = {j with thm = Te tyfr} in
     let proof' = Conv(j',f',trace) in
-    get_product env j' proof'
+    get_product denv env j' proof'
diff --git a/src/sttfa/compile_term.ml b/src/sttfa/compile_term.ml
index add846d..1b88fad 100644
--- a/src/sttfa/compile_term.ml
+++ b/src/sttfa/compile_term.ml
@@ -4,55 +4,54 @@ open Environ
 
 module CType = Compile_type
 
-module Denv = Api.Env.Default
-module Derr = Api.Errors.Make(Denv)
+module Env = Api.Env
 module Dpp = Api.Pp.Default
 
 let rec type_arity_of te =
   match te with ForallK (_, te) -> 1 + type_arity_of te | _ -> 0
 
-let get_type_arity env lc name =
-  try type_arity_of (CType.compile_wrapped_type env (Denv.get_type lc name))
-  with e -> Derr.graceful_fail None e
+let get_type_arity denv env lc name =
+  try type_arity_of (CType.compile_wrapped_type denv env (Env.get_type denv lc name))
+  with e -> Env.fail_env_error denv Kernel.Basic.dloc e
 
 
-let rec compile__term env _te =
+let rec compile__term denv env _te =
   match _te with
   | Term.DB (_, _, n) ->
       let var = get_dk_var env n in
       TeVar var
   | Term.Lam (_, id, Some cst, _te) when is_sttfa_const sttfa_type cst ->
     let id = gen_fresh env [] id in
-      let _te' = compile__term (add_ty_var_dk env id) _te in
+      let _te' = compile__term denv (add_ty_var_dk env id) _te in
       AbsTy (soi id, _te')
   | Term.Lam (_, id, Some _ty, _te) ->
       let id = gen_fresh env [] id in
-      let _ty' = CType.compile_wrapped__type env _ty in
-      let _te' = compile__term (add_te_var_dk env id _ty') _te in
+      let _ty' = CType.compile_wrapped__type denv env _ty in
+      let _te' = compile__term denv (add_te_var_dk env id _ty') _te in
       Abs (soi id, _ty', _te')
   | Term.App (cst, _ty, [(Term.Lam (_, id, Some _, _te))])
     when is_sttfa_const sttfa_forall cst ->
       let id = gen_fresh env [] id in
-      let _ty' = CType.compile__type env _ty in
-      let _te' = compile__term (add_te_var_dk env id _ty') _te in
+      let _ty' = CType.compile__type denv env _ty in
+      let _te' = compile__term denv (add_te_var_dk env id _ty') _te in
       Forall (soi id, _ty', _te')
   | Term.App (cst, tel, [ter]) when is_sttfa_const sttfa_impl cst ->
-    let tel' = compile__term env tel in
-    let ter' = compile__term env ter in
+    let tel' = compile__term denv env tel in
+    let ter' = compile__term denv env ter in
     Impl (tel', ter')
   | Term.App (Term.Const (lc, name), a, args) ->
     let cst' = of_name name in
-    let i = get_type_arity env lc name in
+    let i = get_type_arity denv env lc name in
     let args = a :: args in
     let ty_args, te_args = (take i args, drop i args) in
-    let ty_args' = List.map (CType.compile__type env) ty_args in
-    let te_args' = List.map (fun x -> compile__term env x) te_args in
+    let ty_args' = List.map (CType.compile__type denv env) ty_args in
+    let te_args' = List.map (compile__term denv env) te_args in
     List.fold_left
       (fun app arg -> App (app, arg))
       (Cst (cst', ty_args')) te_args'
   | Term.App (f, a, args) ->
-    let f' = compile__term env f in
-      let args' = List.map (fun x -> compile__term env x) (a :: args) in
+    let f' = compile__term denv env f in
+      let args' = List.map (fun x -> compile__term denv env x) (a :: args) in
       List.fold_left (fun app arg -> App (app, arg)) f' args'
   | Term.Lam (_, _, None, _) -> failwith "lambda untyped are not supported"
   | Term.Const (_, cst) -> Cst (of_name cst, [])
@@ -60,25 +59,25 @@ let rec compile__term env _te =
       Format.eprintf "%a@." Dpp.print_term _te ;
       assert false
 
-let rec compile_term env te =
+let rec compile_term denv env te =
   match te with
   | Term.App (cst, Term.Lam (_, x, Some _, te), [])
     when is_sttfa_const sttfa_forall_kind_prop cst ->
     let x = gen_fresh env [] x in
-    let te' = compile_term (add_ty_var_dk env x) te in
+    let te' = compile_term denv (add_ty_var_dk env x) te in
     ForallP (soi x, te')
-  | _ ->  Te (compile__term env te)
+  | _ ->  Te (compile__term denv env te)
 
 
-let compile_wrapped_term env _te =
+let compile_wrapped_term denv env _te =
   match _te with
   | Term.App (cst, te, []) when is_sttfa_const sttfa_eps cst ->
-      compile_term env te
+      compile_term denv env te
   | _ -> assert false
 
 
-let compile_wrapped__term env _te =
+let compile_wrapped__term denv env _te =
   match _te with
   | Term.App (cst, te, []) when is_sttfa_const sttfa_eps cst ->
-      compile__term env te
+      compile__term denv env te
   | _ -> Format.eprintf "%a@." Dpp.print_term _te; assert false
diff --git a/src/sttfa/compile_type.ml b/src/sttfa/compile_type.ml
index e3351bb..377656e 100644
--- a/src/sttfa/compile_type.ml
+++ b/src/sttfa/compile_type.ml
@@ -2,7 +2,7 @@ open Sttfadk
 open Environ
 open Ast
 
-module Denv = Api.Env
+module Env = Api.Env
 module Dpp = Api.Pp.Default
 
 module Reduction = Kernel.Reduction
@@ -27,48 +27,48 @@ let rec compile__type env _ty =
   | Term.Const _ -> TyOp (compile_tyop _ty, [])
   | _ -> assert false
 
-let compile__type env _ty =
-  let _ty = Denv.reduction ~ctx:env.dk
+let compile__type denv env _ty =
+  let _ty = Env.reduction denv ~ctx:env.dk
       ~red:{Reduction.default_cfg with target=Reduction.Snf} _ty  in
   compile__type env _ty
 
-let rec compile_type (env: env) ty =
+let rec compile_type denv (env: env) ty =
   match ty with
   | Term.App (c, Term.Lam (_, var, _, ty), [])
     when is_sttfa_const sttfa_forall_kind_type c ->
     let var = gen_fresh env [] var in
-    let ty' = compile_type (add_ty_var_dk env var) ty in
+    let ty' = compile_type denv (add_ty_var_dk env var) ty in
     ForallK (soi var, ty')
   | Term.App (c, a, []) when is_sttfa_const sttfa_p c ->
-    Ty (compile__type env a)
+    Ty (compile__type denv env a)
   | _ -> assert false
 
-let compile_wrapped__type env (ty: Term.term) =
+let compile_wrapped__type denv env (ty: Term.term) =
   match ty with
   | Term.App (cst, Term.App (c, a, []), [])
     when is_sttfa_const sttfa_etap cst && is_sttfa_const sttfa_p c ->
-      compile__type env a
+      compile__type denv env a
   | Term.App (cst, a, []) when is_sttfa_const sttfa_eta cst ->
-      compile__type env a
+      compile__type denv env a
   | _ ->
       Format.eprintf "%a@." Dpp.print_term ty ;
       assert false
 
 
-let compile_wrapped_type env (ty: Term.term) =
+let compile_wrapped_type denv env (ty: Term.term) =
   match ty with
   | Term.App (cst, a, []) when is_sttfa_const sttfa_etap cst ->
-      compile_type env a
+      compile_type denv env a
   | Term.App (cst, a, []) when is_sttfa_const sttfa_eta cst ->
-      Ty (compile__type env a)
+      Ty (compile__type denv env a)
   | _ ->
       Format.eprintf "%a@." Dpp.print_term ty ;
       assert false
 
-let rec compile_type_definition env (ty: Term.term) =
+let rec compile_type_definition denv env (ty: Term.term) =
   match ty with
   | Term.Lam (_,x,_,ty) ->
-    compile_type_definition (add_ty_var_dk env x) ty
+    compile_type_definition denv (add_ty_var_dk env x) ty
   | _ ->
     let vars = env.ty in
-    (vars, compile__type env ty)
+    (vars, compile__type denv env ty)
diff --git a/src/sttfa/export/hollight.ml b/src/sttfa/export/hollight.ml
index 92e2668..42b2a99 100644
--- a/src/sttfa/export/hollight.ml
+++ b/src/sttfa/export/hollight.ml
@@ -3,7 +3,7 @@ open Compile
 open Holstt.HolSTT
 open Environ
 
-module Denv = Api.Env.Default
+module Env = Api.Env
 
 (* The memoization of Openstt is not efficient and can be highly increased. For that, the memoization of openstt should be turned off and the memoization should be done in this module. One may also want to handle alpha-renaming *)
 
@@ -39,7 +39,7 @@ let rec mk_ty = function
     mk_ty ty
   | Ty(_ty) -> mk__ty _ty
 
-let rec mk__te ctx conflicts avoid ?(total=false) =
+let rec mk__te denv ctx conflicts avoid ?(total=false) =
   (*let () = (if total then Printf.printf "Entering mk__te, total is true.\n") in*)
   function
   | TeVar(var) ->
@@ -60,31 +60,31 @@ let rec mk__te ctx conflicts avoid ?(total=false) =
       let ctx' = add_te_var ctx (string_of_ident new_var) _ty in
       let _ty' = mk__ty _ty in
       let new_var' = mk_var (mk_id false (string_of_ident new_var)) _ty' in
-      let _te' = mk__te ctx' ((var,string_of_ident new_var)::conflicts) avoid _te in
+      let _te' = mk__te denv ctx' ((var,string_of_ident new_var)::conflicts) avoid _te in
       mk_abs_term new_var' _te'
     else
       let ctx' = add_te_var ctx var _ty in
       let _ty' = mk__ty _ty in
       let var' = mk_var (mk_id false var) _ty' in
-      let _te' = mk__te ctx' conflicts avoid ~total:total _te in
+      let _te' = mk__te denv ctx' conflicts avoid ~total:total _te in
       mk_abs_term var' _te'
   | App(_tel,_ter) ->
-    let _tel' = mk__te ctx conflicts avoid ~total:total _tel in
-    let _ter' = mk__te ctx conflicts avoid ~total:total _ter in
+    let _tel' = mk__te denv ctx conflicts avoid ~total:total _tel in
+    let _ter' = mk__te denv ctx conflicts avoid ~total:total _ter in
     mk_app_term _tel' _ter'
   | Forall(var,_ty,_te) ->
     let _ty' = mk__ty _ty in
    (* let () = (if List.mem (mk_id var) avoid then Printf.printf "Conflict in a forall: variable %s\n" var
              else Printf.printf "No conflict: var %s not in %s\n" var (String.concat "," avoid)) in*)
-    let f' = mk__te ctx conflicts avoid (Abs(var,_ty,_te)) in
+    let f' = mk__te denv ctx conflicts avoid (Abs(var,_ty,_te)) in
     mk_forall_term f' _ty'
   | Impl(_tel,_ter) ->
-    let _tel' = mk__te ctx conflicts avoid ~total:total _tel in
-    let _ter' = mk__te ctx conflicts avoid ~total:total _ter in
+    let _tel' = mk__te denv ctx conflicts avoid ~total:total _tel in
+    let _ter' = mk__te denv ctx conflicts avoid ~total:total _ter in
     mk_impl_term _tel' _ter'
   | AbsTy(var, _te) ->
     let ctx' = add_ty_var ctx var in
-    mk__te ctx' conflicts avoid ~total:total _te
+    mk__te denv ctx' conflicts avoid ~total:total _te
   | Cst(cst, _tys) ->
     let open Basic in
     let name = name_of cst in
@@ -94,19 +94,19 @@ let rec mk__te ctx conflicts avoid ?(total=false) =
       | [] -> Term.mk_Const dloc name
       | x::t -> Term.mk_App (Term.mk_Const dloc name) x t
     in
-    let _ty = Denv.infer ~ctx:ctx.dk cst' in
-    let _ty' = CType.compile_wrapped__type ctx
-        (Denv.unsafe_reduction ~red:Conv.beta_only _ty) in
+    let _ty = Env.infer denv ~ctx:ctx.dk cst' in
+    let _ty' = CType.compile_wrapped__type denv ctx
+        (Env.unsafe_reduction denv ~red:Conv.beta_only _ty) in
     let cst'' = sanitize true (snd cst) in
     if total || not (Vars.is_empty (frees_ty _ty'))
     then mk_var_term (mk_var (sanitize true (snd(cst))) (mk__ty _ty'))
     else term_of_const (const_of_name cst'') (mk__ty _ty')
 
-let rec mk_te ctx avoid ?(total=false) = function
+let rec mk_te denv ctx avoid ?(total=false) = function
   | ForallP(var,te) ->
     let ctx' = add_ty_var ctx var in
-    mk_te ctx' avoid ~total:total te
-  | Te(_te) -> mk__te ctx [] avoid ~total:total _te
+    mk_te denv ctx' avoid ~total:total te
+  | Te(_te) -> mk__te denv ctx [] avoid ~total:total _te
 
 let rec app__te f ctx = function
   | ForallP(var,te) ->
@@ -118,18 +118,18 @@ let rec _ty_of_ty = function
     ForallK(_,t) -> _ty_of_ty t
   | Ty(t) -> t
 
-let thm_of_const cst =
+let thm_of_const denv cst =
   let cst_name = sanitize true (snd cst) in
   try
     thm_of_const_name cst_name
   with Failure _ ->
     let name = Environ.name_of cst in
     let term = Term.mk_Const Basic.dloc name in
-    let te = Denv.unsafe_reduction ~red:(Conv.delta name) (term) in
-    let te' = CTerm.compile_term Environ.empty_env te in
-    let te' = mk_te empty_env [] te' in
-    let ty = Denv.infer term in
-    let ty' = CType.compile_wrapped_type Environ.empty_env ty in
+    let te = Env.unsafe_reduction denv ~red:(Conv.delta name) (term) in
+    let te' = CTerm.compile_term denv Environ.empty_env te in
+    let te' = mk_te denv empty_env [] te' in
+    let ty = Env.infer denv term in
+    let ty' = CType.compile_wrapped_type denv Environ.empty_env ty in
     let ty' = mk_ty ty' in
     let const = const_of_name cst_name in
     let constterm = term_of_const const ty' in
@@ -173,8 +173,8 @@ let rec is_in_var ty = function
 let issue_tyvar u _ty =
   Vars.exists (fun tyvar -> not (is_in_var tyvar u)) (frees_ty _ty)
 
-let rec mk_proof env = function
-  | Assume(j,_) -> (mk_assume (mk_te env [] j.thm),Vars.empty)
+let rec mk_proof denv env = function
+  | Assume(j,_) -> (mk_assume (mk_te denv env [] j.thm),Vars.empty)
   | Lemma(cst,_) ->
     let thm_name = sanitize true (snd cst) in (Thm(thm_name),Vars.empty)
   | ForallE(_,proof, u) ->
@@ -185,11 +185,11 @@ let rec mk_proof env = function
        (* let () = Vars.iter (fun x -> Printf.printf "%s; " x) frees_u in*)
         (* let () = Printf.printf "\n" in*)
         (*let frees_ty = frees_ty _ty in*)
-        let u' = mk__te env [] [] u in
+        let u' = mk__te denv env [] [] u in
           (*(Vars.exists (fun tyvar -> not (is_in_var tyvar u')) frees_ty)*)
-        let u'' = if issue_tyvar u' _ty then mk__te env [] [] ~total:true u else u' in
+        let u'' = if issue_tyvar u' _ty then mk__te denv env [] [] ~total:true u else u' in
         let _ty' = mk__ty _ty in
-        let proof',pc = mk_proof env proof in
+        let proof',pc = mk_proof denv env proof in
         (mk_rule_elim_forall "" u'' proof',Vars.union frees_u pc)
       | _ -> assert false
     end
@@ -197,51 +197,51 @@ let rec mk_proof env = function
     let j' = judgment_of proof in
     let _,_ty = List.find (fun (x,_ty) -> x = var) j'.te in
     let env' = add_te_var env var _ty in
-    let proof',pc = mk_proof env' proof in
+    let proof',pc = mk_proof denv env' proof in
     let _ty' = mk__ty _ty in
     (mk_rule_intro_forall (mk_id false var) _ty' proof',pc)
   | ImplE(_,prfpq,prfp) ->
-    let prfp',pcp = mk_proof env prfp in
-    let prfpq',pcpq = mk_proof env prfpq in
+    let prfp',pcp = mk_proof denv env prfp in
+    let prfpq',pcpq = mk_proof denv env prfpq in
     (mk_rule_elim_impl prfpq' prfp',Vars.union pcp pcpq)
   | ImplI(_,proof,var) ->
     let j' = judgment_of proof in
     let _,p = TeSet.choose (TeSet.filter (fun (x,_ty) -> x = var) j'.hyp) in
     let env' = add_prf_ctx env var (Decompile.decompile__term env.dk p) p in
-    let p' = mk__te env [] [] p in
-    let proof',pc = mk_proof env' proof in
+    let p' = mk__te denv env [] [] p in
+    let proof',pc = mk_proof denv env' proof in
     (mk_rule_intro_impl p' proof',pc)
   | ForallPE(_,proof,_ty) ->
     begin
       match (judgment_of proof).thm with
       | ForallP(var,_) ->
         let subst = [(mk__ty (TyVar(mk_id false var)), mk__ty _ty)] in
-        let proof',pc = mk_proof env proof in
+        let proof',pc = mk_proof denv env proof in
         (mk_subst subst [] proof',pc)
       | _ -> assert false
     end
   | ForallPI(_,proof,var) ->
     let env' = add_ty_var env var in
-    mk_proof env' proof
+    mk_proof denv env' proof
   | Conv(j,proof,trace) ->
     let right = j.thm in
     let n1 = List.length trace.left in
     let n2 = List.length trace.right in
     let (n1',n2',proof') = depth_convs n1 n2 proof in
-    let proof'',pc = mk_proof env proof' in
+    let proof'',pc = mk_proof denv env proof' in
     if n1' = 0 && n2' = 0
     then
       proof'',pc
     else
       let avoid = Vars.elements pc in
-      let _ty = app__te Sttfatyping._infer env right in
-      let right' = mk_te env avoid right in
+      let _ty = app__te (Sttfatyping._infer denv) env right in
+      let right' = mk_te denv env avoid right in
       let right'' = if issue_tyvar right' _ty
-        then mk_te env avoid ~total:true right
+        then mk_te denv env avoid ~total:true right
         else right' in
       mk_conv "" right'' proof'',pc
 
-let print_item ?(short=false) =
+let print_item denv ?(short=false) =
   function
   | Parameter(cst,ty) ->
     begin
@@ -257,17 +257,17 @@ let print_item ?(short=false) =
     begin
       try
         (let cst' = sanitize true (snd cst) in
-         let te' = mk_te Environ.empty_env [] te in
+         let te' = mk_te denv Environ.empty_env [] te in
          let ty' = mk_ty ty in
          let eq = mk_equal_term (term_of_const (const_of_name cst') ty') te' ty' in
-         let Sequent(_,_,_,pi) = thm_of_const cst in
+         let Sequent(_,_,_,pi) = thm_of_const denv cst in
          if short
          then print_term false !oc eq
          else mk_thm cst' eq (mk_hyp []) (pi))
       with _ -> assert false
     end
   | Axiom(cst,te) ->
-    let te' = mk_te empty_env [] te in
+    let te' = mk_te denv empty_env [] te in
     let hyp = mk_hyp [] in
     let Sequent(_,_,_,pi) = mk_axiom (sanitize true (snd cst)) hyp te' in
     (* Axioms just have conclusions in STT and HOL Light *)
@@ -278,13 +278,13 @@ let print_item ?(short=false) =
   | Theorem(cst,te,proof) ->
     begin
       try
-        (let te' = mk_te empty_env [] te in
+        (let te' = mk_te denv empty_env [] te in
          let hyp' = mk_hyp [] in
          let cst' = sanitize true (snd cst) in
          if short
          then print_thm_debug !oc (Sequent(cst',hyp',te',dummy_proof))
          else
-           let proof',_ = mk_proof empty_env proof in
+           let proof',_ = mk_proof denv empty_env proof in
            mk_thm cst' te' hyp' proof')
       with _ -> assert false
     end
@@ -300,16 +300,16 @@ let print_item ?(short=false) =
 
 let content = ref ""
 
-let string_of_item item =
+let string_of_item denv item =
   let str_fmt = Format.str_formatter in
   set_oc str_fmt;
-  print_item ~short:true item;
+  print_item denv ~short:true item;
   Format.flush_str_formatter ()
 
-let print_ast : Format.formatter -> ?mdeps:Ast.mdeps -> Ast.ast -> unit = fun fmt ?mdeps:_ ast ->
+let print_ast denv : Format.formatter -> ?mdeps:Ast.mdeps -> Ast.ast -> unit = fun fmt ?mdeps:_ ast ->
   Buffer.clear Format.stdbuf;
   let oc_tmp = Format.str_formatter in
   set_oc oc_tmp;
-  List.iter (fun item -> print_item item) ast.items;
+  List.iter (fun item -> print_item denv item) ast.items;
   content := Buffer.contents Format.stdbuf;
   Format.fprintf fmt "%s" !content
diff --git a/src/sttfa/export/lean.ml b/src/sttfa/export/lean.ml
index ed991aa..3c2fbcc 100644
--- a/src/sttfa/export/lean.ml
+++ b/src/sttfa/export/lean.ml
@@ -2,7 +2,7 @@ module D = Core.Deps
 open Ast
 open Core.Extras
 
-module Denv = Api.Env.Default
+module Env = Api.Env
 module Basic = Kernel.Basic
 module Signature = Kernel.Signature
 
@@ -120,32 +120,32 @@ let rec is_prop ty =
   | Ty(_ty) -> is__prop _ty
   | ForallK(_,ty) -> is_prop ty
 
-let rec is__computable (_te:_te) =
+let rec is__computable denv (_te:_te) =
   match _te with
    | Ast.TeVar _ -> true
-   | Ast.Abs (_,_,_te) -> is__computable _te
-   | Ast.App (_tel,_ter) -> is__computable _tel && is__computable _ter
-   | Ast.Forall (_,_,_te) -> is__computable _te
-   | Ast.Impl (_tel,_ter) -> is__computable _tel && is__computable _ter
-   | Ast.AbsTy (_,_te) -> is__computable _te
+   | Ast.Abs (_,_,_te) -> is__computable denv _te
+   | Ast.App (_tel,_ter) -> is__computable denv _tel && is__computable denv _ter
+   | Ast.Forall (_,_,_te) -> is__computable denv _te
+   | Ast.Impl (_tel,_ter) -> is__computable denv _tel && is__computable denv _ter
+   | Ast.AbsTy (_,_te) -> is__computable denv _te
    | Ast.Cst ((cmd,cid),_) ->
      let open Basic in
      let name = mk_name (mk_mident cmd) (mk_ident cid) in
-     let ty = Denv.get_type dloc name in
-     let ty' = CType.compile_wrapped_type Environ.empty_env ty in
+     let ty = Env.get_type denv dloc name in
+     let ty' = CType.compile_wrapped_type denv Environ.empty_env ty in
      is_prop ty' ||
-       not @@ DkTools.is_static (Denv.get_signature ()) dloc name
+       not @@ DkTools.is_static (Env.get_signature denv) dloc name
 
-let rec is_computable te =
+let rec is_computable denv te =
   match te with
-  | Te(_te) -> is__computable _te
-  | ForallP(_,te) -> is_computable te
+  | Te(_te) -> is__computable denv _te
+  | ForallP(_,te) -> is_computable denv te
 
-let print_item oc = function
+let print_item denv oc = function
   | Parameter(name,ty) ->
     Format.fprintf oc "constant %a : %a.\n" print_name name print_ty ty
   | Definition(name,ty,te) ->
-    if is_prop ty || is_computable te then
+    if is_prop ty || is_computable denv te then
       Format.fprintf oc "def %a : %a := %a.\n" print_name name print_ty ty print_te te
     else
       Format.fprintf oc "noncomputable def %a : %a := %a.\n" print_name name print_ty ty print_te te
@@ -157,25 +157,25 @@ let print_item oc = function
     Format.fprintf oc "axiom %a : %a.\n" print_name tyop print_arity arity
   | TypeDef _ -> failwith "[Lean] Type definitions not handled right now"
 
-let print_ast : Format.formatter -> ?mdeps:Ast.mdeps -> Ast.ast -> unit = fun fmt ?mdeps:_ ast ->
+let print_ast denv : Format.formatter -> ?mdeps:Ast.mdeps -> Ast.ast -> unit = fun fmt ?mdeps:_ ast ->
   D.QSet.iter (print_dep fmt) ast.dep;
-  List.iter (print_item fmt) ast.items
+  List.iter (print_item denv fmt) ast.items
 
-let print_meta_ast fmt meta_ast =
+let print_meta_ast denv fmt meta_ast =
   let print_ast fmt ast =
     Format.fprintf fmt "namespace %s\n" ast.md;
-    print_ast fmt ast;
+    print_ast denv fmt ast;
     Format.fprintf fmt "end %s\n\n" ast.md
   in
   List.iter (print_ast fmt) meta_ast
 
 let to_string fmt = Format.asprintf "%a" fmt
 
-let string_of_item = function
+let string_of_item denv = function
   | Parameter((_,id),ty) ->
     Format.asprintf "constant %s : %a" id print_ty ty
   | Definition((_,id),ty,te) ->
-    if is_prop ty || is_computable te then
+    if is_prop ty || is_computable denv te then
       Format.asprintf "def %s : %a := %a" id print_ty ty print_te te
     else
       Format.asprintf "noncomputable def %s : %a := %a" id print_ty ty print_te te
diff --git a/src/sttfa/export/opentheory.ml b/src/sttfa/export/opentheory.ml
index d3fe7dd..c6fc6ad 100644
--- a/src/sttfa/export/opentheory.ml
+++ b/src/sttfa/export/opentheory.ml
@@ -3,7 +3,7 @@ open Compile
 open Openstt
 open Environ
 
-module Denv = Api.Env.Default
+module Env = Api.Env
 
 (* The memoization of Openstt is not efficient and can be highly increased. For that, the memoization of openstt should be turned off and the memoization should be done in this module. One may also want to handle alpha-renaming *)
 
@@ -51,7 +51,7 @@ let mk__ty =
         mk_def ty' !counter
       end
 *)
-let rec mk__te ctx = function
+let rec mk__te denv ctx = function
   | TeVar(var) ->
     let _ty = List.assoc var ctx.te in
     let _ty' = mk__ty _ty in
@@ -60,23 +60,23 @@ let rec mk__te ctx = function
     let ctx' = add_te_var ctx var _ty in
     let _ty' = mk__ty _ty in
     let var' = mk_var (mk_id var) _ty' in
-    let _te' = mk__te ctx' _te in
+    let _te' = mk__te denv ctx' _te in
     mk_abs_term var' _te'
   | App(_tel,_ter) ->
-    let _tel' = mk__te ctx _tel in
-    let _ter' = mk__te ctx _ter in
+    let _tel' = mk__te denv ctx _tel in
+    let _ter' = mk__te denv ctx _ter in
     mk_app_term _tel' _ter'
   | Forall(var,_ty,_te) ->
     let _ty' = mk__ty _ty in
-    let f' = mk__te ctx (Abs(var,_ty,_te)) in
+    let f' = mk__te denv ctx (Abs(var,_ty,_te)) in
     mk_forall_term f' _ty'
   | Impl(_tel,_ter) ->
-    let _tel' = mk__te ctx _tel in
-    let _ter' = mk__te ctx _ter in
+    let _tel' = mk__te denv ctx _tel in
+    let _ter' = mk__te denv ctx _ter in
     mk_impl_term _tel' _ter'
   | AbsTy(var, _te) ->
     let ctx' = add_ty_var ctx var in
-    mk__te ctx' _te
+    mk__te denv ctx' _te
   | Cst(cst, _tys) ->
     let open Basic in
     let name = name_of cst in
@@ -86,17 +86,17 @@ let rec mk__te ctx = function
       | [] -> Term.mk_Const dloc name
       | x::t -> Term.mk_App (Term.mk_Const dloc name) x t
     in
-    let _ty = Denv.infer ~ctx:ctx.dk cst' in
-    let _ty' = CType.compile_wrapped__type ctx
-        (Denv.unsafe_reduction ~red:Conv.beta_only _ty)
+    let _ty = Env.infer denv ~ctx:ctx.dk cst' in
+    let _ty' = CType.compile_wrapped__type denv ctx
+        (Env.unsafe_reduction denv ~red:Conv.beta_only _ty)
     in
     term_of_const (const_of_name (mk_qid cst)) (mk__ty _ty')
 
-let rec mk_te ctx = function
+let rec mk_te denv ctx = function
   | ForallP(var,te) ->
     let ctx' = add_ty_var ctx var in
-    mk_te ctx' te
-  | Te(_te) -> mk__te ctx _te
+    mk_te denv ctx' te
+  | Te(_te) -> mk__te denv ctx _te
 
 (* FIXME: buggy don't know why
 let memoization_te = Hashtbl.create 101
@@ -115,17 +115,17 @@ let mk__te =
         mk_def te' !counter
       end
 *)
-let thm_of_const cst =
+let thm_of_const denv cst =
   try
     thm_of_const_name (mk_qid cst)
   with Failure _ ->
     let name = Environ.name_of cst in
     let term = Term.mk_Const Basic.dloc name in
-    let te = Denv.unsafe_reduction ~red:(Conv.delta name) (term) in
-    let te' = CTerm.compile_term Environ.empty_env te in
-    let te' = mk_te empty_env te' in
-    let ty = Denv.infer term in
-    let ty' = CType.compile_wrapped_type Environ.empty_env ty in
+    let te = Env.unsafe_reduction denv ~red:(Conv.delta name) (term) in
+    let te' = CTerm.compile_term denv Environ.empty_env te in
+    let te' = mk_te denv empty_env te' in
+    let ty = Env.infer denv term in
+    let ty' = CType.compile_wrapped_type denv Environ.empty_env ty in
     let ty' = mk_ty ty' in
     let const = const_of_name (mk_qid cst) in
     let constterm = term_of_const const ty' in
@@ -143,35 +143,35 @@ let rec get_vars = function
   | Ty _ -> []
   | ForallK(var, ty) -> var::(get_vars ty)
 
-let mk_rewrite ctx r =
+let mk_rewrite denv ctx r =
   let open Basic in
   match r with
   | Beta(t) ->
-    let t' = mk__te ctx t in
+    let t' = mk__te denv ctx t in
     mk_betaConv t'
   | Delta((md,id),_tys) ->
     let cst = mk_name (mk_mident md) (mk_ident id) in
-    let ty = Denv.get_type dloc cst in
-    let ty' = CType.compile_type ctx ty in
+    let ty = Env.get_type denv dloc cst in
+    let ty' = CType.compile_type denv ctx ty in
     let vars = get_vars ty' in
     assert (List.length vars = List.length _tys);
     let vars' = List.map mk_id vars in
     let _tys' = List.map mk__ty _tys in
-    let thm = thm_of_const (md,id) in
+    let thm = thm_of_const denv (md,id) in
     mk_subst thm (List.combine vars' _tys') []
 
-let mk_beta env _te =
-  let _te' = mk__te env _te in
+let mk_beta denv env _te =
+  let _te' = mk__te denv env _te in
   mk_betaConv _te'
 
-let mk_delta ctx cst _tys =
+let mk_delta denv ctx cst _tys =
   let open Basic in
-  let thm = thm_of_const cst in
+  let thm = thm_of_const denv cst in
   let term =
     Term.mk_Const dloc (mk_name (mk_mident (fst cst)) (mk_ident (snd cst)))
   in
-  let ty = Denv.infer ~ctx:[] term in
-  let ty' = CType.compile_wrapped_type ctx ty in
+  let ty = Env.infer denv ~ctx:[] term in
+  let ty' = CType.compile_wrapped_type denv ctx ty in
   let vars = get_vars ty' in
   let vars' = List.map mk_id vars in
   let _tys' = List.map mk__ty _tys in
@@ -179,102 +179,102 @@ let mk_delta ctx cst _tys =
   let subst = List.combine vars' _tys' in
   mk_subst thm subst []
 
-let rec mk__ctx env thm ctx left right =
+let rec mk__ctx denv env thm ctx left right =
   match ctx,left,right with
   | [], _ , _-> thm
   | CAbsTy::ctx, AbsTy(_,_te), AbsTy(_,_te') ->
-    mk__ctx env thm ctx _te _te'
+    mk__ctx denv env thm ctx _te _te'
   | CAbs::ctx, Abs(var,_ty,_te), Abs(var',_ty',_te') ->
     assert (var = var');
     assert (_ty = _ty');
     let env' = add_te_var env var _ty in
     let var = mk_var (mk_id var) (mk__ty _ty) in
-    let thm = mk__ctx env' thm ctx _te _te' in
+    let thm = mk__ctx denv env' thm ctx _te _te' in
     mk_absThm var thm
   | CForall::ctx, Forall(var,_ty,_tel), Forall(var',_ty',_ter) ->
     assert (var = var');
     assert (_ty = _ty');
     let env' = add_te_var env var _ty in
-    let _tel' = mk__te env' _tel in
-    let _ter' = mk__te env' _ter in
-    let thm = mk__ctx env' thm ctx _tel _ter in
+    let _tel' = mk__te denv env' _tel in
+    let _ter' = mk__te denv env' _ter in
+    let thm = mk__ctx denv env' thm ctx _tel _ter in
     mk_forall_equal thm (mk_id var) _tel' _ter' (mk__ty _ty)
   | CAppL::ctx, App(_tel,_ter), App(_tel',_ter') ->
-    let thm = mk__ctx env thm ctx _tel _tel' in
-    mk_appThm thm (mk_refl (mk__te env _ter))
+    let thm = mk__ctx denv env thm ctx _tel _tel' in
+    mk_appThm thm (mk_refl (mk__te denv env _ter))
   | CAppR::ctx, App(_tel,_ter), App(_tel',_ter') ->
-    let thm = mk__ctx env thm ctx _ter _ter' in
-     mk_appThm (mk_refl (mk__te env _tel)) thm
+    let thm = mk__ctx denv env thm ctx _ter _ter' in
+     mk_appThm (mk_refl (mk__te denv env _tel)) thm
   | CImplL::ctx, Impl(_tel1, _ter1), Impl(_tel2, _ter2) ->
-    let _tel1' = mk__te env _tel1 in
-    let _ter1' = mk__te env _ter1 in
-    let _tel2' = mk__te env _tel2 in
-    let _ter2' = mk__te env _ter2 in
-    let thm = mk__ctx env thm ctx _tel1 _tel2 in
+    let _tel1' = mk__te denv env _tel1 in
+    let _ter1' = mk__te denv env _ter1 in
+    let _tel2' = mk__te denv env _tel2 in
+    let _ter2' = mk__te denv env _ter2 in
+    let thm = mk__ctx denv env thm ctx _tel1 _tel2 in
     mk_impl_equal thm (mk_refl _ter1') _tel1' _ter1' _tel2' _ter2'
   | CImplR::ctx, Impl(_tel1, _ter1), Impl(_tel2, _ter2) ->
-    let _tel1' = mk__te env _tel1 in
-    let _ter1' = mk__te env _ter1 in
-    let _tel2' = mk__te env _tel2 in
-    let _ter2' = mk__te env _ter2 in
-    let thm = mk__ctx env thm ctx _ter1 _ter2 in
+    let _tel1' = mk__te denv env _tel1 in
+    let _ter1' = mk__te denv env _ter1 in
+    let _tel2' = mk__te denv env _tel2 in
+    let _ter2' = mk__te denv env _ter2 in
+    let thm = mk__ctx denv env thm ctx _ter1 _ter2 in
     mk_impl_equal (mk_refl _tel1') thm _tel1' _ter1' _tel2' _ter2'
   | _ -> assert false
 
-let rec mk_ctx env thm ctx left right =
+let rec mk_ctx denv env thm ctx left right =
   match ctx, left,right with
   | CForallP::ctx, ForallP(var,_te) , ForallP(_,_te') ->
     let env' = add_ty_var env var in
-    let thm = mk_ctx env' thm ctx _te _te' in
+    let thm = mk_ctx denv env' thm ctx _te _te' in
     thm
-  | _, Te _te, Te _te' -> mk__ctx env thm ctx  _te _te'
+  | _, Te _te, Te _te' -> mk__ctx denv env thm ctx  _te _te'
   | _, _,_ -> assert false
 
-let mk_rewrite_step env term (redex,ctx) =
+let mk_rewrite_step denv env term (redex,ctx) =
   let env' = Sttfatyping.Tracer.env_of_redex env ctx term in
-  let term' = Sttfatyping.Tracer.reduce env' ctx redex term in
+  let term' = Sttfatyping.Tracer.reduce denv env' ctx redex term in
   let thm = match redex with
-    | Delta(name,_tys) -> mk_delta env' name _tys
-    | Beta(_te) -> mk_beta env' _te
+    | Delta(name,_tys) -> mk_delta denv env' name _tys
+    | Beta(_te) -> mk_beta denv env' _te
   in
-  let thm =  mk_ctx env thm ctx term term' in
+  let thm =  mk_ctx denv env thm ctx term term' in
   term',thm
 
-let mk_rewrite_seq env term rws =
+let mk_rewrite_seq denv env term rws =
   match rws with
-  | [] -> term, mk_refl (mk_te env term)
-  | [rw] ->  mk_rewrite_step env term rw
+  | [] -> term, mk_refl (mk_te denv env term)
+  | [rw] ->  mk_rewrite_step denv env term rw
   | rw::rws ->
-    let term',rw = mk_rewrite_step env term rw in
+    let term',rw = mk_rewrite_step denv env term rw in
     List.fold_left (fun (term,thm) rw ->
-        let term', thm' = (mk_rewrite_step env term rw) in
+        let term', thm' = (mk_rewrite_step denv env term rw) in
         term', mk_trans thm thm') (term',rw) rws
 
-let mk_trace env left right trace =
-  let _,thml = mk_rewrite_seq env left trace.left in
-  let _,thmr = mk_rewrite_seq env right trace.right in
+let mk_trace denv env left right trace =
+  let _,thml = mk_rewrite_seq denv env left trace.left in
+  let _,thmr = mk_rewrite_seq denv env right trace.right in
   let thmr' = mk_sym thmr in
   mk_trans thml thmr'
 
-let rec mk_proof env =
+let rec mk_proof denv env =
   let open Basic in
   function
-  | Assume(j,_) -> mk_assume (mk_te env j.thm)
+  | Assume(j,_) -> mk_assume (mk_te denv env j.thm)
   | Lemma(cst,_) ->
     begin
       try thm_of_lemma (mk_qid cst)
       with _ ->
-        let te = Denv.get_type dloc (name_of cst) in
-        mk_axiom (mk_hyp []) (mk_te empty_env (CTerm.compile_wrapped_term empty_env te))
+        let te = Env.get_type denv dloc (name_of cst) in
+        mk_axiom (mk_hyp []) (mk_te denv empty_env (CTerm.compile_wrapped_term denv empty_env te))
     end
   | ForallE(_,proof, u) ->
     begin
       match (judgment_of proof).thm with
       | Te(Forall(var,_ty,_te)) ->
-        let f' = mk__te env (Abs(var,_ty,_te)) in
-        let u' = mk__te env u in
+        let f' = mk__te denv env (Abs(var,_ty,_te)) in
+        let u' = mk__te denv env u in
         let _ty' = mk__ty _ty in
-        let proof' = mk_proof env proof in
+        let proof' = mk_proof denv env proof in
         mk_rule_elim_forall proof' f' _ty' u'
       | _ -> assert false
     end
@@ -282,50 +282,50 @@ let rec mk_proof env =
     let j' = judgment_of proof in
     let _,_ty = List.find (fun (x,_ty) -> if x = var then true else false) j'.te in
     let env' = add_te_var env var _ty in
-    let proof' = mk_proof env' proof in
+    let proof' = mk_proof denv env' proof in
     let _ty' = mk__ty _ty in
-    let thm' = mk_te env' j'.thm in
+    let thm' = mk_te denv env' j'.thm in
     mk_rule_intro_forall (mk_id var) _ty' thm' proof'
   | ImplE(j,prfpq,prfp) ->
     let p = (judgment_of prfp).thm in
     let q = j.thm in
-    let p' = mk_te env p in
-    let q' = mk_te env q in
-    let prfp' = mk_proof env prfp in
-    let prfpq' = mk_proof env prfpq in
+    let p' = mk_te denv env p in
+    let q' = mk_te denv env q in
+    let prfp' = mk_proof denv env prfp in
+    let prfpq' = mk_proof denv env prfpq in
     mk_rule_elim_impl prfp' prfpq' p' q'
   | ImplI(_,proof,var) ->
     let j' = judgment_of proof in
     let _,p = TeSet.choose (TeSet.filter (fun (x,_ty) -> if x = var then true else false) j'.hyp) in
     let q = j'.thm in
     let env' = add_prf_ctx env var (Decompile.decompile__term env.dk p) p in
-    let p' = mk__te env p in
-    let q' = mk_te env q in
-    let proof' = mk_proof env' proof in
+    let p' = mk__te denv env p in
+    let q' = mk_te denv env q in
+    let proof' = mk_proof denv env' proof in
     mk_rule_intro_impl proof' p' q'
   | ForallPE(_,proof,_ty) ->
     begin
       match (judgment_of proof).thm with
       | ForallP(var,_) ->
         let subst = [(mk_id var, mk__ty _ty)] in
-        let proof' = mk_proof env proof in
+        let proof' = mk_proof denv env proof in
         mk_subst proof' subst []
       | _ -> assert false
     end
   | ForallPI(_,proof,var) ->
     let env' = add_ty_var env var in
-    mk_proof env' proof
+    mk_proof denv env' proof
   | Conv(j,proof,trace) ->
     let right = j.thm in
     let left = (judgment_of proof).thm in
-    let proof = mk_proof env proof in
-    let mp = mk_eqMp proof (mk_trace env left right trace) in
+    let proof = mk_proof denv env proof in
+    let mp = mk_eqMp proof (mk_trace denv env left right trace) in
     mp
 
 let content = ref ""
 
 let string_of_item _ = "Printing for OpenTheory is not supported right now." (*
-  let print_item fmt = function
+  let print_item denv fmt = function
     | Parameter(name,ty) ->
       let ty' = mk_ty ty in
       let name' = mk_qid name in
@@ -334,14 +334,14 @@ let string_of_item _ = "Printing for OpenTheory is not supported right now." (*
       mk_thm name' eq (mk_hyp []) (mk_refl lhs)
     | Definition(cst,ty,te) ->
       let cst' = mk_qid cst in
-      let te' = mk_te Environ.empty_env te in
+      let te' = mk_te denv Environ.empty_env te in
       let ty' = mk_ty ty in
       let eq = mk_equal_term (term_of_const (const_of_name cst') ty') te' ty' in
-      let thm = thm_of_const cst in
+      let thm = thm_of_const denv cst in
       mk_thm cst' eq (mk_hyp []) thm
   | Theorem(cst,te,_)
   | Axiom(cst,te) ->
-    let te' = mk_te empty_env te in
+    let te' = mk_te denv empty_env te in
     let hyp = mk_hyp [] in
     mk_thm (mk_qid cst)  te' hyp (mk_axiom hyp te')
   | TyOpDef(tyop,arity) ->
@@ -358,7 +358,7 @@ let string_of_item _ = "Printing for OpenTheory is not supported right now." (*
   set_oc str_fmt;
   let length = Buffer.length Format.stdbuf in
   version ();
-  print_item str_fmt item;
+  print_item denv str_fmt item;
   clean ();
   let length' = Buffer.length Format.stdbuf in
   content := Buffer.sub Format.stdbuf length (length'-length);
@@ -366,36 +366,36 @@ let string_of_item _ = "Printing for OpenTheory is not supported right now." (*
   !content
 *)
 
-let print_item _ =
+let print_item denv _ =
   function
   | Parameter _ -> ()
   | Definition(cst,ty,te) ->
     (*    let te' = mk_te empty_env te in *)
     let cst' = mk_qid cst in
-    let te' = mk_te Environ.empty_env te in
+    let te' = mk_te denv Environ.empty_env te in
     let ty' = mk_ty ty in
     let eq = mk_equal_term (term_of_const (const_of_name cst') ty') te' ty' in
-    let thm = thm_of_const cst in
+    let thm = thm_of_const denv cst in
     mk_thm cst' eq (mk_hyp []) thm
   | Axiom(cst,te) ->
-    let te' = mk_te empty_env te in
+    let te' = mk_te denv empty_env te in
     let hyp = mk_hyp [] in
     mk_thm (mk_qid cst)  te' hyp (mk_axiom hyp te')
   | Theorem(cst,te,proof) ->
-    let te' = mk_te empty_env te in
+    let te' = mk_te denv empty_env te in
     let hyp' = mk_hyp [] in
-    let proof' = mk_proof empty_env proof in
+    let proof' = mk_proof denv empty_env proof in
     mk_thm (mk_qid cst) te' hyp' proof'
   | TypeDecl _ -> ()
   | TypeDef _ -> failwith "[OpenTheory] Type definitions not handled right now"
 
-let print_ast : Format.formatter -> ?mdeps:Ast.mdeps -> Ast.ast -> unit = fun fmt ?mdeps:_ ast ->
+let print_ast denv : Format.formatter -> ?mdeps:Ast.mdeps -> Ast.ast -> unit = fun fmt ?mdeps:_ ast ->
   Buffer.clear Format.stdbuf;
   reset ();
   let oc_tmp = Format.str_formatter in
   set_oc oc_tmp;
   version ();
-  List.iter (fun item -> print_item oc_tmp item) ast.items;
+  List.iter (fun item -> print_item denv oc_tmp item) ast.items;
   clean ();
   content := Buffer.contents Format.stdbuf;
   Format.fprintf fmt "%s" !content
diff --git a/src/sttfa/exporter.ml b/src/sttfa/exporter.ml
index 96418a3..088ce46 100644
--- a/src/sttfa/exporter.ml
+++ b/src/sttfa/exporter.ml
@@ -1,48 +1,48 @@
 module A = Ast
 module B = Kernel.Basic
 module D = Core.Deps
-module E = Parsing.Entry
-module Denv = Api.Env.Default
-module P = Parsing.Parser
+module E = Parsers.Entry
+module Env = Api.Env
+module P = Parsers.Parser
 open Core
 open Extras
 
-let export_to_system_as_string : Systems.t -> Ast.item -> string = fun sys ->
+let export_to_system_as_string denv : Systems.t -> Ast.item -> string = fun sys ->
   match sys with
   | Coq        -> Coq.string_of_item
   | Matita     -> Matita.string_of_item
   | OpenTheory -> Opentheory.string_of_item
-  | Lean       -> Lean.string_of_item
-  | Hollight   -> Hollight.string_of_item
+  | Lean       -> Lean.string_of_item denv
+  | Hollight   -> Hollight.string_of_item denv
   | Pvs        -> Pvs.string_of_item
   | _ -> assert false
 
-let export_to_system_as_ast : Systems.t -> Format.formatter ->
+let export_to_system_as_ast denv : Systems.t -> Format.formatter ->
   ?mdeps:A.mdeps -> Ast.ast -> unit = fun sys ->
   match sys with
   | Coq        -> Coq.print_ast
   | Matita     -> Matita.print_ast
-  | OpenTheory -> Opentheory.print_ast
-  | Lean       -> Lean.print_ast
-  | Hollight   -> Hollight.print_ast
+  | OpenTheory -> Opentheory.print_ast denv
+  | Lean       -> Lean.print_ast denv
+  | Hollight   -> Hollight.print_ast denv
   | Pvs        -> Pvs.print_ast
   | _ -> assert false
 
 (** [mk_ast md es] creates the STTfa ast of entries [es] from dedukti module
     [md] *)
-let mk_ast : B.mident -> E.entry list -> A.ast = fun md entries ->
-  let items = List.map (Compile.compile_entry md) entries in
+let mk_ast denv : B.mident -> E.entry list -> A.ast = fun md entries ->
+  let items = List.map (Compile.compile_entry denv md) entries in
   let fold_entry_dep dep e = D.QSet.union dep
       (D.dep_of_entry [Sttfadk.sttfa_module;md] e) in
   let dep = List.fold_left fold_entry_dep D.QSet.empty entries in
   { Ast.md = B.string_of_mident md; Ast.dep; items }
 
-let get_sttfa_exporter : Systems.t -> (module Export.S) = fun target ->
+let get_sttfa_exporter denv : Systems.t -> (module Export.S) = fun target ->
   (module struct
     type ast = Ast.ast
     let target = target
-    let compile = mk_ast
+    let compile = mk_ast denv
     let decompile _ = assert false
     let export : ast pp = fun fmt ast->
-      export_to_system_as_ast target fmt ast
+      export_to_system_as_ast denv target fmt ast
   end)
diff --git a/src/sttfa/exporter.mli b/src/sttfa/exporter.mli
index d236c7d..bc98b3e 100644
--- a/src/sttfa/exporter.mli
+++ b/src/sttfa/exporter.mli
@@ -3,8 +3,8 @@
 open Core
 
 (** Directly exports from STTfa to the given system as a string *)
-val export_to_system_as_string : Systems.t -> Ast.item -> string
+val export_to_system_as_string : Api.Env.t -> Systems.t -> Ast.item -> string
 
 (** Generate an Exporter module from STTfa to the given system.
     This allows to handle export through the Makefile system. *)
-val get_sttfa_exporter : Systems.t -> (module Export.S)
+val get_sttfa_exporter : Api.Env.t -> Systems.t -> (module Export.S)
diff --git a/src/sttfa/sttfatyping.ml b/src/sttfa/sttfatyping.ml
index f105a12..f9b66d4 100644
--- a/src/sttfa/sttfatyping.ml
+++ b/src/sttfa/sttfatyping.ml
@@ -3,8 +3,7 @@ open Ast
 open Kernel.Basic
 open Environ
 
-module Denv = Api.Env.Default
-module Derr = Api.Errors.Make(Denv)
+module Env = Api.Env
 module Dpp = Api.Pp.Default
 
 module Reduction = Kernel.Reduction
@@ -16,16 +15,16 @@ module Subst = Kernel.Subst
 module CType = Compile_type
 module CTerm = Compile_term
 
-let infer env _te =
+let infer denv env _te =
   let tedk = Decompile.decompile__term env.dk _te in
-  CType.compile_type env (Denv.infer ~ctx:env.dk tedk)
+  CType.compile_type denv env (Env.infer denv ~ctx:env.dk tedk)
 
-let _infer env _te =
+let _infer denv env _te =
   let tedk = Decompile.decompile__term env.dk _te in
-  let ty = Denv.infer ~ctx:env.dk tedk in
-  try CType.compile__type env ty
+  let ty = Env.infer denv ~ctx:env.dk tedk in
+  try CType.compile__type denv env ty
   with e ->
-    Derr.graceful_fail None e
+    Env.fail_env_error denv Kernel.Basic.dloc e
     (* Derr.fail_exit 1 "Inference fail" None (Some dloc)
      *   "Inference failed because type is polymorphic" ; *)
 
@@ -39,10 +38,10 @@ let eq env left right =
   let rightdk = Decompile.decompile_term env.dk right in
   Term.term_eq leftdk rightdk
 
-let are_convertible env left right =
+let are_convertible denv env left right =
   let leftdk = Decompile.decompile__term env.dk left in
   let rightdk = Decompile.decompile__term env.dk right in
-  Denv.are_convertible ~ctx:env.dk leftdk rightdk
+  Env.are_convertible denv ~ctx:env.dk leftdk rightdk
 
 let print__te env fmt _te =
   let _tedk = Decompile.decompile__term env.dk _te in
@@ -82,36 +81,36 @@ struct
 
 end
 
-let _is_beta_normal env _te =
+let _is_beta_normal denv env _te =
   let _tedk = Decompile.decompile__term env.dk _te in
-  let _tedk' = Denv.unsafe_reduction ~red:ComputeStrategy.beta_snf _tedk in
+  let _tedk' = Env.unsafe_reduction denv ~red:ComputeStrategy.beta_snf _tedk in
   Term.term_eq _tedk _tedk'
 
-let is_beta_normal env te =
+let is_beta_normal denv env te =
   let tedk = Decompile.decompile_term env.dk te in
-  let tedk' = Denv.unsafe_reduction ~red:ComputeStrategy.beta_snf tedk in
+  let tedk' = Env.unsafe_reduction denv ~red:ComputeStrategy.beta_snf tedk in
   Term.term_eq tedk tedk'
 
-let _beta_reduce env _te =
+let _beta_reduce denv env _te =
   let _tedk = Decompile.decompile__term env.dk _te in
-  let _tedk' = Denv.unsafe_reduction ~red:(ComputeStrategy.beta_steps 1) _tedk
+  let _tedk' = Env.unsafe_reduction denv ~red:(ComputeStrategy.beta_steps 1) _tedk
   in
-  CTerm.compile__term env _tedk'
+  CTerm.compile__term denv env _tedk'
 
-let beta_reduce env te =
+let beta_reduce denv env te =
   let tedk = Decompile.decompile_term env.dk te in
-  let tedk' = Denv.unsafe_reduction ~red:(ComputeStrategy.beta_steps 1) tedk in
-  CTerm.compile_term env tedk'
+  let tedk' = Env.unsafe_reduction denv ~red:(ComputeStrategy.beta_steps 1) tedk in
+  CTerm.compile_term denv env tedk'
 
-let beta_normal env te =
+let beta_normal denv env te =
   let tedk = Decompile.decompile_term env.dk te in
-  let tedk' = Denv.unsafe_reduction ~red:(ComputeStrategy.beta_snf) tedk in
-  CTerm.compile_term env tedk'
+  let tedk' = Env.unsafe_reduction denv ~red:(ComputeStrategy.beta_snf) tedk in
+  CTerm.compile_term denv env tedk'
 
-let subst env f a =
+let subst denv env f a =
   let thm = (judgment_of f).thm in
   let te = Decompile.to_eps (Decompile.decompile_term env.dk thm) in
-  let te = Denv.unsafe_reduction ~red:(ComputeStrategy.one_whnf) te in
+  let te = Env.unsafe_reduction denv ~red:(ComputeStrategy.one_whnf) te in
   let _,b = match te with
     | Term.Pi(_,_,tya,tyb) -> tya,tyb
     | _ -> assert false
@@ -122,8 +121,8 @@ let subst env f a =
     | Term.App(_, a, []) -> a
     | _ -> assert false
   in
-  let b' = Denv.unsafe_reduction ~red:(ComputeStrategy.beta_one) b' in
-  CTerm.compile_term env b'
+  let b' = Env.unsafe_reduction denv ~red:(ComputeStrategy.beta_one) b' in
+  CTerm.compile_term denv env b'
 
 (** This module aims to implement functions that trace reduction steps
     checking if two terms are convertible. *)
@@ -132,24 +131,24 @@ struct
 
   let fast = ref false
 
-  let is_defined cst =
+  let is_defined denv cst =
     let name = name_of cst in
-    not (DkTools.is_static (Denv.get_signature ()) dloc name)
+    not (DkTools.is_static (Env.get_signature denv) dloc name)
 
 
-  let rec is_redexable _te =
+  let rec is_redexable denv _te =
     match _te with
-    | Cst(cst, _) ->is_defined cst
+    | Cst(cst, _) -> is_defined denv cst
     | App(Abs _,_) -> true
-    | App(f,_) -> is_redexable f
+    | App(f,_) -> is_redexable denv f
     | _ ->  false
 
-  let rec get_app_redex side ctx tyf' =
+  let rec get_app_redex denv side ctx tyf' =
     match tyf' with
     | App(Abs _, _te) -> side, ctx, Beta(tyf')
-    | App (f, _)      -> get_app_redex side (CAppL::ctx) f
+    | App (f, _)      -> get_app_redex denv side (CAppL::ctx) f
     | Cst(cst, _tys)  ->
-      assert (is_defined cst);
+      assert (is_defined denv cst);
       side, ctx, Delta (cst, _tys)
     | _ -> assert false
 
@@ -201,40 +200,40 @@ struct
     let ctx,redex = _get_beta_redex env ctx term in
     List.rev ctx, redex
 
-  let rec _get_redex (envl,envr) ctx (left,right) =
+  let rec _get_redex denv (envl,envr) ctx (left,right) =
     (* Format.eprintf "left:%a@." (print__te envl) left;
     Format.eprintf "right:%a@." (print__te envr) right; *)
     match (left,right) with
     | TeVar _, TeVar _ -> raise Equal
     | Cst(cst,_tys), Cst(cst', _tys') ->
-      if is_defined cst then
-        if is_defined cst' then
+      if is_defined denv cst then
+        if is_defined denv cst' then
           if cst = cst' then
             raise Maybe
           else
             (true, ctx, Delta(cst, _tys))
         else
           (true, ctx, Delta(cst,_tys))
-      else if is_defined cst' then
+      else if is_defined denv cst' then
         (false, ctx, Delta(cst',_tys'))
       else
         raise Equal
-    | Cst (cst,_tys) , _ when is_defined cst ->
+    | Cst (cst,_tys) , _ when is_defined denv cst ->
       (true, ctx, Delta(cst, _tys))
-    | _ , Cst(cst,_tys) when is_defined cst ->
+    | _ , Cst(cst,_tys) when is_defined denv cst ->
       (false, ctx, Delta(cst, _tys))
     | Abs (var, _ty, _tel), Abs (var', _ty', _ter) ->
       let envl' = add_te_var envl var _ty in
       let envr' = add_te_var envr var' _ty' in
-      _get_redex (envl',envr') (CAbs::ctx) (_tel,_ter)
+      _get_redex denv (envl',envr') (CAbs::ctx) (_tel,_ter)
     | Forall (var, _ty, _tel), Forall (var', _ty', _ter) ->
       let envl' = add_te_var envl var _ty in
       let envr' = add_te_var envr var' _ty' in
-      _get_redex (envl',envr') (CForall::ctx) (_tel,_ter)
+      _get_redex denv (envl',envr') (CForall::ctx) (_tel,_ter)
     | Impl (_tel, _ter), Impl (_tel', _ter') ->
       begin
-        try _get_redex (envl,envr) (CImplL::ctx) (_tel,_tel')
-        with Equal | Maybe ->  _get_redex (envl,envr) (CImplR::ctx) (_ter,_ter')
+        try _get_redex denv (envl,envr) (CImplL::ctx) (_tel,_tel')
+        with Equal | Maybe ->  _get_redex denv (envl,envr) (CImplR::ctx) (_ter,_ter')
       end
     | App(Abs _, _), _ ->
       (true, ctx, Beta(left))
@@ -246,37 +245,37 @@ struct
       if Term.term_eq leftdk rightdk then
         raise Equal
       else
-      if is_redexable _tel then
-        get_app_redex true ctx left
-      else if is_redexable _tel' then
-        get_app_redex false ctx right
+      if is_redexable denv _tel then
+        get_app_redex denv true ctx left
+      else if is_redexable denv _tel' then
+        get_app_redex denv false ctx right
       else
         begin
           try
-            _get_redex (envl,envr) (CAppL::ctx) (_tel, _tel')
+            _get_redex denv (envl,envr) (CAppL::ctx) (_tel, _tel')
           with Equal ->
-            _get_redex (envl,envr) (CAppR::ctx) (_ter,_ter')
+            _get_redex denv (envl,envr) (CAppR::ctx) (_ter,_ter')
         end
     | App _ , _ ->
-      get_app_redex true ctx left
+      get_app_redex denv true ctx left
     | _, (App _) ->
-      get_app_redex false ctx right
+      get_app_redex denv false ctx right
     | _ -> assert false
 
-  let rec get_redex (envl,envr) ctx = function
-    | Te left, Te right -> _get_redex (envl,envr) ctx (left,right)
+  let rec get_redex denv (envl,envr) ctx = function
+    | Te left, Te right -> _get_redex denv (envl,envr) ctx (left,right)
     | ForallP(var,left), ForallP(var', right) ->
       let envl' = add_ty_var envl var in
       let envr' = add_ty_var envr var' in
-      get_redex (envl',envr') (CForallP::ctx) (left,right)
+      get_redex denv (envl',envr') (CForallP::ctx) (left,right)
     | _ -> assert false
 
-  let get_redex env ctx lr =
-    let is_left,ctx,redex = get_redex env ctx lr in
+  let get_redex denv env ctx lr =
+    let is_left,ctx,redex = get_redex denv env ctx lr in
     is_left, List.rev ctx, redex
 
-  let _get_redex env ctx lr =
-    let is_left,ctx,redex = _get_redex env ctx lr in
+  let _get_redex denv env ctx lr =
+    let is_left,ctx,redex = _get_redex denv env ctx lr in
     is_left, List.rev ctx, redex
 
   let rec _env_of_redex env ctx term =
@@ -323,32 +322,32 @@ struct
     | _, Te _te -> Te(_apply ctx newterm _te)
     | _ -> assert false
 
-  let newterm env _ redex =
+  let newterm denv env _ redex =
       match redex with
       | Beta(_te) ->
         let _tedk = Decompile.decompile__term env.dk _te in
-        CTerm.compile__term env
-          (Denv.unsafe_reduction ~red:ComputeStrategy.beta_one _tedk)
+        CTerm.compile__term denv env
+          (Env.unsafe_reduction denv ~red:ComputeStrategy.beta_one _tedk)
       | Delta(cst,_tys) ->
         let name = name_of cst in
         let _tedk = Decompile.decompile__term env.dk (Cst(cst,_tys)) in
         (* These two steps might be buggy in the future since we use
            SNF instead of WHNF because of the coercion eps *)
-        let _tedk' = Denv.unsafe_reduction ~red:(ComputeStrategy.delta name)
+        let _tedk' = Env.unsafe_reduction denv ~red:(ComputeStrategy.delta name)
             _tedk
         in
-        let _tedk' = Denv.unsafe_reduction
+        let _tedk' = Env.unsafe_reduction denv
             ~red:(ComputeStrategy.beta_steps (List.length _tys)) _tedk'
         in
-        CTerm.compile__term env _tedk'
+        CTerm.compile__term denv env _tedk'
 
-  let _reduce env ctx redex _te =
-    let newterm = newterm env ctx redex in
+  let _reduce denv env ctx redex _te =
+    let newterm = newterm denv env ctx redex in
     _apply ctx newterm _te
 
 
-  let reduce env ctx redex te =
-    let newterm = newterm env ctx redex in
+  let reduce denv env ctx redex te =
+    let newterm = newterm denv env ctx redex in
     apply ctx newterm te
 
   type 'a step =
@@ -360,72 +359,72 @@ struct
 
   let get_step is_left redex ctx = {is_left;redex;ctx}
 
-  let _one_step env left right =
-    let is_left,ctx,redex = _get_redex (env,env) [] (left,right) in
+  let _one_step denv env left right =
+    let is_left,ctx,redex = _get_redex denv (env,env) [] (left,right) in
     if is_left then
       let env' = _env_of_redex env ctx left in
-      let left' = _reduce env' ctx redex left in
+      let left' = _reduce denv env' ctx redex left in
       let step = get_step is_left redex ctx in
       step, left', right
     else
       let env' = _env_of_redex env ctx right in
-      let right' = _reduce env' ctx redex right in
+      let right' = _reduce denv env' ctx redex right in
       let step = get_step is_left redex ctx in
       step, left, right'
 
-  let one_step env left right =
-    let is_left,ctx,redex = get_redex (env,env) [] (left,right) in
+  let one_step denv env left right =
+    let is_left,ctx,redex = get_redex denv (env,env) [] (left,right) in
     if is_left then
       let env' = env_of_redex env ctx left in
-      let left' = reduce env' ctx redex left in
+      let left' = reduce denv env' ctx redex left in
       let step = get_step is_left redex ctx in
       step, left', right
     else
       let env' = env_of_redex env ctx right in
-      let right' = reduce env' ctx redex right in
+      let right' = reduce denv env' ctx redex right in
       let step = get_step is_left redex ctx in
       step, left, right'
 
   let empty_trace = {left= []; right = []}
 
-  let rec _annotate_beta env _te =
-    if _is_beta_normal env _te then
+  let rec _annotate_beta denv env _te =
+    if _is_beta_normal denv env _te then
       [], _te
     else
       let ctx,redex = _get_beta_redex env [] _te in
       let env' = _env_of_redex env ctx _te in
-      let _te' = _reduce env' ctx redex _te in
-      let trace, _tenf = _annotate_beta env _te' in
+      let _te' = _reduce denv env' ctx redex _te in
+      let trace, _tenf = _annotate_beta denv env _te' in
       (redex, ctx)::trace, _tenf
 
-  let rec annotate_beta env te =
-    if is_beta_normal env te then
+  let rec annotate_beta denv env te =
+    if is_beta_normal denv env te then
       [], te
     else
       let ctx,redex = get_beta_redex env [] te in
       let env' = env_of_redex env ctx te in
-      let te' = reduce env' ctx redex te in
-      let trace, tenf = annotate_beta env te' in
+      let te' = reduce denv env' ctx redex te in
+      let trace, tenf = annotate_beta denv env te' in
       (redex, ctx)::trace, tenf
 
-  let annotate_beta env te =
+  let annotate_beta denv env te =
     if !fast then
       [], te
     else
-      annotate_beta env te
+      annotate_beta denv env te
 
-  let rec _annotate env left right =
+  let rec _annotate denv env left right =
     if _eq env left right then
       empty_trace
     else
-      let tracel,left' = _annotate_beta env left in
-      let tracer, right' = _annotate_beta env right in
+      let tracel,left' = _annotate_beta denv env left in
+      let tracer, right' = _annotate_beta denv env right in
       let trace_beta = {left=tracel; right =tracer} in
       if _eq env left' right' then
         trace_beta
       else
-        let step, left', right' = _one_step env left' right' in
-        let trace' = _annotate env left' right' in
+        let step, left', right' = _one_step denv env left' right' in
+        let trace' = _annotate denv env left' right' in
         let trace'' =
           if step.is_left then
             {trace' with left=(step.redex, step.ctx)::trace'.left}
@@ -435,24 +434,24 @@ struct
         {left = trace_beta.left@trace''.left;
          right= trace_beta.right@trace''.right}
 
-  let _annotate env left right =
+  let _annotate denv env left right =
     if !fast then
       empty_trace
     else
-      _annotate env left right
+      _annotate denv env left right
 
-  let rec annotate env left right =
+  let rec annotate denv env left right =
     if eq env left right then
       empty_trace
     else
-      let tracel,left' = annotate_beta env left in
-      let tracer, right' = annotate_beta env right in
+      let tracel,left' = annotate_beta denv env left in
+      let tracer, right' = annotate_beta denv env right in
       let trace_beta = {left=tracel; right =tracer} in
       if eq env left' right' then
         trace_beta
       else
-        let step, left', right' = one_step env left' right' in
-        let trace' = annotate env left' right' in
+        let step, left', right' = one_step denv env left' right' in
+        let trace' = annotate denv env left' right' in
         let trace'' =
           if step.is_left then
             {trace' with left=(step.redex, step.ctx)::trace'.left}
@@ -462,9 +461,9 @@ struct
         {left = trace_beta.left@trace''.left;
          right= trace_beta.right@trace''.right}
 
-  let annotate env left right =
+  let annotate denv env left right =
     if !fast then
       empty_trace
     else
-      annotate env left right
+      annotate denv env left right
 end