diff --git a/gitlab-pages/docs/language-basics/maps-records.md b/gitlab-pages/docs/language-basics/maps-records.md
index 5c27f1395..81a26f1be 100644
--- a/gitlab-pages/docs/language-basics/maps-records.md
+++ b/gitlab-pages/docs/language-basics/maps-records.md
@@ -5,12 +5,12 @@ title: Records and Maps
 
 import Syntax from '@theme/Syntax';
 
-So far we have seen pretty basic data types. LIGO also offers more
+So far, we have seen pretty basic data types. LIGO also offers more
 complex built-in constructs, such as *records* and *maps*.
 
 ## Records
 
-Records are one way data of different types can be packed into a
+Records are one-way data of different types can be packed into a
 single type. A record is made of a set of *fields*, which are made of
 a *field name* and a *field type*. Given a value of a record type, the
 value bound to a field can be accessed by giving its field name to a
@@ -18,8 +18,6 @@ special operator (`.`).
 
 Let us first consider and example of record type declaration.
 
-
-
 <Syntax syntax="pascaligo">
 
 ```pascaligo group=records1
@@ -55,10 +53,8 @@ type user = {
 
 </Syntax>
 
-
 And here is how a record value is defined:
 
-
 <Syntax syntax="pascaligo">
 
 ```pascaligo group=records1
@@ -142,7 +138,7 @@ points on a plane.
 
 In PascaLIGO, the shape of that expression is
 `<record variable> with <record value>`.
-The record variable is the record to update and the
+The record variable is the record to update, and the
 record value is the update itself.
 
 ```pascaligo group=records2
@@ -160,13 +156,13 @@ following command of the shell:
 ```shell
 ligo run-function
 gitlab-pages/docs/language-basics/src/maps-records/record_update.ligo
-translate "(record [x=2;y=3;z=1], record [dx=3;dy=4])"
+xy_translate "(record [x=2;y=3;z=1], record [dx=3;dy=4])"
 # Outputs: {z = 1 , y = 7 , x = 5}
 ```
 
 You have to understand that `p` has not been changed by the functional
-update: a namless new version of it has been created and returned by
-the blockless function.
+update: a nameless new version of it has been created and returned by
+the block-less function.
 
 </Syntax>
 <Syntax syntax="cameligo">
@@ -186,6 +182,7 @@ let xy_translate (p, vec : point * vector) : point =
 
 You can call the function `xy_translate` defined above by running the
 following command of the shell:
+
 ```shell
 ligo run-function
 gitlab-pages/docs/language-basics/src/maps-records/record_update.mligo
@@ -218,6 +215,7 @@ let xy_translate = ((p, vec) : (point, vector)) : point =>
 
 You can call the function `xy_translate` defined above by running the
 following command of the shell:
+
 ```shell
 ligo run-function
 gitlab-pages/docs/language-basics/src/maps-records/record_update.religo
@@ -326,12 +324,21 @@ let change_color_preference = (account : account, color : color): account =>
 Note that all the records in the path will get updated. In this example that's
 `account` and `preferences`.
 
+You can call the function `change_color_preference` defined above by running the
+following command:
+
+```shell
+ligo run-function gitlab-pages/docs/language-basics/src/maps-records/record_nested_update.ligo 
+change_color_preference "(record [id=1001; preferences=record [color=Blue; other=1]], Green)"
+# Outputs: record[id -> 1001 , preferences -> record[color -> Green(unit) , other -> 1]]
+```
+
 <Syntax syntax="pascaligo">
 
 ### Record Patches
 
 Another way to understand what it means to update a record value is to
-make sure that any further reference to the value afterwards will
+make sure that any further reference to the value afterward will
 exhibit the modification. This is called a `patch` and this is only
 possible in PascaLIGO, because a patch is an *instruction*, therefore
 we can only use it in a block. Similarly to a *functional update*, a
@@ -355,6 +362,7 @@ function xy_translate (var p : point; const vec : vector) : point is
 
 You can call the function `xy_translate` defined above by running the
 following command of the shell:
+
 ```shell
 ligo run-function
 gitlab-pages/docs/language-basics/src/maps-records/record_patch.ligo
@@ -378,6 +386,7 @@ function xy_translate (var p : point; const vec : vector) : point is
 
 You can call the new function `xy_translate` defined above by running the
 following command of the shell:
+
 ```shell
 ligo run-function
 gitlab-pages/docs/language-basics/src/maps-records/record_patch2.ligo
@@ -401,6 +410,7 @@ function xy_translate (var p : point; const vec : vector) : point is
 
 You can call the new function `xy_translate` defined above by running the
 following command of the shell:
+
 ```shell
 ligo run-function
 gitlab-pages/docs/language-basics/src/maps-records/record_simu.ligo
@@ -425,8 +435,6 @@ sense.
 Here is how a custom map from addresses to a pair of integers is
 defined.
 
-
-
 <Syntax syntax="pascaligo">
 
 ```pascaligo group=maps
@@ -680,8 +688,8 @@ let assign = (m : register) : register =>
     (("tz1gjaF81ZRRvdzjobyfVNsAeSC6PScjfQwN" : address), Some ((4,9)), m);
 ```
 
-Notice the optional value `Some (4,9)` instead of `(4,9)`. If we had
-use `None` instead, that would have meant that the binding is removed.
+Notice the optional value `Some (4,9)` instead of `(4,9)`. If we used
+`None` instead that would have meant that the binding is removed.
 
 As a particular case, we can only add a key and its associated value.
 
@@ -693,7 +701,6 @@ let add = (m : register) : register =>
 
 </Syntax>
 
-
 To remove a binding from a map, we need its key.
 
 
@@ -748,8 +755,8 @@ There are three kinds of functional iterations over LIGO maps: the
 
 The first, the *iterated operation*, is an iteration over the map with
 no return value: its only use is to produce side-effects. This can be
-useful if for example you would like to check that each value inside
-of a map is within a certain range, and fail with an error otherwise.
+useful if, for example you would like to check that each value inside
+of a map is within a certain range and fail with an error otherwise.
 
 The predefined functional iterator implementing the iterated operation
 over maps is called `Map.iter`. In the following example, the register
@@ -985,7 +992,7 @@ let moves : register =
     (("tz1gjaF81ZRRvdzjobyfVNsAeSC6PScjfQwN" : address), (0,3))]
 ```
 
-The predefind function `Big_map.literal` constructs a big map from a
+The predefined function `Big_map.literal` constructs a big map from a
 list of key-value pairs `(<key>, <value>)`. Note also the semicolon
 separating individual map entries.  The annotated value `("<string>
 value>" : address)` means that we cast a string into an address.
@@ -1000,7 +1007,7 @@ let moves : register =
     ("tz1gjaF81ZRRvdzjobyfVNsAeSC6PScjfQwN" : address, (0,3))]);
 ```
 
-The predefind function `Big_map.literal` constructs a big map from a
+The predefined function `Big_map.literal` constructs a big map from a
 list of key-value pairs `(<key>, <value>)`. Note also the semicolon
 separating individual map entries.  The annotated value `("<string>
 value>" : address)` means that we cast a string into an address.
diff --git a/src/bin/cli.ml b/src/bin/cli.ml
index c8da92924..8c3720042 100644
--- a/src/bin/cli.ml
+++ b/src/bin/cli.ml
@@ -275,7 +275,7 @@ let compile_parameter =
     let%bind typed_prg,state = Compile.Utils.type_file source_file syntax (Contract entry_point) in
     let%bind mini_c_prg      = Compile.Of_typed.compile typed_prg in
     let%bind michelson_prg   = Compile.Of_mini_c.aggregate_and_compile_contract mini_c_prg entry_point in
-    let      env             = Ast_typed.program_environment typed_prg in
+    let      env             = Ast_typed.program_environment Environment.default typed_prg in
     let%bind (_contract: Tezos_utils.Michelson.michelson) =
       (* fails if the given entry point is not a valid contract *)
       Compile.Of_michelson.build_contract michelson_prg in
@@ -302,7 +302,7 @@ let interpret =
       | Some init_file ->
         let%bind typed_prg,state = Compile.Utils.type_file init_file syntax Env in
         let%bind mini_c_prg      = Compile.Of_typed.compile typed_prg in
-        let      env             = Ast_typed.program_environment typed_prg in
+        let      env             = Ast_typed.program_environment Environment.default typed_prg in
         ok (mini_c_prg,state,env)
       | None -> ok ([],Typer.Solver.initial_state,Environment.default) in
 
@@ -344,7 +344,7 @@ let compile_storage =
     let%bind typed_prg,state = Compile.Utils.type_file source_file syntax (Contract entry_point) in
     let%bind mini_c_prg      = Compile.Of_typed.compile typed_prg in
     let%bind michelson_prg   = Compile.Of_mini_c.aggregate_and_compile_contract mini_c_prg entry_point in
-    let      env             = Ast_typed.program_environment typed_prg in
+    let      env             = Ast_typed.program_environment Environment.default typed_prg in
     let%bind (_contract: Tezos_utils.Michelson.michelson) =
       (* fails if the given entry point is not a valid contract *)
       Compile.Of_michelson.build_contract michelson_prg in
@@ -368,7 +368,7 @@ let dry_run =
   let f source_file entry_point storage input amount balance sender source predecessor_timestamp syntax display_format =
     toplevel ~display_format @@
     let%bind typed_prg,state = Compile.Utils.type_file source_file syntax (Contract entry_point) in
-    let      env             = Ast_typed.program_environment typed_prg in
+    let      env             = Ast_typed.program_environment Environment.default typed_prg in
     let%bind mini_c_prg      = Compile.Of_typed.compile typed_prg in
     let%bind michelson_prg   = Compile.Of_mini_c.aggregate_and_compile_contract mini_c_prg entry_point in
     let%bind (_contract: Tezos_utils.Michelson.michelson) =
@@ -398,7 +398,7 @@ let run_function =
   let f source_file entry_point parameter amount balance sender source predecessor_timestamp syntax display_format =
     toplevel ~display_format @@
     let%bind typed_prg,state = Compile.Utils.type_file source_file syntax Env in
-    let      env             = Ast_typed.program_environment typed_prg in
+    let      env             = Ast_typed.program_environment Environment.default typed_prg in
     let%bind mini_c_prg      = Compile.Of_typed.compile typed_prg in
 
 
diff --git a/src/bin/expect_tests/michelson_converter.ml b/src/bin/expect_tests/michelson_converter.ml
index f1437f44f..b8a6cd90e 100644
--- a/src/bin/expect_tests/michelson_converter.ml
+++ b/src/bin/expect_tests/michelson_converter.ml
@@ -202,4 +202,121 @@ let%expect_test _ =
              IF_LEFT
                { DUP ; CDR ; NIL operation ; PAIR ; DIP { DROP } }
                { DUP ; CDR ; NIL operation ; PAIR ; DIP { DROP } } ;
+             DIP { DROP 2 } } } |}]
+
+let%expect_test _ =
+  run_ligo_good [ "compile-contract" ; (contract "double_fold_converter.religo") ; "main" ] ;
+  [%expect {|
+    { parameter
+        (list (pair (address %from_)
+                    (list %txs (pair (address %to_) (pair (nat %token_id) (nat %amount)))))) ;
+      storage (big_map nat address) ;
+      code { DUP ;
+             CDR ;
+             DIG 1 ;
+             DUP ;
+             DUG 2 ;
+             CAR ;
+             ITER { SWAP ;
+                    PAIR ;
+                    DUP ;
+                    CDR ;
+                    DUP ;
+                    CAR ;
+                    SENDER ;
+                    DIG 1 ;
+                    DUP ;
+                    DUG 2 ;
+                    COMPARE ;
+                    NEQ ;
+                    IF { PUSH string "NOT_OWNER" ; FAILWITH } { PUSH unit Unit } ;
+                    DIG 1 ;
+                    DUP ;
+                    DUG 2 ;
+                    DIG 4 ;
+                    DUP ;
+                    DUG 5 ;
+                    CAR ;
+                    PAIR ;
+                    DIG 3 ;
+                    DUP ;
+                    DUG 4 ;
+                    CDR ;
+                    ITER { SWAP ;
+                           PAIR ;
+                           DUP ;
+                           CAR ;
+                           DIG 1 ;
+                           DUP ;
+                           DUG 2 ;
+                           CDR ;
+                           DIG 1 ;
+                           DUP ;
+                           DUG 2 ;
+                           CAR ;
+                           DIG 2 ;
+                           DUP ;
+                           DUG 3 ;
+                           CDR ;
+                           DIG 2 ;
+                           DUP ;
+                           DUG 3 ;
+                           CDR ;
+                           CAR ;
+                           DIG 3 ;
+                           DUP ;
+                           DUG 4 ;
+                           CAR ;
+                           DIG 4 ;
+                           DUP ;
+                           DUG 5 ;
+                           CDR ;
+                           CDR ;
+                           PAIR ;
+                           PAIR ;
+                           DIG 2 ;
+                           DUP ;
+                           DUG 3 ;
+                           DIG 1 ;
+                           DUP ;
+                           DUG 2 ;
+                           CDR ;
+                           GET ;
+                           IF_NONE
+                             { PUSH string "TOKEN_UNDEFINED" ; FAILWITH }
+                             { DIG 2 ;
+                               DUP ;
+                               DUG 3 ;
+                               DIG 1 ;
+                               DUP ;
+                               DUG 2 ;
+                               COMPARE ;
+                               EQ ;
+                               IF { DUP } { PUSH string "INSUFFICIENT_BALANCE" ; FAILWITH } ;
+                               DIP { DROP } } ;
+                           DIG 2 ;
+                           DUP ;
+                           DUG 3 ;
+                           DIG 4 ;
+                           DUP ;
+                           DUG 5 ;
+                           DIG 3 ;
+                           DUP ;
+                           DUG 4 ;
+                           CAR ;
+                           CDR ;
+                           SOME ;
+                           DIG 4 ;
+                           DUP ;
+                           DUG 5 ;
+                           CDR ;
+                           UPDATE ;
+                           PAIR ;
+                           DIP { DROP 7 } } ;
+                    DUP ;
+                    CAR ;
+                    DIP { DROP 5 } } ;
+             DUP ;
+             NIL operation ;
+             PAIR ;
              DIP { DROP 2 } } } |}]
\ No newline at end of file
diff --git a/src/environment/bool.ml b/src/environment/bool.ml
index 611c84dfd..d3fea07eb 100644
--- a/src/environment/bool.ml
+++ b/src/environment/bool.ml
@@ -1,4 +1,8 @@
 open Ast_typed
 open Stage_common.Constant
 
-let environment = env_sum_type ~type_name:t_bool @@ [(Constructor "true",{ctor_type=t_unit ();michelson_annotation=None;ctor_decl_pos=0});(Constructor "false",{ctor_type=t_unit ();michelson_annotation=None;ctor_decl_pos=1})]
+let environment = Ast_typed.Environment.add_ez_sum_type ~type_name:t_bool @@ 
+  [
+    (Constructor "true" ,{ctor_type=t_unit ();michelson_annotation=None;ctor_decl_pos=0});
+    (Constructor "false",{ctor_type=t_unit ();michelson_annotation=None;ctor_decl_pos=1});
+  ]
diff --git a/src/passes/10-interpreter/interpreter.ml b/src/passes/10-interpreter/interpreter.ml
index c76b464f7..31867602b 100644
--- a/src/passes/10-interpreter/interpreter.ml
+++ b/src/passes/10-interpreter/interpreter.ml
@@ -368,19 +368,23 @@ and eval : Ast_typed.expression -> env -> value result
 
 let dummy : Ast_typed.program -> string result =
   fun prg ->
-    let%bind (res,_) = bind_fold_list
-      (fun (pp,top_env) el ->
-        let (Ast_typed.Declaration_constant {binder; expr ; inline=_ ; _}) = Location.unwrap el in
-        let%bind v =
-        (*TODO This TRY-CATCH is here until we properly implement effects*)
-        try
-          eval expr top_env
-        with Temporary_hack s -> ok @@ V_Failure s
-        (*TODO This TRY-CATCH is here until we properly implement effects*)
-        in
-        let pp' = pp^"\n val "^(Var.to_name binder)^" = "^(Ligo_interpreter.PP.pp_value v) in
-        let top_env' = Env.extend top_env (binder, v) in
-        ok @@ (pp',top_env')
-      )
+  let aux  (pp,top_env) el =
+    match Location.unwrap el with
+    | Ast_typed.Declaration_constant {binder; expr ; inline=_ ; _} ->
+       let%bind v =
+         (*TODO This TRY-CATCH is here until we properly implement effects*)
+         try
+           eval expr top_env
+         with Temporary_hack s ->
+           ok (V_Failure s)
+              (*TODO This TRY-CATCH is here until we properly implement effects*)
+       in
+    let pp' = pp^"\n val "^(Var.to_name binder)^" = "^(Ligo_interpreter.PP.pp_value v) in
+    let top_env' = Env.extend top_env (binder, v) in
+    ok @@ (pp',top_env')
+    | Ast_typed.Declaration_type _ ->
+       ok (pp , top_env)
+  in
+  let%bind (res,_) = bind_fold_list aux
       ("",Env.empty_env) prg in
     ok @@ res
diff --git a/src/passes/10-transpiler/transpiler.ml b/src/passes/10-transpiler/transpiler.ml
index 9c1973f0d..5ea4ea43f 100644
--- a/src/passes/10-transpiler/transpiler.ml
+++ b/src/passes/10-transpiler/transpiler.ml
@@ -42,14 +42,6 @@ them. please report this to the developers." in
       ] in
     error ~data title content
 
-  let unsupported_iterator location =
-    let title () = "unsupported iterator" in
-    let content () = "only lambda are supported as iterators" in
-    let data = [
-        row_loc location ;
-      ] in
-    error ~data title content
-
   let not_functional_main location =
     let title () = "not functional main" in
     let content () = "main should be a function" in
@@ -382,9 +374,6 @@ let rec transpile_literal : AST.literal -> value = fun l -> match l with
   | Literal_unit -> D_unit
   | Literal_void -> D_none
 
-and transpile_environment_element_type : AST.environment_element -> type_expression result = fun ele ->
-  transpile_type ele.type_value
-
 and tree_of_sum : AST.type_expression -> (AST.constructor' * AST.type_expression) Append_tree.t result = fun t ->
   let%bind map_tv = get_t_sum t in
   let kt_list = List.map (fun (k,({ctor_type;_}:AST.ctor_content)) -> (k,ctor_type)) (kv_list_of_cmap map_tv) in
@@ -405,11 +394,7 @@ and transpile_annotated_expression (ae:AST.expression) : expression result =
     return (E_let_in ((let_binder, rhs'.type_expression), inline, rhs', result'))
   | E_literal l -> return @@ E_literal (transpile_literal l)
   | E_variable name -> (
-      let%bind ele =
-        trace_option (corner_case ~loc:__LOC__ "name not in environment") @@
-        AST.Environment.get_opt name ae.environment in
-      let%bind tv = transpile_environment_element_type ele in
-      return ~tv @@ E_variable (name)
+      return @@ E_variable (name)
     )
   | E_application {lamb; args} ->
       let%bind a = transpile_annotated_expression lamb in
@@ -449,7 +434,6 @@ and transpile_annotated_expression (ae:AST.expression) : expression result =
       return ~tv ae
     )
   | E_record m -> (
-    (*list_of_lmap to record_to_list*)
       let node = Append_tree.of_list @@ Ast_typed.Helpers.list_of_record_or_tuple m in
       let aux a b : expression result =
         let%bind a = a in
@@ -511,28 +495,14 @@ and transpile_annotated_expression (ae:AST.expression) : expression result =
       return @@ E_record_update (record, path, update)
   | E_constant {cons_name=name; arguments=lst} -> (
       let iterator_generator iterator_name =
-        let lambda_to_iterator_body (f : AST.expression) (l : AST.lambda) =
-          let%bind body' = transpile_annotated_expression l.result in
-          let%bind (input , _) = AST.get_t_function f.type_expression in
-          let%bind input' = transpile_type input in
-          ok ((l.binder , input') , body')
-        in
         let expression_to_iterator_body (f : AST.expression) =
-          match f.expression_content with
-          | E_lambda l -> lambda_to_iterator_body f l
-          | E_variable v -> (
-              let%bind elt =
-                trace_option (corner_case ~loc:__LOC__ "missing var") @@
-                AST.Environment.get_opt v f.environment in
-              match elt.definition with
-              | ED_declaration { expr = f ; free_variables = _ } -> (
-                  match f.expression_content with
-                  | E_lambda l -> lambda_to_iterator_body f l
-                  | _ -> fail @@ unsupported_iterator f.location
-                )
-              | _ -> fail @@ unsupported_iterator f.location
-            )
-          | _ -> fail @@ unsupported_iterator f.location
+          let%bind (input , output) = AST.get_t_function f.type_expression in
+          let%bind f' = transpile_annotated_expression f in
+          let%bind input' = transpile_type input in
+          let%bind output' = transpile_type output in
+          let binder = Var.fresh ~name:"iterated" () in
+          let application = Mini_c.Combinators.e_application f' output' (Mini_c.Combinators.e_var binder input') in
+          ok ((binder , input'), application)
         in
         fun (lst : AST.expression list) -> match (lst , iterator_name) with
           | [f ; i] , C_ITER | [f ; i] , C_MAP -> (
@@ -781,25 +751,29 @@ and transpile_recursive {fun_name; fun_type; lambda} =
   let body = Expression.make (E_iterator (C_LOOP_LEFT, ((lambda.binder, loop_type),body), expr)) output_type in
   ok @@ Expression.make (E_closure {binder;body}) fun_type
 
-let transpile_declaration env (d:AST.declaration) : toplevel_statement result =
+let transpile_declaration env (d:AST.declaration) : toplevel_statement option result =
   match d with
-  | Declaration_constant { binder ; expr ; inline ; post_env=_ } ->
+  | Declaration_constant { binder ; expr ; inline } ->
       let%bind expression = transpile_annotated_expression expr in
       let tv = Combinators.Expression.get_type expression in
       let env' = Environment.add (binder, tv) env in
-      ok @@ ((binder, inline, expression), environment_wrap env env')
+      ok @@ Some ((binder, inline, expression), environment_wrap env env')
+  | _ -> ok None
 
 let transpile_program (lst : AST.program) : program result =
   let aux (prev:(toplevel_statement list * Environment.t) result) cur =
     let%bind (hds, env) = prev in
-    let%bind ((_, env') as cur') = transpile_declaration env cur in
-    ok (hds @ [ cur' ], env'.post_environment)
+    match%bind transpile_declaration env cur with
+    | Some ((_ , env')  as cur') -> ok (hds @ [ cur' ] , env'.post_environment)
+    | None -> ok (hds , env)
   in
   let%bind (statements, _) = List.fold_left aux (ok ([], Environment.empty)) (temp_unwrap_loc_list lst) in
   ok statements
 
 (* check whether the storage contains a big_map, if yes, check that
-  it appears on the left hand side of a pair *)
+  it appears on the left hand side of a pair 
+  TODO : checking should appears in check_pass.  
+*)
 let check_storage f ty loc : (anon_function * _) result =
   let rec aux (t:type_expression) on_big_map =
     match t.type_content with
diff --git a/src/passes/10-transpiler/untranspiler.ml b/src/passes/10-transpiler/untranspiler.ml
index a6864bff9..5f68cddd5 100644
--- a/src/passes/10-transpiler/untranspiler.ml
+++ b/src/passes/10-transpiler/untranspiler.ml
@@ -42,19 +42,19 @@ open Errors
 
 let rec untranspile (v : value) (t : AST.type_expression) : AST.expression result =
   let open! AST in
-  let return e = ok (make_a_e_empty e t) in
+  let return e = ok (make_e e t) in
   match t.type_content with
   | T_variable (name) when Var.equal name Stage_common.Constant.t_bool -> (
         let%bind b =
           trace_strong (wrong_mini_c_value "bool" v) @@
           get_bool v in
-        return (e_bool b Environment.empty)
+        return (e_bool b)
       )
   | t when (compare t (t_bool ()).type_content) = 0-> (
         let%bind b =
           trace_strong (wrong_mini_c_value "bool" v) @@
           get_bool v in
-        return (e_bool b Environment.empty)
+        return (e_bool b)
       )
   | T_constant type_constant -> (
     match type_constant with
@@ -152,10 +152,10 @@ let rec untranspile (v : value) (t : AST.type_expression) : AST.expression resul
           trace_strong (wrong_mini_c_value "option" v) @@
           get_option v in
         match opt with
-        | None -> ok (e_a_empty_none o)
+        | None -> ok (e_a_none o)
         | Some s ->
             let%bind s' = untranspile s o in
-            ok (e_a_empty_some s')
+            ok (e_a_some s')
       )
     | TC_map {k=k_ty;v=v_ty}-> (
         let%bind map =
diff --git a/src/passes/8-typer-new/typer.ml b/src/passes/8-typer-new/typer.ml
index 36fa997fe..13a7def62 100644
--- a/src/passes/8-typer-new/typer.ml
+++ b/src/passes/8-typer-new/typer.ml
@@ -29,7 +29,7 @@ let rec type_declaration env state : I.declaration -> (environment * O.typer_sta
         trace (constant_declaration_error binder expression tv'_opt) @@
         type_expression env state expression in
       let post_env = Environment.add_ez_declaration binder expr env in
-      ok (post_env, state' , Some (O.Declaration_constant { binder ; expr ; inline ; post_env} ))
+      ok (post_env, state' , Some (O.Declaration_constant { binder ; expr ; inline} ))
     )
 
 and type_match : environment -> O.typer_state -> O.type_expression -> I.matching_expr -> I.expression -> Location.t -> (O.matching_expr * O.typer_state) result =
@@ -196,7 +196,7 @@ and type_expression : environment -> O.typer_state -> ?tv_opt:O.type_expression
     let%bind new_state = aggregate_constraints state constraints in
     let tv = t_variable type_name () in
     let location = ae.location in
-    let expr' = make_e ~location expr tv e in
+    let expr' = make_e ~location expr tv in
     ok @@ (expr' , new_state) in
   let return_wrapped expr state (constraints , expr_type) = return expr state constraints expr_type in
   let main_error =
diff --git a/src/passes/8-typer-old/typer.ml b/src/passes/8-typer-old/typer.ml
index 17af76c00..ca2a123a7 100644
--- a/src/passes/8-typer-old/typer.ml
+++ b/src/passes/8-typer-old/typer.ml
@@ -494,27 +494,25 @@ let rec type_program (p:I.program) : (O.program * O.typer_state) result =
     let%bind ed' = (bind_map_location (type_declaration e (Solver.placeholder_for_state_of_new_typer ()))) d in
     let loc : 'a . 'a Location.wrap -> _ -> _ = fun x v -> Location.wrap ~loc:x.location v in
     let (e', _placeholder_for_state_of_new_typer , d') = Location.unwrap ed' in
-    match d' with
-    | None -> ok (e', acc)
-    | Some d' -> ok (e', loc ed' d' :: acc)
+    ok (e', loc ed' d' :: acc)
   in
   let%bind (_, lst) =
     trace (fun () -> program_error p ()) @@
     bind_fold_list aux (DEnv.default, []) p in
   ok @@ (List.rev lst , (Solver.placeholder_for_state_of_new_typer ()))
 
-and type_declaration env (_placeholder_for_state_of_new_typer : O.typer_state) : I.declaration -> (environment * O.typer_state * O.declaration option) result = function
-  | Declaration_type (type_name , type_expression) ->
-      let%bind tv = evaluate_type env type_expression in
-      let env' = Environment.add_type (type_name) tv env in
-      ok (env', (Solver.placeholder_for_state_of_new_typer ()) , None)
+and type_declaration env (_placeholder_for_state_of_new_typer : O.typer_state) : I.declaration -> (environment * O.typer_state * O.declaration) result = function
+  | Declaration_type (type_binder , type_expr) ->
+      let%bind tv = evaluate_type env type_expr in
+      let env' = Environment.add_type (type_binder) tv env in
+      ok (env', (Solver.placeholder_for_state_of_new_typer ()) , (O.Declaration_type { type_binder ; type_expr = tv } ))
   | Declaration_constant (binder , tv_opt , inline, expression) -> (
       let%bind tv'_opt = bind_map_option (evaluate_type env) tv_opt in
       let%bind expr =
         trace (constant_declaration_error binder expression tv'_opt) @@
         type_expression' ?tv_opt:tv'_opt env expression in
       let post_env = Environment.add_ez_declaration binder expr env in
-      ok (post_env, (Solver.placeholder_for_state_of_new_typer ()) , Some (O.Declaration_constant { binder ; expr ; inline ; post_env}))
+      ok (post_env, (Solver.placeholder_for_state_of_new_typer ()) , (O.Declaration_constant { binder ; expr ; inline}))
     )
 
 and type_match : (environment -> I.expression -> O.expression result) -> environment -> O.type_expression -> I.matching_expr -> I.expression -> Location.t -> O.matching_expr result =
@@ -674,6 +672,7 @@ and type_expression : environment -> O.typer_state -> ?tv_opt:O.type_expression
   = fun e _placeholder_for_state_of_new_typer ?tv_opt ae ->
     let%bind res = type_expression' e ?tv_opt ae in
     ok (res, (Solver.placeholder_for_state_of_new_typer ()))
+
 and type_expression' : environment -> ?tv_opt:O.type_expression -> I.expression -> O.expression result = fun e ?tv_opt ae ->
   let module L = Logger.Stateful() in
   let return expr tv =
@@ -682,7 +681,7 @@ and type_expression' : environment -> ?tv_opt:O.type_expression -> I.expression
       | None -> ok ()
       | Some tv' -> O.assert_type_expression_eq (tv' , tv) in
     let location = ae.location in
-    ok @@ make_e ~location expr tv e in
+    ok @@ make_e ~location expr tv in
   let main_error =
     let title () = "typing expression" in
     let content () = "" in
@@ -736,7 +735,7 @@ and type_expression' : environment -> ?tv_opt:O.type_expression -> I.expression
               generic_try (bad_record_access property ae prev.type_expression ae.location)
               @@ (fun () -> let ({field_type;_} : O.field_content) = O.LMap.find (convert_label property) r_tv in field_type) in
             let location = ae.location in
-            ok @@ make_e ~location (E_record_accessor {record=prev; path=convert_label property}) tv e
+            ok @@ make_e ~location (E_record_accessor {record=prev; path=convert_label property}) tv
       in
       let%bind ae =
       trace (simple_info "accessing") @@ aux e' path in
@@ -832,7 +831,7 @@ and type_expression' : environment -> ?tv_opt:O.type_expression -> I.expression
       let e' = Environment.add_ez_binder lname input_type e in
       let%bind body = type_expression' ?tv_opt:(Some tv_out) e' result in
       let output_type = body.type_expression in
-      let lambda' = make_e (E_lambda {binder = lname ; result=body}) (t_function input_type output_type ()) e' in
+      let lambda' = make_e (E_lambda {binder = lname ; result=body}) (t_function input_type output_type ()) in
       let lst' = [lambda'; v_col; v_initr] in
       let tv_lst = List.map get_type_expression lst' in
       let%bind (opname', tv) =
@@ -853,7 +852,7 @@ and type_expression' : environment -> ?tv_opt:O.type_expression -> I.expression
       let e' = Environment.add_ez_binder lname input_type e in
       let%bind body = type_expression' e' result in
       let output_type = body.type_expression in
-      let lambda' = make_e (E_lambda {binder = lname ; result=body}) (t_function input_type output_type ()) e' in
+      let lambda' = make_e (E_lambda {binder = lname ; result=body}) (t_function input_type output_type ()) in
       let lst' = [lambda';v_initr] in
       let tv_lst = List.map get_type_expression lst' in
       let%bind (opname',tv) = type_constant opname tv_lst tv_opt in
diff --git a/src/passes/8-typer-old/typer.mli b/src/passes/8-typer-old/typer.mli
index ff7009a8c..531a6b751 100644
--- a/src/passes/8-typer-old/typer.mli
+++ b/src/passes/8-typer-old/typer.mli
@@ -39,7 +39,7 @@ module Errors : sig
 end
 
 val type_program : I.program -> (O.program * O.typer_state) result
-val type_declaration : environment -> O.typer_state -> I.declaration -> (environment * O.typer_state * O.declaration option) result
+val type_declaration : environment -> O.typer_state -> I.declaration -> (environment * O.typer_state * O.declaration) result
 (* val type_match : (environment -> 'i -> 'o result) -> environment -> O.type_value -> 'i I.matching -> I.expression -> Location.t -> 'o O.matching result *)
 val evaluate_type : environment -> I.type_expression -> O.type_expression result
 val type_expression : environment -> O.typer_state -> ?tv_opt:O.type_expression -> I.expression -> (O.expression * O.typer_state) result
diff --git a/src/passes/9-self_ast_typed/helpers.ml b/src/passes/9-self_ast_typed/helpers.ml
index f42d1ea37..a63a2893a 100644
--- a/src/passes/9-self_ast_typed/helpers.ml
+++ b/src/passes/9-self_ast_typed/helpers.ml
@@ -156,10 +156,11 @@ and map_cases : mapper -> matching_expr -> matching_expr result = fun f m ->
 and map_program : mapper -> program -> program result = fun m p ->
   let aux = fun (x : declaration) ->
     match x with
-    | Declaration_constant {binder; expr ; inline ; post_env} -> (
+    | Declaration_constant {binder; expr ; inline} -> (
         let%bind expr = map_expression m expr in
-        ok (Declaration_constant {binder; expr ; inline ; post_env})
-      )
+        ok (Declaration_constant {binder; expr ; inline})
+    )
+    | Declaration_type t -> ok (Declaration_type t)
   in
   bind_map_list (bind_map_location aux) p
 
@@ -246,11 +247,15 @@ and fold_map_cases : 'a . 'a fold_mapper -> 'a -> matching_expr -> ('a * matchin
 and fold_map_program : 'a . 'a fold_mapper -> 'a -> program -> ('a * program) result = fun m init p ->
   let aux = fun (acc,acc_prg) (x : declaration Location.wrap) ->
     match Location.unwrap x with
-    | Declaration_constant {binder ; expr ; inline ; post_env} -> (
+    | Declaration_constant {binder ; expr ; inline} -> (
         let%bind (acc', expr) = fold_map_expression m acc expr in
-        let wrap_content = Declaration_constant {binder ; expr ; inline ; post_env} in
+        let wrap_content = Declaration_constant {binder ; expr ; inline} in
         ok (acc', List.append acc_prg [{x with wrap_content}])
       )
+    | Declaration_type t -> (
+        let wrap_content = Declaration_type t in
+        ok (acc, List.append acc_prg [{x with wrap_content}])
+      )
   in
   bind_fold_list aux (init,[]) p
 
@@ -298,30 +303,31 @@ type contract_type = {
 }
 
 let fetch_contract_type : string -> program -> contract_type result = fun main_fname program ->
-  let main_decl = List.rev @@ List.filter
-    (fun declt ->
-      let (Declaration_constant { binder ; expr=_ ; inline=_ ; post_env=_ }) = Location.unwrap declt in
-      String.equal (Var.to_name binder) main_fname
-    )
-    program
+  let aux declt = match Location.unwrap declt with
+    | Declaration_constant ({ binder ; expr=_ ; inline=_ } as p) ->
+       if String.equal (Var.to_name binder) main_fname
+       then Some p
+       else None
+    | Declaration_type _ -> None
   in
-  match main_decl with
-  | (hd::_) -> (
-    let (Declaration_constant { binder=_ ; expr ; inline=_ ; post_env=_ }) = Location.unwrap hd in
-    match expr.type_expression.type_content with
-    | T_arrow {type1 ; type2} -> (
-      match type1.type_content , type2.type_content with
-      | T_record tin , T_record tout when (is_tuple_lmap tin) && (is_tuple_lmap tout) ->
-        let%bind (parameter,storage) = Ast_typed.Helpers.get_pair tin in
-        let%bind (listop,storage') = Ast_typed.Helpers.get_pair tout in
-        let%bind () = trace_strong (Errors.expected_list_operation main_fname listop expr) @@
-          Ast_typed.assert_t_list_operation listop in
-        let%bind () = trace_strong (Errors.expected_same main_fname storage storage' expr) @@
-          Ast_typed.assert_type_expression_eq (storage,storage') in
-        (* TODO: on storage/parameter : assert_storable, assert_passable ? *)
-        ok { parameter ; storage }
-      |  _ -> fail @@ Errors.bad_contract_io main_fname expr
-      )
-    | _ -> fail @@ Errors.bad_contract_io main_fname expr
+  let main_decl_opt = List.find_map aux @@ List.rev  program in
+  let%bind main_decl =
+    trace_option (simple_error ("Entrypoint '"^main_fname^"' does not exist")) @@
+      main_decl_opt
+    in
+  let { binder=_ ; expr ; inline=_ } = main_decl in
+  match expr.type_expression.type_content with
+  | T_arrow {type1 ; type2} -> (
+    match type1.type_content , type2.type_content with
+    | T_record tin , T_record tout when (is_tuple_lmap tin) && (is_tuple_lmap tout) ->
+       let%bind (parameter,storage) = Ast_typed.Helpers.get_pair tin in
+       let%bind (listop,storage') = Ast_typed.Helpers.get_pair tout in
+       let%bind () = trace_strong (Errors.expected_list_operation main_fname listop expr) @@
+                       Ast_typed.assert_t_list_operation listop in
+       let%bind () = trace_strong (Errors.expected_same main_fname storage storage' expr) @@
+                       Ast_typed.assert_type_expression_eq (storage,storage') in
+       (* TODO: on storage/parameter : assert_storable, assert_passable ? *)
+       ok { parameter ; storage }
+    |  _ -> fail @@ Errors.bad_contract_io main_fname expr
   )
-  | [] -> simple_fail ("Entrypoint '"^main_fname^"' does not exist")
+  | _ -> fail @@ Errors.bad_contract_io main_fname expr
diff --git a/src/passes/9-self_ast_typed/michelson_layout.ml b/src/passes/9-self_ast_typed/michelson_layout.ml
index 2211715b9..ce59c0898 100644
--- a/src/passes/9-self_ast_typed/michelson_layout.ml
+++ b/src/passes/9-self_ast_typed/michelson_layout.ml
@@ -13,25 +13,25 @@ let accessor (record:expression) (path:label) (t:type_expression) =
   { expression_content = E_record_accessor {record; path} ;
     location = Location.generated ;
     type_expression = t ;
-    environment = record.environment }
+  }
 
 let constructor (constructor:constructor') (element:expression) (t:type_expression) =
   { expression_content = E_constructor { constructor ; element } ;
     location = Location.generated ;
     type_expression = t ;
-    environment = element.environment }
+  }
 
 let match_var (t:type_expression) =
   { expression_content = E_variable (Var.of_name "x") ;
     location = Location.generated ;
     type_expression = t ;
-    environment = Environment.add_ez_binder (Var.of_name "x") t Environment.empty}
+  }
 
 let matching (e:expression) matchee cases =
   { expression_content = E_matching {matchee ; cases};
     location = Location.generated ;
     type_expression = e.type_expression ;
-    environment = e.environment }
+  }
 
 let rec descend_types s lmap i =
   if i > 0 then
@@ -105,7 +105,7 @@ let rec to_right_comb_record
     let exp = { expression_content = E_record_accessor {record = prev ; path = label } ;
                 location = Location.generated ;
                 type_expression = field_type ;
-                environment = prev.environment } in
+              } in
     let conv_map' = LMap.add (Label "0") exp conv_map in
     LMap.add (Label "1") ({exp with expression_content = E_record (to_right_comb_record prev tl conv_map')}) conv_map'
 
@@ -275,4 +275,4 @@ let peephole_expression : expression -> expression result = fun e ->
         return match_expr.expression_content
       | _ -> return e.expression_content
   )
-  | _ as e -> return e
\ No newline at end of file
+  | _ as e -> return e
diff --git a/src/passes/9-self_ast_typed/self_ast_typed.ml b/src/passes/9-self_ast_typed/self_ast_typed.ml
index 77b50ce9c..442564638 100644
--- a/src/passes/9-self_ast_typed/self_ast_typed.ml
+++ b/src/passes/9-self_ast_typed/self_ast_typed.ml
@@ -13,8 +13,7 @@ let contract_passes = [
 let all_program program =
   let all_p = List.map Helpers.map_program all_passes in
   let%bind program' = bind_chain all_p program in
-  let program'' = Recompute_environment.program Environment.default program' in
-  ok program''
+  ok program'
 
 let all_expression =
   let all_p = List.map Helpers.map_expression all_passes in
diff --git a/src/stages/4-ast_typed/PP.ml b/src/stages/4-ast_typed/PP.ml
index 5691cac65..08e2f778c 100644
--- a/src/stages/4-ast_typed/PP.ml
+++ b/src/stages/4-ast_typed/PP.ml
@@ -326,8 +326,10 @@ and matching : (formatter -> expression -> unit) -> _ -> matching_expr -> unit =
 
 let declaration ppf (d : declaration) =
   match d with
-  | Declaration_constant {binder; expr; inline; post_env=_} ->
+  | Declaration_constant {binder; expr; inline} ->
       fprintf ppf "const %a = %a%a" expression_variable binder expression expr option_inline inline
+  | Declaration_type {type_binder; type_expr} ->
+      fprintf ppf "type %a = %a" type_variable type_binder type_expression type_expr
 
 let program ppf (p : program) =
   fprintf ppf "@[<v>%a@]"
diff --git a/src/stages/4-ast_typed/ast.ml b/src/stages/4-ast_typed/ast.ml
index e85aace9d..8a846aa61 100644
--- a/src/stages/4-ast_typed/ast.ml
+++ b/src/stages/4-ast_typed/ast.ml
@@ -272,31 +272,30 @@ and declaration_loc = declaration location_wrap
 
 and program = declaration_loc list
 
+(* A Declaration_constant is described by
+ *   a name + a type-annotated expression
+ *   a boolean indicating whether it should be inlined
+ *   the environment before the declaration (the original environment)
+ *   the environment after the declaration (i.e. with that new declaration added to the original environment). *)
 and declaration_constant = {
     binder : expression_variable ;
     expr : expression ;
     inline : bool ;
-    post_env : environment ;
+  }
+
+and declaration_type = {
+    type_binder : type_variable ;
+    type_expr : type_expression ;
   }
 
 and declaration =
-  (* A Declaration_constant is described by
-   *   a name + a type-annotated expression
-   *   a boolean indicating whether it should be inlined
-   *   the environment before the declaration (the original environment)
-   *   the environment after the declaration (i.e. with that new declaration added to the original environment). *)
   | Declaration_constant of declaration_constant
-  (*
-  | Declaration_type of (type_variable * type_expression)
-  | Declaration_constant of (named_expression * (environment * environment))
-  *)
-(* | Macro_declaration of macro_declaration *)
+  | Declaration_type of declaration_type
 
 and expression = {
     expression_content: expression_content ;
     location: location ;
     type_expression: type_expression ;
-    environment: environment ;
   }
 
 and map_kv = {
diff --git a/src/stages/4-ast_typed/ast_typed.ml b/src/stages/4-ast_typed/ast_typed.ml
index e78dc9188..9a1250ecc 100644
--- a/src/stages/4-ast_typed/ast_typed.ml
+++ b/src/stages/4-ast_typed/ast_typed.ml
@@ -4,7 +4,6 @@ module PP = PP
 module PP_generic = PP_generic
 module Combinators = struct
   include Combinators
-  include Combinators_environment
 end
 module Misc = struct
   include Misc
@@ -15,3 +14,5 @@ module Helpers = Helpers
 include Types
 include Misc
 include Combinators
+
+let program_environment env program = fst (Compute_environment.program env program)
diff --git a/src/stages/4-ast_typed/combinators.ml b/src/stages/4-ast_typed/combinators.ml
index e7959cec7..b423da73d 100644
--- a/src/stages/4-ast_typed/combinators.ml
+++ b/src/stages/4-ast_typed/combinators.ml
@@ -24,10 +24,9 @@ module Errors = struct
 end
 
 let make_t ?(loc = Location.generated) type_content core = {type_content; location=loc; type_meta = core}
-let make_e ?(location = Location.generated) expression_content type_expression environment = {
+let make_e ?(location = Location.generated) expression_content type_expression = {
   expression_content ;
   type_expression ;
-  environment ;
   location ;
 }
 let make_n_t type_name type_value = { type_name ; type_value }
@@ -83,7 +82,6 @@ let t_shallow_closure param result ?loc ?s () : type_expression = make_t ?loc (T
 
 let get_type_expression (x:expression) = x.type_expression
 let get_type' (x:type_expression) = x.type_content
-let get_environment (x:expression) = x.environment
 let get_expression (x:expression) = x.expression_content
 
 let get_lambda e : _ result = match e.expression_content with
@@ -330,13 +328,13 @@ let e_let_in let_binder inline rhs let_result = E_let_in { let_binder ; rhs ; le
 
 let e_constructor constructor element: expression_content = E_constructor {constructor;element}
 
-let e_bool b env : expression_content = e_constructor (Constructor (string_of_bool b)) (make_e (e_unit ())(t_unit()) env)
+let e_bool b : expression_content = e_constructor (Constructor (string_of_bool b)) (make_e (e_unit ())(t_unit()))
 
 let e_a_unit = make_e (e_unit ()) (t_unit ())
 let e_a_int n = make_e (e_int n) (t_int ())
 let e_a_nat n = make_e (e_nat n) (t_nat ())
 let e_a_mutez n = make_e (e_mutez n) (t_mutez ())
-let e_a_bool b = fun env -> make_e (e_bool b env) (t_bool ()) env
+let e_a_bool b = make_e (e_bool b) (t_bool ())
 let e_a_string s = make_e (e_string s) (t_string ())
 let e_a_address s = make_e (e_address s) (t_address ())
 let e_a_pair a b = make_e (e_pair a b)
@@ -381,7 +379,8 @@ let get_a_record_accessor = fun t ->
 let get_declaration_by_name : program -> string -> declaration result = fun p name ->
   let aux : declaration -> bool = fun declaration ->
     match declaration with
-    | Declaration_constant { binder ; expr=_ ; inline=_ ; post_env=_ } -> binder = Var.of_name name
+    | Declaration_constant { binder ; expr=_ ; inline=_ } -> binder = Var.of_name name
+    | Declaration_type _ -> false
   in
   trace_option (Errors.declaration_not_found name ()) @@
   List.find_opt aux @@ List.map Location.unwrap p
diff --git a/src/stages/4-ast_typed/combinators.mli b/src/stages/4-ast_typed/combinators.mli
index 192939c72..f4fe615b2 100644
--- a/src/stages/4-ast_typed/combinators.mli
+++ b/src/stages/4-ast_typed/combinators.mli
@@ -3,7 +3,7 @@ open Types
 
 val make_n_t : type_variable -> type_expression -> named_type_content
 val make_t : ?loc:Location.t -> type_content -> S.type_expression option -> type_expression
-val make_e : ?location:Location.t -> expression_content -> type_expression -> environment -> expression
+val make_e : ?location:Location.t -> expression_content -> type_expression -> expression
 
 val t_bool : ?loc:Location.t -> ?s:S.type_expression -> unit -> type_expression
 val t_string : ?loc:Location.t -> ?s:S.type_expression -> unit -> type_expression
@@ -38,7 +38,6 @@ val t_function : type_expression -> type_expression -> ?loc:Location.t -> ?s:S.t
 val t_shallow_closure : type_expression -> type_expression -> ?loc:Location.t -> ?s:S.type_expression -> unit -> type_expression
 val get_type_expression : expression -> type_expression
 val get_type' : type_expression -> type_content
-val get_environment : expression -> environment
 val get_expression : expression -> expression_content
 val get_lambda : expression -> lambda result
 val get_lambda_with_type : expression -> (lambda * ( type_expression * type_expression) ) result
@@ -119,7 +118,7 @@ val e_unit : unit -> expression_content
 val e_int : Z.t -> expression_content
 val e_nat : Z.t -> expression_content
 val e_mutez : Z.t -> expression_content
-val e_bool : bool -> environment -> expression_content
+val e_bool : bool -> expression_content
 val e_string : ligo_string -> expression_content
 val e_bytes : bytes -> expression_content
 val e_timestamp : Z.t -> expression_content
@@ -135,22 +134,22 @@ val e_application : expression -> expression -> expression_content
 val e_variable : expression_variable -> expression_content
 val e_let_in : expression_variable -> inline -> expression -> expression -> expression_content
 
-val e_a_unit : environment -> expression
-val e_a_int : Z.t -> environment -> expression
-val e_a_nat : Z.t -> environment -> expression
-val e_a_mutez : Z.t -> environment -> expression
-val e_a_bool : bool -> environment -> expression
-val e_a_string : ligo_string -> environment -> expression
-val e_a_address : string -> environment -> expression
-val e_a_pair : expression -> expression -> environment -> expression
-val e_a_some : expression -> environment -> expression
-val e_a_lambda : lambda -> type_expression -> type_expression -> environment -> expression
-val e_a_none : type_expression -> environment -> expression
-val e_a_record : expression label_map -> environment -> expression
-val e_a_application : expression -> expression -> environment -> expression
-val e_a_variable : expression_variable -> type_expression -> environment -> expression
-val ez_e_a_record : ( label * expression ) list -> environment -> expression
-val e_a_let_in : expression_variable -> bool -> expression -> expression -> environment -> expression
+val e_a_unit : expression
+val e_a_int : Z.t -> expression
+val e_a_nat : Z.t -> expression
+val e_a_mutez : Z.t -> expression
+val e_a_bool : bool -> expression
+val e_a_string : ligo_string -> expression
+val e_a_address : string -> expression
+val e_a_pair : expression -> expression -> expression
+val e_a_some : expression -> expression
+val e_a_lambda : lambda -> type_expression -> type_expression -> expression
+val e_a_none : type_expression -> expression
+val e_a_record : expression label_map -> expression
+val e_a_application : expression -> expression -> expression
+val e_a_variable : expression_variable -> type_expression -> expression
+val ez_e_a_record : ( label * expression ) list -> expression
+val e_a_let_in : expression_variable -> bool -> expression -> expression -> expression
 
 val get_a_int : expression -> Z.t result
 val get_a_unit : expression -> unit result
diff --git a/src/stages/4-ast_typed/combinators_environment.ml b/src/stages/4-ast_typed/combinators_environment.ml
deleted file mode 100644
index 78e11ad9a..000000000
--- a/src/stages/4-ast_typed/combinators_environment.ml
+++ /dev/null
@@ -1,25 +0,0 @@
-open Types
-open Combinators
-
-let make_a_e_empty expression type_annotation = make_e expression type_annotation Environment.empty
-
-let e_a_empty_unit = e_a_unit Environment.empty
-let e_a_empty_int n = e_a_int n Environment.empty
-let e_a_empty_nat n = e_a_nat n Environment.empty
-let e_a_empty_mutez n = e_a_mutez n Environment.empty
-let e_a_empty_bool b = e_a_bool b Environment.empty
-let e_a_empty_string s = e_a_string s Environment.empty
-let e_a_empty_address s = e_a_address s Environment.empty
-let e_a_empty_pair a b = e_a_pair a b Environment.empty
-let e_a_empty_some s = e_a_some s Environment.empty
-let e_a_empty_none t = e_a_none t Environment.empty
-let e_a_empty_record r = e_a_record r Environment.empty
-let ez_e_a_empty_record r = ez_e_a_record r Environment.empty
-let e_a_empty_lambda l i o = e_a_lambda l i o Environment.empty
-
-open Environment
-
-let env_sum_type ?(env = empty)
-    ?(type_name = Var.of_name "a_sum_type")
-    (lst : (constructor' * ctor_content) list) =
-  add_type type_name (make_t_ez_sum lst) env
diff --git a/src/stages/4-ast_typed/combinators_environment.mli b/src/stages/4-ast_typed/combinators_environment.mli
deleted file mode 100644
index 64b325975..000000000
--- a/src/stages/4-ast_typed/combinators_environment.mli
+++ /dev/null
@@ -1,19 +0,0 @@
-open Types
-
-val make_a_e_empty : expression_content -> type_expression -> expression
-
-val e_a_empty_unit : expression
-val e_a_empty_int : Z.t -> expression
-val e_a_empty_nat : Z.t -> expression
-val e_a_empty_mutez : Z.t -> expression
-val e_a_empty_bool : bool -> expression
-val e_a_empty_string : ligo_string -> expression
-val e_a_empty_address : string -> expression
-val e_a_empty_pair : expression -> expression -> expression
-val e_a_empty_some : expression -> expression
-val e_a_empty_none : type_expression -> expression
-val e_a_empty_record : expression label_map -> expression
-val ez_e_a_empty_record : ( label * expression ) list -> expression
-val e_a_empty_lambda : lambda -> type_expression -> type_expression -> expression
-
-val env_sum_type : ?env:environment -> ?type_name:type_variable -> (constructor' * ctor_content) list ->  environment
diff --git a/src/passes/9-self_ast_typed/recompute_environment.ml b/src/stages/4-ast_typed/compute_environment.ml
similarity index 75%
rename from src/passes/9-self_ast_typed/recompute_environment.ml
rename to src/stages/4-ast_typed/compute_environment.ml
index 4124038c2..ce4013a28 100644
--- a/src/passes/9-self_ast_typed/recompute_environment.ml
+++ b/src/stages/4-ast_typed/compute_environment.ml
@@ -1,23 +1,9 @@
-open Ast_typed
-
-(*
-  During the modifications of the passes on `Ast_typed`, the binding
-  environments are not kept in sync. To palliate this, this module
-  recomputes them from scratch.
-*)
-
-(*
-  This module is very coupled to `typer.ml`. Given environments are
-  not used until the next pass, it makes sense to split this into
-  its own separate pass. This pass would go from `Ast_typed` without
-  environments to `Ast_typed` with embedded environments.
-*)
+open Types
 
 let rec expression : environment -> expression -> expression = fun env expr ->
   (* Standard helper functions to help with the fold *)
-  let return ?(env' = env) content = {
+  let return content = {
       expr with
-      environment = env' ;
       expression_content = content ;
     } in
   let return_id = return expr.expression_content in
@@ -34,9 +20,9 @@ let rec expression : environment -> expression -> expression = fun env expr ->
     return @@ E_lambda { c with result }
   )
   | E_let_in c -> (
-    let env' = Environment.add_ez_declaration c.let_binder c.rhs env in
-    let let_result = self ~env' c.let_result in
     let rhs = self c.rhs in
+    let env' = Environment.add_ez_declaration c.let_binder rhs env in
+    let let_result = self ~env' c.let_result in
     return @@ E_let_in { c with rhs ; let_result }
   )
   (* rec fun_name binder -> result *)
@@ -90,7 +76,7 @@ and cases : environment -> matching_expr -> matching_expr = fun env cs ->
     let match_cons =
       let mc = c.match_cons in
       let env_hd = Environment.add_ez_binder mc.hd mc.tv env in
-      let env_tl = Environment.add_ez_binder mc.tl (t_list mc.tv ()) env_hd in
+      let env_tl = Environment.add_ez_binder mc.tl (Combinators.t_list mc.tv ()) env_hd in
       let body = self ~env':env_tl mc.body in
       { mc with body }
     in
@@ -139,24 +125,27 @@ and cases : environment -> matching_expr -> matching_expr = fun env cs ->
     return @@ Match_variant { c with cases }
   )
 
-let program : environment -> program -> program = fun init_env prog ->
+let program : environment -> program -> environment * program = fun init_env prog ->
   (*
       BAD
       We take the old type environment and add it to the current value environment
       because type declarations are removed in the typer. They should be added back.
    *)
-  let merge old_env re_env = {
-      expression_environment = re_env.expression_environment ;
-      type_environment = old_env.type_environment ;
-    } in
   let aux (pre_env , rev_decls) decl_wrapped =
-    let (Declaration_constant c) = Location.unwrap decl_wrapped in
-    let expr = expression pre_env c.expr in
-    let post_env = Environment.add_ez_declaration c.binder c.expr pre_env in
-    let post_env' = merge c.post_env post_env in
-    let wrap_content = Declaration_constant { c with expr ; post_env = post_env' } in
-    let decl_wrapped' = { decl_wrapped with wrap_content } in
-    (post_env , decl_wrapped' :: rev_decls)
+    match Location.unwrap decl_wrapped with
+    | Declaration_constant c -> (
+      let expr = expression pre_env c.expr in
+      let post_env = Environment.add_ez_declaration c.binder expr pre_env in
+      let wrap_content = Declaration_constant { c with expr } in
+      let decl_wrapped' = { decl_wrapped with wrap_content } in
+      (post_env , decl_wrapped' :: rev_decls)
+    )
+    | Declaration_type t -> (
+      let post_env = Environment.add_type t.type_binder t.type_expr pre_env in      
+      let wrap_content = Declaration_type t in
+      let decl_wrapped' = { decl_wrapped with wrap_content } in
+      (post_env , decl_wrapped' :: rev_decls)
+    )
   in
-  let (_last_env , rev_decls) = List.fold_left aux (init_env , []) prog in
-  List.rev rev_decls
+  let (last_env , rev_decls) = List.fold_left aux (init_env , []) prog in
+  (last_env , List.rev rev_decls)
diff --git a/src/stages/4-ast_typed/environment.ml b/src/stages/4-ast_typed/environment.ml
index 30e59ebab..0b9457466 100644
--- a/src/stages/4-ast_typed/environment.ml
+++ b/src/stages/4-ast_typed/environment.ml
@@ -38,6 +38,9 @@ let add_ez_binder : expression_variable -> type_expression -> t -> t = fun k v e
 let add_ez_declaration : expression_variable -> expression -> t -> t = fun k ae e ->
   add_expr k (make_element_declaration e ae) e
 
+let add_ez_sum_type ?(env = empty) ?(type_name = Var.of_name "a_sum_type") (lst : (constructor' * ctor_content) list) =
+  add_type type_name (make_t_ez_sum lst) env
+
 let convert_constructor' (S.Constructor c) = Constructor c
 
 let get_constructor : Ast_core.constructor' -> t -> (type_expression * type_expression) option = fun k x -> (* Left is the constructor, right is the sum type *)
@@ -76,4 +79,4 @@ module PP = struct
       expr_environment (get_expr_environment e)
       type_environment (get_type_environment e)
 
-end
\ No newline at end of file
+end
diff --git a/src/stages/4-ast_typed/environment.mli b/src/stages/4-ast_typed/environment.mli
index 6b3fb52e2..d73279d85 100644
--- a/src/stages/4-ast_typed/environment.mli
+++ b/src/stages/4-ast_typed/environment.mli
@@ -11,6 +11,7 @@ val get_opt : expression_variable -> t -> element option
 val get_type_opt : type_variable -> t -> type_expression option
 val get_constructor : Ast_core.constructor' -> t -> (type_expression * type_expression) option
 
+val add_ez_sum_type : ?env:environment -> ?type_name:type_variable -> (constructor' * ctor_content) list ->  environment
 module PP : sig
   open Format
 
diff --git a/src/stages/4-ast_typed/misc.ml b/src/stages/4-ast_typed/misc.ml
index a3df9718f..7528dab2e 100644
--- a/src/stages/4-ast_typed/misc.ml
+++ b/src/stages/4-ast_typed/misc.ml
@@ -511,19 +511,17 @@ let merge_annotation (a:type_expression option) (b:type_expression option) err :
 
 let get_entry (lst : program) (name : string) : expression result =
   trace_option (Errors.missing_entry_point name) @@
-  let aux x =
-    let (Declaration_constant { binder ; expr ; inline=_ ; _ }) = Location.unwrap x in
-    if Var.equal binder (Var.of_name name)
-    then Some expr
-    else None
+    let aux x =
+      match Location.unwrap x with
+      | Declaration_constant { binder ; expr ; inline=_ } -> (
+        if Var.equal binder (Var.of_name name)
+        then Some expr
+        else None
+      )
+      | Declaration_type _ -> None
   in
   List.find_map aux lst
 
-let program_environment (program : program) : environment =
-  let last_declaration = Location.unwrap List.(hd @@ rev program) in
-  match last_declaration with
-  | Declaration_constant { binder=_ ; expr=_ ; inline=_ ; post_env } -> post_env
-
 let equal_variables a b : bool =
   match a.expression_content, b.expression_content with
   | E_variable a, E_variable b -> Var.equal a b
diff --git a/src/stages/4-ast_typed/misc.mli b/src/stages/4-ast_typed/misc.mli
index ae0bb692f..561458303 100644
--- a/src/stages/4-ast_typed/misc.mli
+++ b/src/stages/4-ast_typed/misc.mli
@@ -70,7 +70,6 @@ val assert_literal_eq : ( literal * literal ) -> unit result
 *)
 
 val get_entry : program -> string -> expression result
-val program_environment : program -> environment
 
 val p_constant : constant_tag -> p_ctor_args -> type_value
 val c_equation : type_value -> type_value -> string -> type_constraint
diff --git a/src/stages/4-ast_typed/misc_smart.ml b/src/stages/4-ast_typed/misc_smart.ml
index a09ed2acc..d62665149 100644
--- a/src/stages/4-ast_typed/misc_smart.ml
+++ b/src/stages/4-ast_typed/misc_smart.ml
@@ -8,8 +8,9 @@ let program_to_main : program -> string -> lambda result = fun p s ->
   let%bind (main , input_type , _) =
     let pred = fun d ->
       match d with
-      | Declaration_constant { binder; expr; inline=_ ; post_env=_ } when binder = Var.of_name s -> Some expr
+      | Declaration_constant { binder; expr; inline=_ } when binder = Var.of_name s -> Some expr
       | Declaration_constant _ -> None
+      | Declaration_type _ -> None
     in
     let%bind main =
       trace_option (simple_error "no main with given name") @@
@@ -20,16 +21,11 @@ let program_to_main : program -> string -> lambda result = fun p s ->
       | _ -> simple_fail "program main isn't a function" in
     ok (main , input_ty , output_ty)
   in
-  let env =
-    let aux = fun _ d ->
-      match d with
-      | Declaration_constant {binder=_ ; expr= _ ; inline=_ ; post_env } -> post_env in
-    List.fold_left aux Environment.empty (List.map Location.unwrap p) in
   let binder = Var.of_name "@contract_input" in
   let result =
-    let input_expr = e_a_variable binder input_type env in
-    let main_expr = e_a_variable (Var.of_name s) (get_type_expression main) env in
-    e_a_application main_expr input_expr env in
+    let input_expr = e_a_variable binder input_type in
+    let main_expr = e_a_variable (Var.of_name s) (get_type_expression main) in
+    e_a_application main_expr input_expr in
   ok {
     binder ;
     result ;
@@ -46,8 +42,8 @@ module Captured_variables = struct
   let of_list : expression_variable list -> bindings = fun x -> x
 
   let rec expression : bindings -> expression -> bindings result = fun b e ->
-    expression_content b e.environment e.expression_content
-  and expression_content : bindings -> environment -> expression_content -> bindings result = fun b env ec ->
+    expression_content b e.expression_content
+  and expression_content : bindings -> expression_content -> bindings result = fun b ec ->
     let self = expression b in
     match ec with
     | E_lambda l -> ok @@ Free_variables.lambda empty l
@@ -56,12 +52,7 @@ module Captured_variables = struct
       let%bind lst' = bind_map_list self arguments in
       ok @@ unions lst'
     | E_variable name -> (
-        let%bind env_element =
-          trace_option (simple_error "missing var in env") @@
-          Environment.get_opt name env in
-        match env_element.definition with
-        | ED_binder -> ok empty
-        | ED_declaration {expr=_ ; free_variables=_} -> simple_fail "todo"
+      if mem name b then ok empty else ok (singleton name)
       )
     | E_application {lamb;args} ->
       let%bind lst' = bind_map_list self [ lamb ; args ] in
@@ -84,7 +75,7 @@ module Captured_variables = struct
       expression b' li.let_result
     | E_recursive r -> 
       let b' = union (singleton r.fun_name) b in
-      expression_content b' env @@ E_lambda r.lambda
+      expression_content b' @@ E_lambda r.lambda
 
   and matching_variant_case : (bindings -> expression -> bindings result) -> bindings -> matching_content_case -> bindings result  = fun f b { constructor=_ ; pattern ; body } ->
     f (union (singleton pattern) b) body
diff --git a/src/stages/5-mini_c/combinators.ml b/src/stages/5-mini_c/combinators.ml
index ff421421c..f01eda745 100644
--- a/src/stages/5-mini_c/combinators.ml
+++ b/src/stages/5-mini_c/combinators.ml
@@ -183,6 +183,15 @@ let e_let_in ?loc v tv inline expr body : expression = Expression.(make_tpl ?loc
     E_let_in ((v , tv) , inline, expr , body) ,
     get_type body
   ))
+let e_application ?loc f t arg: expression = Expression.(make_tpl ?loc(
+    E_application (f,arg) ,
+    t
+  ))
+let e_var ?loc vname t: expression = Expression.(make_tpl ?loc(
+    E_variable vname ,
+    t
+  ))
+
 
 let ez_e_sequence ?loc a b : expression = Expression.(make_tpl (E_sequence (make_tpl ?loc (a , t_unit ()) , b) , get_type b))
 
diff --git a/src/stages/5-mini_c/combinators.mli b/src/stages/5-mini_c/combinators.mli
index f198e8b8e..3a9aab3ed 100644
--- a/src/stages/5-mini_c/combinators.mli
+++ b/src/stages/5-mini_c/combinators.mli
@@ -78,3 +78,5 @@ val d_unit : value
 
 val environment_wrap : environment -> environment -> environment_wrap
 val id_environment_wrap : environment -> environment_wrap
+val e_var : ?loc:Location.t -> var_name -> type_expression -> expression
+val e_application : ?loc:Location.t -> expression -> type_expression -> expression -> expression
diff --git a/src/stages/typesystem/misc.ml b/src/stages/typesystem/misc.ml
index d7662698a..336f8cdf2 100644
--- a/src/stages/typesystem/misc.ml
+++ b/src/stages/typesystem/misc.ml
@@ -195,20 +195,19 @@ module Substitution = struct
         let%bind cases = s_matching_expr ~substs cases in
         ok @@ T.E_matching {matchee;cases}
 
-    and s_expression : T.expression w = fun ~(substs:substs) { expression_content; type_expression; environment; location } ->
+    and s_expression : T.expression w = fun ~(substs:substs) { expression_content; type_expression; location } ->
       let%bind expression_content = s_expression_content ~substs expression_content in
       let%bind type_expr = s_type_expression ~substs type_expression in
-      let%bind environment = s_environment ~substs environment in
       let location = location in
-      ok T.{ expression_content;type_expression=type_expr; environment; location }
+      ok T.{ expression_content;type_expression=type_expr; location }
 
     and s_declaration : T.declaration w = fun ~substs ->
       function
-        Ast_typed.Declaration_constant {binder ; expr ; inline ; post_env} ->
-        let%bind binder = s_variable ~substs binder in
-        let%bind expr = s_expression ~substs expr in
-        let%bind post_env = s_environment ~substs post_env in
-        ok @@ Ast_typed.Declaration_constant {binder; expr; inline; post_env}
+      | Ast_typed.Declaration_constant {binder ; expr ; inline} ->
+         let%bind binder = s_variable ~substs binder in
+         let%bind expr = s_expression ~substs expr in
+         ok @@ Ast_typed.Declaration_constant {binder; expr; inline}
+      | Declaration_type t -> ok (Ast_typed.Declaration_type t)
 
     and s_declaration_wrap :T.declaration Location.wrap w = fun ~substs d ->
       Trace.bind_map_location (s_declaration ~substs) d    
diff --git a/src/test/contracts/double_fold_converter.religo b/src/test/contracts/double_fold_converter.religo
new file mode 100644
index 000000000..01245222b
--- /dev/null
+++ b/src/test/contracts/double_fold_converter.religo
@@ -0,0 +1,72 @@
+type tokenId = nat;
+type tokenOwner = address;
+type tokenAmount = nat;
+type transferContents = {
+    to_: tokenOwner,
+    token_id: tokenId,
+    amount: tokenAmount
+};
+type transfer = {
+    from_: tokenOwner,
+    txs: list(transferContents)
+};
+type transferContentsMichelson = michelson_pair_right_comb(transferContents);
+type transferAuxiliary = {
+    from_: tokenOwner,
+    txs: list(transferContentsMichelson)
+};
+type transferMichelson = michelson_pair_right_comb(transferAuxiliary);
+type transferParameter = list(transferMichelson);
+type parameter = 
+| Transfer(transferParameter)
+type storage = big_map(tokenId, tokenOwner);
+type entrypointParameter = (parameter, storage);
+type entrypointReturn = (list(operation), storage);
+let errorTokenUndefined = "TOKEN_UNDEFINED";
+let errorNotOwner = "NOT_OWNER";
+let errorInsufficientBalance = "INSUFFICIENT_BALANCE";
+type transferContentsIteratorAccumulator = (storage, tokenOwner);
+let transferContentsIterator = ((accumulator, transferContentsMichelson): (transferContentsIteratorAccumulator, transferContentsMichelson)): transferContentsIteratorAccumulator => {
+    let (storage, from_) = accumulator;
+    let transferContents: transferContents = Layout.convert_from_right_comb(transferContentsMichelson);
+    let tokenOwner: option(tokenOwner) = Map.find_opt(transferContents.token_id, storage);
+    let tokenOwner = switch (tokenOwner) {
+        | None => (failwith(errorTokenUndefined): tokenOwner)
+        | Some(tokenOwner) => if (tokenOwner == from_) {
+                tokenOwner
+            } else {
+                (failwith(errorInsufficientBalance): tokenOwner);
+            }
+    };
+    let storage = Map.update(
+        transferContents.token_id,
+        Some(transferContents.to_),
+        storage
+    );
+    (storage, from_)
+};
+let allowOnlyOwnTransfer = (from: tokenOwner): unit => {
+    if (from != Tezos.sender) {
+        failwith(errorNotOwner)
+    } else { (); }
+}
+let transferIterator = ((storage, transferMichelson): (storage, transferMichelson)): storage => {
+    let transferAuxiliary2: transferAuxiliary = Layout.convert_from_right_comb(transferMichelson);
+    let from_: tokenOwner = transferAuxiliary2.from_;
+    allowOnlyOwnTransfer(from_);
+    let (storage, _) = List.fold(
+        transferContentsIterator, 
+        transferAuxiliary2.txs,
+        (storage, from_)
+    );
+    storage
+};
+let transfer = ((transferParameter, storage): (transferParameter, storage)): entrypointReturn => {
+    let storage = List.fold(transferIterator, transferParameter, storage);
+    (([]: list(operation)), storage);
+};
+let main = ((parameter, storage): entrypointParameter): entrypointReturn => {
+    switch (parameter) {
+        | Transfer(transferParameter) => transfer((transferParameter, storage))
+    }
+}
\ No newline at end of file
diff --git a/src/test/test_helpers.ml b/src/test/test_helpers.ml
index ded88c33b..adeb5649a 100644
--- a/src/test/test_helpers.ml
+++ b/src/test/test_helpers.ml
@@ -38,7 +38,7 @@ open Ast_imperative
 
 let pack_payload (program:Ast_typed.program) (payload:expression) : bytes result =
   let%bind code =
-    let env = Ast_typed.program_environment program in
+    let env = Ast_typed.program_environment Environment.default program in
 
     let%bind sugar     = Compile.Of_imperative.compile_expression payload in
     let%bind core      = Compile.Of_sugar.compile_expression sugar in
@@ -89,7 +89,7 @@ let typed_program_with_imperative_input_to_michelson
     (program: Ast_typed.program) (entry_point: string)
     (input: Ast_imperative.expression) : Compiler.compiled_expression result =
   Printexc.record_backtrace true;
-  let env = Ast_typed.program_environment program in
+  let env = Ast_typed.program_environment Environment.default program in
   let state = Typer.Solver.initial_state in
   let%bind sugar            = Compile.Of_imperative.compile_expression input in
   let%bind core             = Compile.Of_sugar.compile_expression sugar in
diff --git a/src/test/typer_tests.ml b/src/test/typer_tests.ml
index e4ea12df5..c26e690ba 100644
--- a/src/test/typer_tests.ml
+++ b/src/test/typer_tests.ml
@@ -34,7 +34,7 @@ module TestExpressions = struct
 
   module I = Simplified.Combinators
   module O = Typed.Combinators
-  module E = O
+  module E = Typed.Environment
 
   let unit   () : unit result = test_expression I.(e_unit ())    O.(t_unit ())
   let int    () : unit result = test_expression I.(e_int (Z.of_int 32))     O.(t_int ())
@@ -59,7 +59,7 @@ module TestExpressions = struct
         (Typed.Constructor "foo", {ctor_type = Typed.t_int () ; michelson_annotation = None ; ctor_decl_pos = 0});
         (Typed.Constructor "bar", {ctor_type = Typed.t_string () ; michelson_annotation = None ; ctor_decl_pos = 1}) ]
     in test_expression
-      ~env:(E.env_sum_type variant_foo_bar)
+      ~env:(E.add_ez_sum_type variant_foo_bar)
       I.(e_constructor "foo" (e_int (Z.of_int 32)))
       O.(make_t_ez_sum variant_foo_bar)