diff --git a/compiler/global/clocks.ml b/compiler/global/clocks.ml
index e818cc5..04bbf50 100644
--- a/compiler/global/clocks.ml
+++ b/compiler/global/clocks.ml
@@ -38,6 +38,16 @@ let gen_index () = (incr index; !index)
 (** returns a new clock variable *)
 let fresh_clock () = Cvar { contents = Cindex (gen_index ()); }
 
+(** returns a new clock type corresponding to the data type [ty] *)
+let rec fresh_ct ty = match ty with
+  | Tprod ty_list ->
+      (match ty_list with
+        | [] -> Ck (fresh_clock())
+        | _ -> Cprod (List.map fresh_ct ty_list))
+  | Tarray (t, _) -> fresh_ct t
+  | Tid _ | Tinvalid -> Ck (fresh_clock())
+
+
 (** returns the canonic (short) representant of a [ck]
     and update it to this value. *)
 let rec ck_repr ck = match ck with
@@ -90,19 +100,26 @@ and unify_list t1_list t2_list =
   with _ -> raise Unify
 
 
-let rec skeleton ck = function
+let prod ck_l = match ck_l with
+  | [ck] -> Ck ck
+  | _ -> Cprod (List.map (fun ck -> Ck ck) ck_l)
+
+(*
+let rec tuple ck = function
   | Tprod ty_list ->
       (match ty_list with
         | [] -> Ck ck
-        | _ -> Cprod (List.map (skeleton ck) ty_list))
-  | Tarray (t, _) -> skeleton ck t
+        | _ -> Cprod (List.map (tuple ck) ty_list))
+  | Tarray (t, _) -> tuple ck t
   | Tid _ | Tinvalid -> Ck ck
+*)
+(*
+let max ck_1 ck_2 = match ck_repr ck_1, ck_reprck_2 with
+  | 
 
-(* TODO here it implicitely says that the base clock is Cbase
-    and that all tuple is on Cbase *)
-let ckofct = function | Ck ck -> ck_repr ck | Cprod _ -> Cbase
-
-
-
+let rec optim_base_ck base_ck ct = match ct with
+  | Ck ck -> 
+  | Cprod c_l -> 
+*)
 
 
diff --git a/compiler/global/global_printer.ml b/compiler/global/global_printer.ml
index fb97c35..a102d24 100644
--- a/compiler/global/global_printer.ml
+++ b/compiler/global/global_printer.ml
@@ -149,8 +149,8 @@ let print_ident ff id = Format.fprintf ff "%s" (name id)
   | Cvar { contents = Cindex _ } -> fprintf ff "base"
   | Cvar { contents = Clink ck } -> print_ck ff ck
 
-let rec print_clock ff = function
+let rec print_ct ff = function
   | Ck ck -> print_ck ff ck
   | Cprod ct_list ->
-      fprintf ff "@[<2>(%a)@]" (print_list_r print_clock """ *""") ct_list
+      fprintf ff "@[<2>(%a)@]" (print_list_r print_ct """ *""") ct_list
 
diff --git a/compiler/global/idents.ml b/compiler/global/idents.ml
index 318ef35..c7e3344 100644
--- a/compiler/global/idents.ml
+++ b/compiler/global/idents.ml
@@ -138,6 +138,7 @@ let ident_of_name s =
   let id = { num = !num; source = s; is_generated = false } in
     UniqueNames.assign_name id; id
 
+let source_name id = id.source
 let name id = UniqueNames.name id
 let enter_node n = UniqueNames.enter_node n
 
diff --git a/compiler/global/idents.mli b/compiler/global/idents.mli
index 571c665..bc38346 100644
--- a/compiler/global/idents.mli
+++ b/compiler/global/idents.mli
@@ -18,6 +18,9 @@ val ident_compare : ident -> ident -> int
 (** Get the full name of an identifier (it is guaranteed to be unique) *)
 val name : ident -> string
 
+(** Get the source name of an identifier (useful when dealing with signatures *)
+val source_name : ident -> string
+
 (** [gen_fresh pass_name kind_to_string kind]
     generate a fresh ident with a sweet [name].
     It should be used to define a [fresh] function specific to a pass. *)
@@ -27,7 +30,7 @@ val gen_fresh : string -> ('a -> string) -> 'a -> ident
     generates a fresh ident with a sweet [name] *)
 val gen_var : string -> string -> ident
 
-(** [ident_of_name n] returns an identifier corresponding
+(** [ident_of_name n] returns an fresh identifier corresponding
   to a _source_ variable (do not use it for generated variables). *)
 val ident_of_name : string -> ident
 
diff --git a/compiler/global/signature.ml b/compiler/global/signature.ml
index c040ab1..2a57f94 100644
--- a/compiler/global/signature.ml
+++ b/compiler/global/signature.ml
@@ -9,12 +9,15 @@
 (* global data in the symbol tables *)
 open Names
 open Types
-open Clocks
 
 (** Warning: Whenever these types are modified,
     interface_format_version should be incremented. *)
 let interface_format_version = "30"
 
+type ck =
+  | Cbase
+  | Con of ck * constructor_name * name
+
 (** Node argument : inputs and outputs *)
 type arg = {
   a_name  : name option;
@@ -50,6 +53,14 @@ type type_def =
 
 type const_def = { c_type : ty; c_value : static_exp }
 
+let rec ck_to_sck ck =
+  let ck = Clocks.ck_repr ck in
+  match ck with
+    | Clocks.Cbase -> Cbase
+    | Clocks.Con (ck,c,x) -> Con(ck_to_sck ck, c, Idents.source_name x)
+    | _ -> Misc.internal_error "Signature couldn't translate ck" 1
+
+
 let names_of_arg_list l = List.map (fun ad -> ad.a_name) l
 
 let types_of_arg_list l = List.map (fun ad -> ad.a_type) l
diff --git a/compiler/heptagon/hept_utils.ml b/compiler/heptagon/hept_utils.ml
index 8953540..919c449 100644
--- a/compiler/heptagon/hept_utils.ml
+++ b/compiler/heptagon/hept_utils.ml
@@ -19,9 +19,10 @@ open Initial
 open Heptagon
 
 (* Helper functions to create AST. *)
-let mk_exp desc ?(ct_annot = Clocks.invalid_clock) ?(loc = no_location) ty  =
+(* TODO : After switch, all mk_exp should take care of level_ck *)
+let mk_exp desc ?(level_ck = Cbase) ?(ct_annot = None) ?(loc = no_location) ty =
   { e_desc = desc; e_ty = ty; e_ct_annot = ct_annot;
-    e_base_ck = Cbase; e_loc = loc; }
+    e_level_ck = level_ck; e_loc = loc; }
 
 let mk_app ?(params=[]) ?(unsafe=false) op =
   { a_op = op; a_params = params; a_unsafe = unsafe }
diff --git a/compiler/heptagon/heptagon.ml b/compiler/heptagon/heptagon.ml
index 663ed71..4df0227 100644
--- a/compiler/heptagon/heptagon.ml
+++ b/compiler/heptagon/heptagon.ml
@@ -29,8 +29,8 @@ type iterator_type =
 type exp = {
   e_desc      : desc;
   e_ty        : ty;
-  e_ct_annot  : ct;
-  e_base_ck   : ck;
+  e_ct_annot  : ct option; (* exists when a source annotation exists *)
+  e_level_ck  : ck; (* set by the switch pass, represents the base activation of the expression *)
   e_loc       : location }
 
 and desc =
@@ -188,82 +188,4 @@ and interface_desc =
   | Itypedef of type_dec
   | Iconstdef of const_dec
   | Isignature of signature
-(*
-(* Helper functions to create AST. *)
-let mk_exp desc ?(ct_annot = Clocks.invalid_clock) ?(loc = no_location) ty  =
-  { e_desc = desc; e_ty = ty; e_ct_annot = ct_annot;
-    e_base_ck = Cbase; e_loc = loc; }
 
-let mk_app ?(params=[]) ?(unsafe=false) op =
-  { a_op = op; a_params = params; a_unsafe = unsafe }
-
-let mk_op_app ?(params=[]) ?(unsafe=false) ?(reset=None) op args =
-  Eapp(mk_app ~params:params ~unsafe:unsafe op, args, reset)
-
-let mk_type_dec name desc =
-  { t_name = name; t_desc = desc; t_loc = no_location; }
-
-let mk_equation stateful desc =
-  { eq_desc = desc; eq_stateful = stateful; eq_loc = no_location; }
-
-let mk_var_dec ?(last = Var) ?(clock = fresh_clock()) name ty =
-  { v_ident = name; v_type = ty; v_clock = clock;
-    v_last = last; v_loc = no_location }
-
-let mk_block stateful ?(defnames = Env.empty) ?(locals = []) eqs =
-  { b_local = locals; b_equs = eqs; b_defnames = defnames;
-    b_stateful = stateful; b_loc = no_location; }
-
-let dfalse =
-  mk_exp (Econst (mk_static_bool false)) (Tid Initial.pbool)
-let dtrue =
-  mk_exp (Econst (mk_static_bool true)) (Tid Initial.pbool)
-
-let mk_ifthenelse e1 e2 e3 =
-  { e3 with e_desc = mk_op_app Eifthenelse [e1; e2; e3] }
-
-let mk_simple_equation stateful pat e =
-  mk_equation stateful (Eeq(pat, e))
-
-let mk_switch_equation stateful e l =
-  mk_equation stateful (Eswitch (e, l))
-
-
-let mk_signature name ins outs stateful params loc =
-  { sig_name = name;
-    sig_inputs = ins;
-    sig_stateful = stateful;
-    sig_outputs = outs;
-    sig_params = params;
-    sig_loc = loc }
-
-let mk_node
-    ?(input = []) ?(output = []) ?(contract = None) ?(local = [])
-    ?(stateful = true) ?(loc = no_location) ?(param = []) ?(constraints = [])
-    name block =
-  { n_name = name;
-    n_stateful = stateful;
-    n_input = input;
-    n_output = output;
-    n_contract = contract;
-    n_block = block;
-    n_loc = loc;
-    n_params = param;
-    n_params_constraints = constraints }
-
-(** @return the set of variables defined in [pat]. *)
-let vars_pat pat =
-  let rec _vars_pat locals acc = function
-    | Evarpat x ->
-        if (IdentSet.mem x locals) or (IdentSet.mem x acc)
-        then acc
-        else IdentSet.add x acc
-    | Etuplepat pat_list -> List.fold_left (_vars_pat locals) acc pat_list
-  in _vars_pat IdentSet.empty IdentSet.empty pat
-
-(** @return whether an object of name [n] belongs to
-    a list of [var_dec]. *)
-let rec vd_mem n = function
-  | [] -> false
-  | vd::l -> vd.v_ident = n or (vd_mem n l)
-*)
diff --git a/compiler/heptagon/parsing/hept_parser.mly b/compiler/heptagon/parsing/hept_parser.mly
index 7e97d28..9db93af 100644
--- a/compiler/heptagon/parsing/hept_parser.mly
+++ b/compiler/heptagon/parsing/hept_parser.mly
@@ -193,8 +193,8 @@ nonmt_params:
 ;
 
 param:
-  | ident_list COLON ty_ident
-      { List.map (fun id -> mk_var_dec id $3 Var (Loc($startpos,$endpos))) $1 }
+  | idl=ident_list COLON ty=ty_ident ck=ck
+      { List.map (fun id -> mk_var_dec id ty ck Var (Loc($startpos,$endpos))) idl }
 ;
 
 out_params:
@@ -248,12 +248,12 @@ loc_params:
 
 
 var_last:
-  | ident_list COLON ty_ident
-      { List.map (fun id -> mk_var_dec id $3 Var (Loc($startpos,$endpos))) $1 }
-  | LAST IDENT COLON ty_ident EQUAL exp
-      { [ mk_var_dec $2 $4 (Last(Some($6))) (Loc($startpos,$endpos)) ] }
-  | LAST IDENT COLON ty_ident
-      { [ mk_var_dec $2 $4 (Last(None)) (Loc($startpos,$endpos)) ] }
+  | idl=ident_list COLON ty=ty_ident ck=ck
+      { List.map (fun id -> mk_var_dec id ty ck Var (Loc($startpos,$endpos))) idl }
+  | LAST id=IDENT COLON ty=ty_ident ck=ck EQUAL e=exp
+      { [ mk_var_dec id ty ck (Last(Some(e))) (Loc($startpos,$endpos)) ] }
+  | LAST id=IDENT COLON ty=ty_ident ck=ck
+      { [ mk_var_dec id ty ck (Last(None)) (Loc($startpos,$endpos)) ] }
 ;
 
 ident_list:
@@ -268,9 +268,13 @@ ty_ident:
       { Tarray ($1, $3) }
 ;
 
+ck:
+  | /*empty */  { None }
+  | ON ck=on_ck    { Some ck }
+
 on_ck:
-  | /*empty */                                              { Cbase }
-  | b=on_ck ON c=constructor_or_bool LPAREN x=IDENT RPAREN  { Con (b,c,x) }
+  | c=constructor_or_bool LPAREN x=IDENT RPAREN             { Con(Cbase,c,x) }
+  | b=on_ck ON c=constructor_or_bool LPAREN x=IDENT RPAREN  { Con(b,c,x) }
 
 equs:
   | /* empty */                      { [] }
@@ -630,8 +634,8 @@ nonmt_params_signature:
 ;
 
 param_signature:
-  | IDENT COLON ty_ident ck=on_ck { mk_arg (Some $1) $3 ck }
-  | ty_ident ck=on_ck { mk_arg None $1 ck }
+  | IDENT COLON ty_ident ck=ck { mk_arg (Some $1) $3 ck }
+  | ty_ident ck=ck { mk_arg None $1 ck }
 ;
 
 %%
diff --git a/compiler/heptagon/parsing/hept_parsetree.ml b/compiler/heptagon/parsing/hept_parsetree.ml
index 68a26c2..6394fb9 100644
--- a/compiler/heptagon/parsing/hept_parsetree.ml
+++ b/compiler/heptagon/parsing/hept_parsetree.ml
@@ -65,11 +65,14 @@ and ck =
   | Cbase
   | Con of ck * constructor_name * var_name
 
+and ct =
+  | Ck of ck
+  | Cprod of ct list
 
 and exp =
-  { e_desc : edesc;
-    e_ct_annot : Clocks.ct;
-    e_loc  : location }
+  { e_desc     : edesc;
+    e_ct_annot : ct option ;
+    e_loc      : location }
 
 and edesc =
   | Econst of static_exp
@@ -144,10 +147,11 @@ and present_handler =
     p_block : block; }
 
 and var_dec =
-  { v_name : var_name;
-    v_type : ty;
-    v_last : last;
-    v_loc  : location; }
+  { v_name  : var_name;
+    v_type  : ty;
+    v_clock : ck option;
+    v_last  : last;
+    v_loc   : location; }
 
 and last = Var | Last of exp option
 
@@ -198,7 +202,7 @@ and program_desc =
 
 type arg =
   { a_type  : ty;
-    a_clock : ck;
+    a_clock : ck option;
     a_name  : var_name option }
 
 type signature =
@@ -223,7 +227,7 @@ and interface_desc =
 
 (* {3 Helper functions to create AST} *)
 
-let mk_exp desc ?(ct_annot = Clocks.invalid_clock) loc =
+let mk_exp desc ?(ct_annot = None) loc =
   { e_desc = desc; e_ct_annot = ct_annot; e_loc = loc }
 
 let mk_app op params =
@@ -256,8 +260,8 @@ let mk_equation desc loc =
 let mk_interface_decl desc loc =
   { interf_desc = desc; interf_loc = loc }
 
-let mk_var_dec name ty last loc =
-  { v_name = name; v_type = ty;
+let mk_var_dec name ty ck last loc =
+  { v_name = name; v_type = ty; v_clock = ck;
     v_last = last; v_loc = loc }
 
 let mk_block locals eqs loc =
diff --git a/compiler/heptagon/parsing/hept_scoping.ml b/compiler/heptagon/parsing/hept_scoping.ml
index 6ba7b7a..b50c3f0 100644
--- a/compiler/heptagon/parsing/hept_scoping.ml
+++ b/compiler/heptagon/parsing/hept_scoping.ml
@@ -233,13 +233,25 @@ let rec translate_type loc ty =
   with
     | ScopingError err -> message loc err
 
+let rec translate_some_clock loc env ck = match ck with
+  | None -> Clocks.fresh_clock()
+  | Some(ck) -> translate_clock loc env ck
+
+and translate_clock loc env ck = match ck with
+  | Cbase -> Clocks.Cbase
+  | Con(ck,c,x) -> Clocks.Con(translate_clock loc env ck, qualify_constrs c, Rename.var loc env x)
+
+let rec translate_ct loc env ct = match ct with
+  | Ck ck -> Clocks.Ck (translate_clock loc env ck)
+  | Cprod c_l -> Clocks.Cprod (List.map (translate_ct loc env) c_l)
+
 
 let rec translate_exp env e =
   try
     { Heptagon.e_desc = translate_desc e.e_loc env e.e_desc;
       Heptagon.e_ty = Types.invalid_type;
-      Heptagon.e_base_ck = Clocks.Cbase;
-      Heptagon.e_ct_annot = e.e_ct_annot;
+      Heptagon.e_level_ck = Clocks.Cbase;
+      Heptagon.e_ct_annot = Misc.optional (translate_ct e.e_loc env) e.e_ct_annot;
       Heptagon.e_loc = e.e_loc }
   with ScopingError(error) -> message e.e_loc error
 
@@ -374,9 +386,10 @@ and translate_var_dec env vd =
     { Heptagon.v_ident = Rename.var vd.v_loc env vd.v_name;
       Heptagon.v_type = translate_type vd.v_loc vd.v_type;
       Heptagon.v_last = translate_last vd.v_last;
-      Heptagon.v_clock = Clocks.fresh_clock(); (* TODO add clock annotations *)
+      Heptagon.v_clock = translate_some_clock vd.v_loc env vd.v_clock;
       Heptagon.v_loc = vd.v_loc }
 
+(** [env] should contain the declared variables prior to this translation *)
 and translate_vd_list env =
   List.map (translate_var_dec env)
 
@@ -398,26 +411,27 @@ let params_of_var_decs =
                         (translate_type vd.v_loc vd.v_type))
 
 let args_of_var_decs =
-  List.map (fun vd -> Signature.mk_arg
-                        (Some vd.v_name)
-                        (translate_type vd.v_loc vd.v_type)
-                        Clocks.Cbase) (* before clocking and without annotations, default choice.*)
+  (* before the clocking the clock is wrong in the signature *)
+ List.map (fun vd -> Signature.mk_arg (Some (Idents.source_name vd.Heptagon.v_ident))
+                                      vd.Heptagon.v_type Signature.Cbase)
+
 
 let translate_node node =
   let n = current_qual node.n_name in
   Idents.enter_node n;
-  (* Inputs and outputs define the initial local env *)
-  let env0 = Rename.append Rename.empty (node.n_input @ node.n_output) in
   let params = params_of_var_decs node.n_params in
-  let inputs = translate_vd_list env0 node.n_input in
+  let input_env = Rename.append Rename.empty (node.n_input) in
+  (* inputs should refer only to inputs *)  
+  let inputs = translate_vd_list input_env node.n_input in
+  (* Inputs and outputs define the initial local env *)  
+  let env0 = Rename.append input_env node.n_output in
   let outputs = translate_vd_list env0 node.n_output in
   let b, env = translate_block env0 node.n_block in
-  let contract =
-    Misc.optional (translate_contract env) node.n_contract in
-  (* the env of the block is used in the contract translation *)
+  (* the env of the block is used in the contract translation *) 
+  let contract = Misc.optional (translate_contract env) node.n_contract in
   (* add the node signature to the environment *)
-  let i = args_of_var_decs node.n_input in
-  let o = args_of_var_decs node.n_output in
+  let i = args_of_var_decs inputs in
+  let o = args_of_var_decs outputs in
   let p = params_of_var_decs node.n_params in
   add_value n (Signature.mk_node i o node.n_stateful p);
   { Heptagon.n_name = n;
@@ -483,14 +497,30 @@ let translate_program p =
     Heptagon.p_desc = desc; }
 
 let translate_signature s =
-  let translate_arg a =
-    Signature.mk_arg a.a_name
-      (translate_type s.sig_loc a.a_type)
-      (translate_clock s.sig_loc a.a_clock))
+  (* helper functions, having [env] as being the list of existing var names *)
+  let rec append env sa_l = match sa_l with
+    | [] -> env
+    | sa::sa_l -> match sa.a_name with
+        | None -> append env sa_l
+        | Some x -> append (x::env) sa_l
+  and translate_some_clock loc env ck = match ck with
+    | None -> Signature.Cbase
+    | Some ck -> translate_clock loc env ck
+  and translate_clock loc env ck = match ck with
+    | Cbase -> Signature.Cbase
+    | Con(ck,c,x) ->
+        if not (List.mem x env)
+        then message loc (Evar_unbound x)
+        else Signature.Con(translate_clock loc env ck, qualify_constrs c, x)
+  and translate_arg env a =
+    Signature.mk_arg a.a_name (translate_type s.sig_loc a.a_type)
+                              (translate_some_clock s.sig_loc env a.a_clock)
   in
   let n = current_qual s.sig_name in
-  let i = List.map translate_arg s.sig_inputs in
-  let o = List.map translate_arg s.sig_outputs in
+  let env = append [] s.sig_inputs in
+  let i = List.map (translate_arg env) s.sig_inputs in
+  let env = append env s.sig_outputs in
+  let o = List.map (translate_arg env) s.sig_outputs in
   let p = params_of_var_decs s.sig_params in
   add_value n (Signature.mk_node i o s.sig_stateful p);
   mk_signature n i o s.sig_stateful p s.sig_loc
diff --git a/compiler/heptagon/transformations/switch.ml b/compiler/heptagon/transformations/switch.ml
index 6d58091..b3ac085 100644
--- a/compiler/heptagon/transformations/switch.ml
+++ b/compiler/heptagon/transformations/switch.ml
@@ -105,7 +105,7 @@ let current_level env = match env with
 
 (** Set the base clock of an expression to the current level of the [env] *)
 let annot_exp e env =
-  { e with e_base_ck = current_level env }
+  { e with e_level_ck = current_level env }
 
 end
 
diff --git a/compiler/main/hept2mls.ml b/compiler/main/hept2mls.ml
index 984291a..13db8cf 100644
--- a/compiler/main/hept2mls.ml
+++ b/compiler/main/hept2mls.ml
@@ -104,45 +104,46 @@ let rec translate_extvalue e =
           mk_extvalue (Wfield (translate_extvalue e, fn))
     | _ -> Error.message e.Heptagon.e_loc Error.Enormalization
 
-let translate
-    ({ Heptagon.e_desc = desc; Heptagon.e_ty = ty;
-      Heptagon.e_loc = loc } as e) =
-  let mk_exp = mk_exp ~loc:loc in
-  match desc with
+let translate ({ Heptagon.e_desc = desc; Heptagon.e_ty = ty; Heptagon.e_level_ck = b_ck;
+                 Heptagon.e_ct_annot = a_ct; Heptagon.e_loc = loc } as e) =
+  let desc = match desc with
     | Heptagon.Econst _
     | Heptagon.Evar _
     | Heptagon.Ewhen _
     | Heptagon.Eapp({ Heptagon.a_op = Heptagon.Efield }, _, _) ->
         let w = translate_extvalue e in
-          mk_exp ty (Eextvalue w)
+        Eextvalue w
     | Heptagon.Epre(None, e) ->
-        mk_exp ty (Efby(None, translate_extvalue e))
+        Efby(None, translate_extvalue e)
     | Heptagon.Epre(Some c, e) ->
-        mk_exp ty (Efby(Some c, translate_extvalue e))
+        Efby(Some c, translate_extvalue e)
     | Heptagon.Efby ({ Heptagon.e_desc = Heptagon.Econst c }, e) ->
-        mk_exp ty (Efby(Some c, translate_extvalue e))
+        Efby(Some c, translate_extvalue e)
     | Heptagon.Estruct f_e_list ->
         let f_e_list = List.map
           (fun (f, e) -> (f, translate_extvalue e)) f_e_list in
-        mk_exp ty (Estruct f_e_list)
+        Estruct f_e_list
     | Heptagon.Eapp({ Heptagon.a_op = Heptagon.Earrow }, _, _) ->
          Error.message loc Error.Eunsupported_language_construct
     | Heptagon.Eapp(app, e_list, reset) ->
-        mk_exp ty (Eapp (translate_app app,
-                                     List.map translate_extvalue e_list,
-                                     translate_reset reset))
+        Eapp (translate_app app, List.map translate_extvalue e_list, translate_reset reset)
     | Heptagon.Eiterator(it, app, n, pe_list, e_list, reset) ->
-        mk_exp ty
-          (Eiterator (translate_iterator_type it,
+        Eiterator (translate_iterator_type it,
                     translate_app app, n,
                     List.map translate_extvalue pe_list,
                     List.map translate_extvalue e_list,
-                    translate_reset reset))
+                    translate_reset reset)
     | Heptagon.Efby _
     | Heptagon.Elast _ ->
         Error.message loc Error.Eunsupported_language_construct
     | Heptagon.Emerge (x, c_e_list) ->
-        mk_exp ty (Emerge (x, List.map (fun (c,e)-> c, translate_extvalue e) c_e_list))
+        Emerge (x, List.map (fun (c,e)-> c, translate_extvalue e) c_e_list)
+  in
+  match a_ct with
+    | None -> mk_exp b_ck ty ~loc:loc desc
+    | Some ct -> mk_exp b_ck ty ~ct:ct ~loc:loc desc
+
+
 
 let rec translate_pat = function
   | Heptagon.Evarpat(n) -> Evarpat n
@@ -167,8 +168,8 @@ let translate_contract contract =
              Heptagon.c_controllables = l_c } ->
         Some { c_local = List.map translate_var v;
                c_eq = List.map translate_eq eq_list;
-               c_assume = translate e_a;
-               c_enforce = translate e_g;
+               c_assume = translate_extvalue e_a;
+               c_enforce = translate_extvalue e_g;
                c_controllables = List.map translate_var l_c }
 
 let node n =
diff --git a/compiler/main/mls2obc.ml b/compiler/main/mls2obc.ml
index 007315b..83e09c6 100644
--- a/compiler/main/mls2obc.ml
+++ b/compiler/main/mls2obc.ml
@@ -11,12 +11,12 @@
 open Misc
 open Names
 open Idents
-open Clocks
 open Signature
 open Obc
 open Obc_utils
 open Obc_mapfold
 open Types
+open Clocks
 open Static
 open Initial
 
@@ -361,7 +361,7 @@ let empty_call_context = None
     [v] var decs *)
 let rec translate_eq map call_context { Minils.eq_lhs = pat; Minils.eq_rhs = e }
     (v, si, j, s) =
-  let { Minils.e_desc = desc; Minils.e_ck = ck; Minils.e_loc = loc } = e in
+  let { Minils.e_desc = desc; Minils.e_base_ck = ck; Minils.e_loc = loc } = e in
   match (pat, desc) with
     | Minils.Evarpat n, Minils.Efby (opt_c, e) ->
         let x = var_from_name map n in
diff --git a/compiler/minils/analysis/clocking.ml b/compiler/minils/analysis/clocking.ml
index 3b3d774..fef4416 100644
--- a/compiler/minils/analysis/clocking.ml
+++ b/compiler/minils/analysis/clocking.ml
@@ -8,9 +8,19 @@
 (**************************************************************************)
 (* clock checking *)
 
+(* v_clock is expected to contain correct clocks before entering here :
+     either explicit with Cbase representing the node activation clock
+     or fresh_clock() for unannoted variables.
+  Idem for e_ct : if explicit, it represents a clock annotation.
+  Unification is done on this mutable fields.
+  e_base_ck is set according to node signatures.
+  
+ *)
+
 open Misc
 open Idents
 open Minils
+open Global_printer
 open Mls_printer
 open Signature
 open Types
@@ -19,139 +29,152 @@ open Location
 open Format
 
 (** Error Kind *)
-type error_kind = | Etypeclash of ct * ct
+type error_kind = | Etypeclash of ct * ct | Eclockclash of ck * ck | Edefclock
 
 let error_message loc = function
   | Etypeclash (actual_ct, expected_ct) ->
       Format.eprintf "%aClock Clash: this expression has clock %a,@\n\
                         but is expected to have clock %a.@."
         print_location loc
-        print_clock actual_ct
-        print_clock expected_ct;
+        print_ct actual_ct
+        print_ct expected_ct;
+      raise Errors.Error
+  | Eclockclash (actual_ck, expected_ck) ->
+      Format.eprintf "%aClock Clash: this value has clock %a,@\n\
+                        but is exprected to have clock %a.@."
+        print_location loc
+        print_ck actual_ck
+        print_ck expected_ck;
+      raise Errors.Error
+  | Edefclock ->
+      Format.eprintf "%aArguments defining clocks should be given as names@."
+        print_location loc;
       raise Errors.Error
 
 
-let typ_of_name h x = Env.find x h
+let ck_of_name h x = Env.find x h
 
 let rec typing_extvalue h w =
-  let ct = match w.w_desc with
-    | Wconst se -> skeleton (fresh_clock ()) se.se_ty
-    | Wvar x -> Ck (typ_of_name h x)
+  let ck = match w.w_desc with
+    | Wconst se -> fresh_clock()
+    | Wvar x -> ck_of_name h x
     | Wwhen (w1, c, n) ->
-        let ck_n = typ_of_name h n in
-        (expect h (skeleton ck_n w1.w_ty) w1; skeleton (Con (ck_n, c, n)) w1.w_ty)
+        let ck_n = ck_of_name h n in
+        expect_extvalue h ck_n w1;
+        Con (ck_n, c, n)
     | Wfield (w1, f) ->
-        let ck = fresh_clock () in
-        let ct = skeleton ck w1.w_ty in (expect h (Ck ck) w1; ct)
-  in (w.w_ck <- ckofct ct; ct)
+        typing_extvalue h w1
+  in
+  w.w_ck <- ck;
+  ck
 
-and expect h expected_ty e =
-  let actual_ty = typing_extvalue h e in
-  try unify actual_ty expected_ty
+and expect_extvalue h expected_ck e =
+  let actual_ck = typing_extvalue h e in
+  try unify_ck actual_ck expected_ck
   with
   | Unify -> eprintf "%a : " print_extvalue e;
-      error_message e.w_loc (Etypeclash (actual_ty, expected_ty))
+      error_message e.w_loc (Eclockclash (actual_ck, expected_ck))
 
-let rec typing h e =
-  let ct = match e.e_desc with
-    | Eextvalue w -> typing_extvalue h w
-    | Efby (_, e) -> typing_extvalue h e
-    | Eapp({a_op = op}, args, r) ->
-        let ck = match r with
-          | None -> fresh_clock ()
-          | Some(reset) -> typ_of_name h reset in
-        typing_op op args h e ck
-    (* Typed exactly as a fun or a node... *)
-    | Eiterator (_, _, _, pargs, args, r) ->
-        let ck = match r with
-          | None -> fresh_clock()
-          | Some(reset) -> typ_of_name h reset
-        in
-          List.iter (expect h (Ck ck)) pargs;
-          List.iter (expect h (Ck ck)) args;
-          skeleton ck e.e_ty
-    | Emerge (n, c_e_list) ->
-        let ck_c = typ_of_name h n in
-        (typing_c_e_list h ck_c n c_e_list; skeleton ck_c e.e_ty)
+let rec typing_pat h = function
+  | Evarpat x -> Ck (ck_of_name h x)
+  | Etuplepat pat_list -> Cprod (List.map (typing_pat h) pat_list)
+
+
+let typing_app h base pat op w_list = match op with
+  | Earray_fill | Eselect | Eselect_dyn | Eselect_trunc | Eupdate | Eequal
+  | Eselect_slice | Econcat | Earray | Efield_update | Eifthenelse ->
+      List.iter (expect_extvalue h base) w_list;
+      Ck base
+  | ( Efun f | Enode f) ->
+      let node = Modules.find_value f in
+      let pat_id_list = Mls_utils.ident_list_of_pat pat in
+      let rec build_env a_l v_l env = match a_l, v_l with
+        | [],[] -> env
+        | a::a_l, v::v_l -> (match a.a_name with
+          | None -> build_env a_l v_l env
+          | Some n -> build_env a_l v_l ((n,v)::env))
+        | _ -> Misc.internal_error "Clocking, non matching signature" 2
+      in
+      let env_pat = build_env node.node_outputs pat_id_list [] in
+      let env_args = build_env node.node_inputs w_list [] in
+      (* implement with Cbase as base, replace name dep by ident dep *)
+      let rec sigck_to_ck sck = match sck with
+        | Signature.Cbase -> base
+        | Signature.Con (sck,c,x) ->
+            (* find x in the envs : *)
+            let id = try List.assoc x env_pat
+                     with Not_found ->
+                       try
+                         let w = List.assoc x env_args in
+                         (match w.w_desc with
+                           | Wvar id -> id
+                           | _ -> error_message w.w_loc Edefclock)
+                       with Not_found ->
+                         Misc.internal_error "Clocking, non matching signature" 3
+            in
+            Clocks.Con (sigck_to_ck sck, c, id)
+      in
+      List.iter2 (fun a w -> expect_extvalue h (sigck_to_ck a.a_clock) w) node.node_inputs w_list;
+      Clocks.prod (List.map (fun a -> sigck_to_ck a.a_clock) node.node_outputs)
+
+
+let typing_eq h { eq_lhs = pat; eq_rhs = e } =
+  (* typing the expression *)
+  let ct,base = match e.e_desc with
+    | Eextvalue w 
+    | Efby (_, w) ->
+        let ck = typing_extvalue h w in
+        Ck ck, ck
+    | Emerge (x, c_e_list) ->
+        let ck = ck_of_name h x in
+        List.iter (fun (c,e) -> expect_extvalue h (Con (ck,c,x)) e) c_e_list;
+        Ck ck, ck
     | Estruct l ->
         let ck = fresh_clock () in
-        (List.iter
-           (fun (_, e) -> let ct = skeleton ck e.w_ty in expect h ct e) l;
-         Ck ck)
-  in (e.e_ck <- ckofct ct; ct)
+        List.iter (fun (_, e) -> expect_extvalue h ck e) l;
+        Ck ck, ck
+    | Eapp({a_op = op}, args, r) ->
+        let ck_r = match r with
+          | None -> fresh_clock ()
+          | Some(reset) -> ck_of_name h reset in
+        let ct = typing_app h ck_r pat op args in
+        ct, ck_r    
+    | Eiterator (_, _, _, pargs, args, r) ->
+        (* Typed exactly as a fun or a node... *)
+        let ck_r = match r with
+          | None -> fresh_clock()
+          | Some(reset) -> ck_of_name h reset
+        in
+        List.iter (expect_extvalue h ck_r) pargs;
+        List.iter (expect_extvalue h ck_r) args;
+        (*TODO*)
+        Ck ck_r, ck_r
+  in
+  e.e_base_ck <- base;
+  begin
+    try unify ct e.e_ct
+    with Unify ->
+      eprintf "Incoherent clock annotation.@\n";
+      error_message e.e_loc (Etypeclash (ct,e.e_ct))
+  end;
+  e.e_ct <- ct;
+ (* typing the full equation *)
+  let pat_ct = typing_pat h pat in
+  begin
+    try unify ct pat_ct
+    with Unify ->
+      eprintf "Incoherent clock between right and left side of the equation@\n";
+      error_message e.e_loc (Etypeclash (ct, pat_ct))
+  end
 
-and typing_op op e_list h e ck = match op with
-  | (Eequal | Efun _ | Enode _) -> (*LA*)
-      List.iter (fun e -> expect h (skeleton ck e.w_ty) e) e_list;
-      skeleton ck e.e_ty
-  | Eifthenelse ->
-      let e1, e2, e3 = assert_3 e_list in
-      let ct = skeleton ck e.e_ty
-      in (expect h (Ck ck) e1; expect h ct e2; expect h ct e3; ct)
-  | Efield_update ->
-      let e1, e2 = assert_2 e_list in
-      let ct = skeleton ck e.e_ty
-      in (expect h (Ck ck) e1; expect h ct e2; ct)
-  | Earray ->
-      (List.iter (expect h (Ck ck)) e_list; skeleton ck e.e_ty)
-  | Earray_fill -> let e = assert_1 e_list in typing_extvalue h e
-  | Eselect -> let e = assert_1 e_list in typing_extvalue h e
-  | Eselect_dyn -> (* TODO defe not treated ? *)
-      let e1, defe, idx = assert_2min e_list in
-      let ct = skeleton ck e1.w_ty
-      in (List.iter (expect h ct) (e1::defe::idx); ct)
-  | Eselect_trunc ->
-      let e1, idx = assert_1min e_list in
-      let ct = skeleton ck e1.w_ty
-      in (List.iter (expect h ct) (e1::idx); ct)
-  | Eupdate ->
-      let e1, e2, idx = assert_2min e_list in
-      let ct = skeleton ck e.e_ty
-      in (expect h (Ck ck) e1; expect h ct e2; List.iter (expect h ct) idx; ct)
-  | Eselect_slice -> let e = assert_1 e_list in typing_extvalue h e
-  | Econcat ->
-      let e1, e2 = assert_2 e_list in
-      let ct = skeleton ck e.e_ty
-      in (expect h (Ck ck) e1; expect h ct e2; ct)
 
-and typing_c_e_list h ck_c n c_e_list =
-  let rec typrec =
-    function
-      | [] -> ()
-      | (c, e) :: c_e_list ->
-          (expect h (skeleton (Con (ck_c, c, n)) e.w_ty) e; typrec c_e_list)
-  in typrec c_e_list
+let typing_eqs h eq_list = List.iter (typing_eq h) eq_list
 
-let expect_exp h expected_ty e =
-  let actual_ty = typing h e in
-  try unify actual_ty expected_ty
-  with
-  | Unify -> eprintf "%a : " print_exp e;
-      error_message e.e_loc (Etypeclash (actual_ty, expected_ty))
+let append_env h vds =
+  List.fold_left (fun h { v_ident = n; v_clock = ck } -> Env.add n ck h) h vds
 
-let rec typing_pat h =
-  function
-    | Evarpat x -> Ck (typ_of_name h x)
-    | Etuplepat pat_list -> Cprod (List.map (typing_pat h) pat_list)
 
-let typing_eqs h eq_list = (*TODO FIXME*)
-  let typing_eq { eq_lhs = pat; eq_rhs = e } =
-    let ty_pat = typing_pat h pat in
-    (try expect_exp h ty_pat e with
-      | Errors.Error -> (* DEBUG *)
-          Format.eprintf "Complete expression: %a@\nClock pattern: %a@."
-            Mls_printer.print_exp e
-            Mls_printer.print_clock ty_pat;
-          raise Errors.Error)
-  in List.iter typing_eq eq_list
-
-let build h dec =
-  List.fold_left (fun h { v_ident = n } -> Env.add n (fresh_clock ()) h) h dec
-
-let sbuild h dec base =
-  List.fold_left (fun h { v_ident = n } -> Env.add n base h) h dec
-
-let typing_contract h contract base =
+let typing_contract h contract =
   match contract with
     | None -> h
     | Some { c_local = l_list;
@@ -159,32 +182,25 @@ let typing_contract h contract base =
              c_assume = e_a;
              c_enforce = e_g;
              c_controllables = c_list } ->
-        let h' = build h l_list in
+        let h' = append_env h l_list in
         (* assumption *)
         (* property *)
         typing_eqs h' eq_list;
-        expect_exp h' (Ck base) e_a;
-        expect_exp h' (Ck base) e_g;
-        sbuild h c_list base
+        expect_extvalue h' Cbase e_a;
+        expect_extvalue h' Cbase e_g;
+        append_env h c_list
 
-let typing_node ({ n_input = i_list;
-                   n_output = o_list;
-                   n_contract = contract;
-                   n_local = l_list;
-                   n_equs = eq_list
-                 } as node) =
-  let base = Cbase in
-  let h = sbuild Env.empty i_list base in
-  let h = sbuild h o_list base in
-  let h = typing_contract h contract base in
-  let h = build h l_list in
-  (typing_eqs h eq_list;
-   (*update clock info in variables descriptions *)
-   let set_clock vd = { vd with v_clock = ck_repr (Env.find vd.v_ident h) } in
-   { (node) with
-       n_input = List.map set_clock i_list;
-       n_output = List.map set_clock o_list;
-       n_local = List.map set_clock l_list })
+let typing_node node =
+  let h = append_env Env.empty node.n_input in
+  let h = append_env h node.n_output in
+  let h = typing_contract h node.n_contract in
+  let h = append_env h node.n_local in
+  (typing_eqs h node.n_equs;
+  (*update clock info in variables descriptions *)
+  let set_clock vd = { vd with v_clock = ck_repr (Env.find vd.v_ident h) } in
+  { node with n_input = List.map set_clock node.n_input;
+              n_output = List.map set_clock node.n_output;
+              n_local = List.map set_clock node.n_local })
 
 let program p =
   let program_desc pd = match pd with
diff --git a/compiler/minils/minils.ml b/compiler/minils/minils.ml
index fbd38ea..4ffcd2f 100644
--- a/compiler/minils/minils.ml
+++ b/compiler/minils/minils.ml
@@ -46,16 +46,18 @@ and extvalue = {
   w_loc       : location }
 
 and extvalue_desc =
-  | Wconst of static_exp
+  | Wconst of static_exp (*no tuple*)
   | Wvar of var_ident
   | Wfield of extvalue * field_name
   | Wwhen of extvalue * constructor_name * var_ident (** extvalue when Constructor(ident) *)
 
 and exp = {
-  e_desc      : edesc;
-  mutable e_ck: ck;
-  e_ty        : ty;
-  e_loc       : location }
+  e_desc            : edesc;
+  e_level_ck        : ck; (* when no data dep, execute the exp on this clock (set by [switch] *)
+  mutable e_base_ck : ck;
+  mutable e_ct      : ct;
+  e_ty              : ty;
+  e_loc             : location }
 
 and edesc =
   | Eextvalue of extvalue
@@ -107,8 +109,8 @@ type var_dec = {
   v_loc : location }
 
 type contract = {
-  c_assume : exp;
-  c_enforce : exp;
+  c_assume : extvalue;
+  c_enforce : extvalue;
   c_controllables : var_dec list;
   c_local : var_dec list;
   c_eq : eq list }
@@ -119,8 +121,6 @@ type node_dec = {
   n_input  : var_dec list;
   n_output : var_dec list;
   n_contract : contract option;
-  (* GD: inglorious hack for controller call
-  mutable n_controller_call : var_ident list * var_ident list; *)
   n_local  : var_dec list;
   n_equs   : eq list;
   n_loc    : location;
@@ -150,9 +150,8 @@ let mk_extvalue ~ty ?(clock = fresh_clock()) ?(loc = no_location) desc =
   { w_desc = desc; w_ty = ty;
     w_ck = clock; w_loc = loc }
 
-let mk_exp ty ?(clock = fresh_clock()) ?(loc = no_location) desc =
-  { e_desc = desc; e_ty = ty;
-    e_ck = clock; e_loc = loc }
+let mk_exp level_ck ty ?(ck = Cbase) ?(ct = fresh_ct ty) ?(loc = no_location) desc =
+  { e_desc = desc; e_ty = ty; e_level_ck = level_ck; e_base_ck = ck; e_ct = ct; e_loc = loc }
 
 let mk_var_dec ?(loc = no_location) ?(clock = fresh_clock()) ident ty =
   { v_ident = ident; v_type = ty; v_clock = clock; v_loc = loc }
diff --git a/compiler/minils/mls_mapfold.ml b/compiler/minils/mls_mapfold.ml
index 2575d0d..0cb5d02 100644
--- a/compiler/minils/mls_mapfold.ml
+++ b/compiler/minils/mls_mapfold.ml
@@ -136,8 +136,8 @@ and var_decs funs acc vds = mapfold (var_dec_it funs) acc vds
 
 and contract_it funs acc c = funs.contract funs acc c
 and contract funs acc c =
-  let c_assume, acc = exp_it funs acc c.c_assume in
-  let c_enforce, acc = exp_it funs acc c.c_enforce in
+  let c_assume, acc = extvalue_it funs acc c.c_assume in
+  let c_enforce, acc = extvalue_it funs acc c.c_enforce in
   let c_local, acc = var_decs_it funs acc c.c_local in
   let c_eq, acc = eqs_it funs acc c.c_eq in
   { c with
diff --git a/compiler/minils/mls_printer.ml b/compiler/minils/mls_printer.ml
index 40ad008..aaa28e8 100644
--- a/compiler/minils/mls_printer.ml
+++ b/compiler/minils/mls_printer.ml
@@ -1,11 +1,11 @@
 open Misc
 open Names
+open Signature
 open Idents
 open Types
 open Clocks
 open Static
 open Format
-open Signature
 open Global_printer
 open Pp_tools
 open Minils
@@ -27,7 +27,7 @@ let rec print_pat ff = function
   | Evarpat n -> print_ident ff n
   | Etuplepat pat_list ->
       fprintf ff "@[<2>(%a)@]" (print_list_r print_pat """,""") pat_list
-
+(*
 let rec print_ck ff = function
   | Cbase -> fprintf ff "base"
   | Con (ck, c, n) ->
@@ -35,11 +35,11 @@ let rec print_ck ff = function
   | Cvar { contents = Cindex _ } -> fprintf ff "base"
   | Cvar { contents = Clink ck } -> print_ck ff ck
 
-let rec print_clock ff = function
+let rec print_ct ff = function
   | Ck ck -> print_ck ff ck
   | Cprod ct_list ->
       fprintf ff "@[<2>(%a)@]" (print_list_r print_clock """ *""") ct_list
-
+*)
 let print_vd ff { v_ident = n; v_type = ty; v_clock = ck } =
   if !Compiler_options.full_type_info then
     fprintf ff "%a : %a :: %a" print_ident n print_type ty print_ck ck
@@ -86,7 +86,7 @@ and print_trunc_index ff idx =
 and print_exp ff e =
   if !Compiler_options.full_type_info then
     fprintf ff "(%a : %a :: %a)"
-      print_exp_desc e.e_desc print_type e.e_ty print_ck e.e_ck
+      print_exp_desc e.e_desc print_type e.e_ty print_ct e.e_ct
   else fprintf ff "%a" print_exp_desc e.e_desc
 
 and print_every ff reset =
@@ -180,7 +180,7 @@ and print_tag_w_list ff tag_w_list =
 and print_eq ff { eq_lhs = p; eq_rhs = e } =
   if !Compiler_options.full_type_info
   then fprintf ff "@[<2>%a :: %a =@ %a@]"
-    print_pat p  print_ck e.e_ck  print_exp e
+    print_pat p  print_ck e.e_base_ck  print_exp e
   else fprintf ff "@[<2>%a =@ %a@]" print_pat p  print_exp e
 
 
@@ -207,8 +207,8 @@ let print_contract ff { c_local = l; c_eq = eqs;
   fprintf ff "@[<v2>contract@\n%a%a@ assume %a@ enforce %a@ with (%a)@]"
     print_local_vars l
     print_eqs eqs
-    print_exp e_a
-    print_exp e_g
+    print_extvalue e_a
+    print_extvalue e_g
     print_vd_tuple c
 
 
diff --git a/compiler/minils/mls_utils.ml b/compiler/minils/mls_utils.ml
index 6844894..99f2e98 100644
--- a/compiler/minils/mls_utils.ml
+++ b/compiler/minils/mls_utils.ml
@@ -46,10 +46,6 @@ let rec vd_mem n = function
   | [] -> false
   | vd::l -> vd.v_ident = n or (vd_mem n l)
 
-(** @return a signature arguments from the vardecs *)
-let args_of_var_decs vds =
-  List.map (fun vd -> Signature.mk_arg (Some (name vd.v_ident)) vd.v_type) vds
-
 
 (** @return whether [ty] corresponds to a record type. *)
 let is_record_type ty = match ty with
@@ -77,6 +73,10 @@ struct
     | Cbase | Cvar { contents = Cindex _ } -> acc
     | Cvar { contents = Clink ck } -> vars_ck acc ck
 
+  let rec vars_ct acc = function
+    | Ck ck -> vars_ck acc ck
+    | Cprod c_l -> List.fold_left vars_ct acc c_l
+
   let read_extvalue read_funs (is_left, acc_init) w =
     (* recursive call *)
     let _,(_, acc) = Mls_mapfold.extvalue read_funs (is_left, acc_init) w in
@@ -104,7 +104,7 @@ struct
           else acc
       | _ -> acc
     in
-    e, (is_left, vars_ck acc e.e_ck)
+    e, (is_left, vars_ct acc e.e_ct)
 
   let read_exp is_left acc e =
     let _, (_, acc) =
@@ -136,9 +136,7 @@ struct
   let antidep { eq_rhs = e } =
     match e.e_desc with Efby _ -> true | _ -> false
 
-  let clock { eq_rhs = e } = match e.e_desc with
-    | Emerge(_, (_, e) :: _) -> e.w_ck
-    | _ -> e.e_ck
+  let clock { eq_rhs = e } = e.e_base_ck
 
   let head ck =
     let rec headrec ck l =
@@ -191,3 +189,11 @@ module AllDep = Dep.Make
 
 let eq_find id = List.find (fun eq -> List.mem id (Vars.def [] eq))
 
+
+let ident_list_of_pat pat =
+  let rec f acc pat = match pat with
+    | Evarpat id -> id::acc
+    | Etuplepat [] -> acc
+    | Etuplepat (pat::pat_l) -> f (f acc pat) (Etuplepat pat_l)
+  in
+  f [] pat 
diff --git a/compiler/minils/transformations/normalize_mem.ml b/compiler/minils/transformations/normalize_mem.ml
index a54c2a5..21ecfba 100644
--- a/compiler/minils/transformations/normalize_mem.ml
+++ b/compiler/minils/transformations/normalize_mem.ml
@@ -22,8 +22,9 @@ let eq _ (outputs, eqs, env) eq = match eq.eq_lhs, eq.eq_rhs.e_desc with
   | Evarpat x, Efby _ ->
       if Mls_utils.vd_mem x outputs then
         let ty = eq.eq_rhs.e_ty in
+        let ck = eq.eq_rhs.e_base_ck in
         let x_copy = Idents.gen_var "normalize_mem" ("out_"^(Idents.name x)) in
-        let exp_x = mk_exp ty (Eextvalue (mk_extvalue ~ty:ty (Wvar x))) in
+        let exp_x = mk_exp ck ty (Eextvalue (mk_extvalue ~ty:ty (Wvar x))) in
         let eq_copy = { eq with eq_lhs = Evarpat x_copy; eq_rhs = exp_x } in
         let env = Env.add x x_copy env in
           eq, (outputs, eq::eq_copy::eqs, env)