diff --git a/compiler/global/initial.ml b/compiler/global/initial.ml
index 5f25bb6..26d61ec 100644
--- a/compiler/global/initial.ml
+++ b/compiler/global/initial.ml
@@ -20,6 +20,8 @@ let por = Modname({ qual = "Pervasives"; id = "or" })
 let pint = Modname({ qual = "Pervasives"; id = "int" })
 let pfloat = Modname({ qual = "Pervasives"; id = "float" })
 
+let mk_pervasives s = Modname({ qual = "Pervasives"; id = s })
+
 (* build the initial environment *)
 let initialize () =
   List.iter (fun (f, ty) -> Modules.add_type f ty) tglobal;
diff --git a/compiler/global/types.ml b/compiler/global/types.ml
index 53496a5..736e0c3 100644
--- a/compiler/global/types.ml
+++ b/compiler/global/types.ml
@@ -8,11 +8,13 @@
 (**************************************************************************)
 
 open Names
-
+open Location
 
 type ty = | Tprod of ty list | Tid of longname | Tarray of ty * static_exp
 
-type static_exp = { se_desc: static_exp_desc; se_typ:  loc: location }
+type static_exp = { se_desc: static_exp_desc; se_ty: ty; se_loc: location }
+
+and static_exp_desc =
   | Svar of name
   | Sint of int
   | Sfloat of float
@@ -25,7 +27,8 @@ type static_exp = { se_desc: static_exp_desc; se_typ:  loc: location }
 
 let invalid_type = Tprod []
 
-let const_array_of ty n = Tarray (ty, SConst n) (* TODO ??? *)
+let mk_static_exp ?(loc = no_location) ?(ty = invalid_type) =
+  { se_desc = desc; se_ty = ty; se_loc = loc }
 
 open Pp_tools
 open Format
diff --git a/compiler/heptagon/analysis/typing.ml b/compiler/heptagon/analysis/typing.ml
index a1ff811..4923476 100644
--- a/compiler/heptagon/analysis/typing.ml
+++ b/compiler/heptagon/analysis/typing.ml
@@ -306,7 +306,7 @@ let typing_static_exp const_env se =
     | Sarray se::se_list ->
         let ty = typing_static_exp const_env se in
           List.iter (expect_static_exp const_env ty) se_list;
-          Tarray(ty, Sint ((List.length se_list) + 1))
+          Tarray(ty, mk_static_exp (Sint ((List.length se_list) + 1)))
     | Stuple se_list ->
         prod (List.map (typing_static_exp const_env) se_list)
 
@@ -546,7 +546,7 @@ let rec typing statefull h e =
           let typed_exp, t1 = typing statefull h exp in
           let typed_e_list = List.map (expect statefull h t1) e_list in
           Earray(typed_exp::typed_e_list),
-          const_array_of t1 (List.length e_list + 1)
+          Tarray(t1, mk_static_exp (Sint (List.length e_list + 1)))
             (* Arity problems *)
       | Earray [] ->
           error (Earity_clash (0, 1))
@@ -635,7 +635,7 @@ and typing_array_op statefull h op e_list =
         let typed_e2 = expect statefull h (Tid Initial.pint) e2 in
         let e2 = static_exp_of_exp e2 in
         let typed_e1, t1 = typing statefull h e1 in
-        add_size_constraint (Clequal (Sconst 1, e2));
+        add_size_constraint (Clequal (mk_static_exp (Sint 1), e2));
         Tarray (t1, e2), op, [typed_e1; typed_e2]
     | Eselect idx_list, [e1] ->
         let typed_e1, t1 = typing statefull h e1 in
@@ -656,9 +656,12 @@ and typing_array_op statefull h op e_list =
         let typed_idx2 = expect statefull h (Tid Initial.pint) idx2 in
         let typed_e, t1 = typing statefull h e in
         (*Create the expression to compute the size of the array *)
-        let e1 = Sop (SMinus, static_exp_of_exp idx2, static_exp_of_exp idx1) in
-        let e2 = Sop (SPlus, e1, SConst 1) in
-        add_size_constr (Clequal (SConst 1, e2));
+        let e1 = mk_static_exp (Sop (mk_pervasives "-",
+                                     [static_exp_of_exp idx2;
+                                      static_exp_of_exp idx1])) in
+        let e2 = mk_static_exp (Sop (mk_pervasives "+", e1,
+                                     mk_static_exp (Sint  1))) in
+        add_size_constr (Clequal (mk_static_exp (Sint  1), e2));
         Tarray (element_type t1, e2), op, [typed_e; typed_idx1; typed_idx2]
     | Econcat, [e1; e2] ->
         let typed_e1, t1 = typing statefull h e1 in
@@ -684,8 +687,8 @@ and typing_array_op statefull h op e_list =
           (* add size constraints *)
         let size_constrs =
           instanciate_constr m ty_desc.node_params_constraints in
-          add_size_constraint (Clequal (SConst 1, e));
-        List.iter add_size_constraint size_constrs;
+          add_size_constraint (Clequal (mk_static_exp (Sint  1), e));
+          List.iter add_size_constraint size_constrs;
         (* return the type *)
         ty, Eiterator(it, { op_desc with op_name = f; op_kind = k }, reset),
           typed_e::typed_e_list
@@ -746,9 +749,11 @@ and typing_array_subscript statefull const_env h idx_list ty  =
     | ty, [] -> ty
     | Tarray(ty, exp), idx::idx_list ->
         expect_static_exp const_env (Tid Initial.pint) exp;
-        add_size_constraint (Clequal (SConst 0, idx));
-        add_size_constraint (Clequal (idx, Sop(SMinus, exp, SConst 1)));
-        typing_array_subscript statefull h idx_list ty
+        add_size_constraint (Clequal (mk_static_exp (Sint 0), idx));
+        let bound =  mk_static_exp (Sop(mk_pervasives "-",
+                                        [exp; mk_static_exp (Sint 1))) in
+          add_size_constraint (Clequal (idx,bound));
+          typing_array_subscript statefull h idx_list ty
     | _, _ -> error (Esubscripted_value_not_an_array ty)
 
 (* This function checks that the array dimensions matches
diff --git a/compiler/heptagon/parsing/hept_parser.mly b/compiler/heptagon/parsing/hept_parser.mly
index efaa590..e7c515f 100644
--- a/compiler/heptagon/parsing/hept_parser.mly
+++ b/compiler/heptagon/parsing/hept_parser.mly
@@ -5,6 +5,8 @@ open Location
 open Names
 open Hept_parsetree
 
+let mk_static_exp = mk_static_exp ~loc:(current_loc())
+
 %}
 
 %token DOT LPAREN RPAREN LBRACE RBRACE COLON SEMICOL
@@ -491,10 +493,10 @@ longname:
 ;
 
 const:
-  | INT { Sint $1 }
-  | FLOAT { Sfloat $1 }
-  | BOOL { Sbool $1 }
-  | constructor { Sconstructor $1 }
+  | INT { mk_static_exp (Sint $1) }
+  | FLOAT {  mk_static_exp (Sfloat $1) }
+  | BOOL {  mk_static_exp (Sbool $1) }
+  | constructor {  mk_static_exp (Sconstructor $1) }
 ;
 
 tuple_exp: