diff --git a/compiler/heptagon/main/hept_compiler.ml b/compiler/heptagon/main/hept_compiler.ml
index c43147a..b622669 100644
--- a/compiler/heptagon/main/hept_compiler.ml
+++ b/compiler/heptagon/main/hept_compiler.ml
@@ -44,12 +44,12 @@ let compile_program p =
   (* Shared variables (last) *)
   let p = pass "Last" true Last.program p pp in
 
-  (* Remove switch statements *)
-  let p = pass "switch" true Switch.program p pp in
-
   (* Reset *)
   let p = pass "Reset" true Reset.program p pp in
 
+  (* Remove switch statements *)
+  let p = pass "switch" true Switch.program p pp in
+
   (* Every *)
   let p = pass "Every" true Every.program p pp in
 
diff --git a/compiler/heptagon/transformations/reset.ml b/compiler/heptagon/transformations/reset.ml
index 90e7bd1..2c078db 100644
--- a/compiler/heptagon/transformations/reset.ml
+++ b/compiler/heptagon/transformations/reset.ml
@@ -94,8 +94,8 @@ let eqdesc funs (res,stateful) = function
       else ( (* recursive call to remove useless resets *)
         let b, _ = Hept_mapfold.block_it funs (res,stateful) b in
         Eblock(b), (res,stateful))
-  | Eswitch _ | Eautomaton _ | Epresent _ ->
-      Format.eprintf "[reset] should be done after [switch automaton present]";
+  | Eautomaton _ | Epresent _ ->
+      Format.eprintf "[reset] should be done after [automaton present]";
       assert false
   | _ -> raise Errors.Fallback
 
diff --git a/compiler/heptagon/transformations/switch.ml b/compiler/heptagon/transformations/switch.ml
index 9abe755..6d58091 100644
--- a/compiler/heptagon/transformations/switch.ml
+++ b/compiler/heptagon/transformations/switch.ml
@@ -124,10 +124,12 @@ let level_up defnames constr h =
   let ident_level_up n new_h =
     let old_n = rename n h in
     let new_n = fresh_case_var (Idents.name old_n) constr in
-    add n new_n new_h in
+    add n new_n new_h
+  in
   fold (fun n _ new_h -> ident_level_up n new_h) defnames empty
 
-let add_to_vds vd_env locals h =
+(* only use of [vd_env] is here to create y_Up with the same type as y, etc. *)
+let add_to_locals vd_env locals h =
   let add_one n nn (locals,vd_env) =
     let orig_vd = Idents.Env.find n vd_env in
     let vd_nn = mk_var_dec nn orig_vd.v_type in
@@ -180,7 +182,6 @@ let eqdesc funs (vd_env,env,h) eqd = match eqd with
 
       (* typing have proved that defined variables are the same among states *)
       let defnames = (List.hd sw_h_l).w_block.b_defnames in
-      let defnames = Rename.rename_defnames defnames h in
 
       (* deal with the handlers *)
       let switch_handler (c_h_l, locals, equs, vd_env) sw_h =
@@ -189,7 +190,7 @@ let eqdesc funs (vd_env,env,h) eqd = match eqd with
         let h = Rename.level_up defnames constr h in
         let env = Env.level_up constr ck env in
         (* add to the locals the new vars from leveling_up *)
-        let locals,vd_env = Rename.add_to_vds vd_env locals h in
+        let locals,vd_env = Rename.add_to_locals vd_env locals h in
         (* mapfold with updated envs *)
         let b_eq, (_,_,h) = block_it funs (vd_env,env,h) sw_h.w_block in
         (* inline the handler as a block *)
@@ -202,16 +203,15 @@ let eqdesc funs (vd_env,env,h) eqd = match eqd with
       in
 
       (* create a merge equation for each defnames *)
-      let new_merge n equs =
-        let ty = (Idents.Env.find n defnames) in
-        let c_h_to_c_e (constr,h) =
-          constr, mk_exp (Evar (Rename.rename n h)) ty in
+      let new_merge n ty equs =
+        let c_h_to_c_e (constr,h) = constr, mk_exp (Evar(Rename.rename n h)) ty in
         let c_e_l = List.map c_h_to_c_e c_h_l in
         let merge = mk_exp (Emerge (ck, c_e_l)) ty in
-        (mk_equation (Eeq (Evarpat n, merge))) :: equs
+        (mk_equation (Eeq (Evarpat (Rename.rename n h), merge))) :: equs
       in
       let equs =
-        Idents.Env.fold (fun n _ equs -> new_merge n equs) defnames equs in
+        Idents.Env.fold (fun n ty equs -> new_merge n ty equs) defnames equs
+      in
      
         (* return the transformation in a block *)
       let b = mk_block ~defnames:defnames ~locals:locals equs in
diff --git a/test/good/autohiera.ept b/test/good/autohiera.ept
new file mode 100644
index 0000000..a112692
--- /dev/null
+++ b/test/good/autohiera.ept
@@ -0,0 +1,28 @@
+node count() returns (o : int)
+let
+  o = 0 fby (o + 1);
+tel
+
+node main(x : bool) returns (d : bool)
+var last c : bool = false;
+let
+  d = c;
+  automaton
+    state One
+      var last xone : bool = false;
+      do
+        automaton
+          state A
+            do c = xone & x;
+               xone = true;
+            until count() = 2 then B
+          state B
+            do
+            until count() = 3 then A
+        end 
+      until count() = 5 then Two
+    state Two
+      do c = x;
+      until count() = 3 then One
+  end
+tel
diff --git a/test/good/autohiera2.ept b/test/good/autohiera2.ept
new file mode 100644
index 0000000..4cf134f
--- /dev/null
+++ b/test/good/autohiera2.ept
@@ -0,0 +1,24 @@
+node count() returns (o : int)
+let
+  o = 0 fby (o + 1);
+tel
+
+node main(x : bool) returns (c : bool)
+let
+  automaton
+    state One
+      do
+        automaton
+          state A
+            do c = x;
+            until count() = 2 then B
+          state B
+            do c = not(x);
+            until true then A
+        end 
+      until true then Two
+    state Two
+      do c = x;
+      until true then One
+  end
+tel