diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index d1bcc167969300c2a6883f8da8a7f99fce8fbbcf..242feb6c6a054e09f4016d0168be57a3e4a9c38f 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -305,30 +305,49 @@ let parse_float ?loc literal =
 let mk_coerce ltyp t =
   Logic_const.term ~loc:t.term_loc (TLogic_coerce(ltyp, t)) ltyp
 
-let numeric_coerce ltyp t =
+let rec numeric_coerce ltyp t =
   let oldt = unroll_type t.term_type in
-  if Cil_datatype.Logic_type.equal oldt ltyp then t
-  else match t.term_node with
-    | TLogic_coerce(lt,e) when Cil.no_op_coerce lt e ->
-      (* coercion hidden by the printer, but still present *)
-      mk_coerce ltyp e
-    | TConst(LEnum _) | TConst(Integer _) when ltyp = Linteger
-      -> { t with term_type = Linteger }
-    | TConst(LReal _ ) when ltyp = Lreal ->
-      { t with term_type = Lreal }
-    | TCastE(ty,e) ->
-      begin match ltyp, Cil.unrollType ty, e.term_node with
-        | Linteger, TInt(ik,_), TConst(Integer(v,_))
-          when Cil.fitsInInt ik v -> { e with term_type = Linteger }
-        | Lreal, TFloat(fk,_), TConst(LReal r)
-          when Cil.isExactFloat fk r -> { e with term_type = Lreal }
-        | Linteger, TInt(ik,_), TConst(LEnum { eival }) ->
-          ( match Cil.constFoldToInt eival with
-            | Some i when Cil.fitsInInt ik i -> { e with term_type = Linteger }
-            | _ -> mk_coerce ltyp t )
-        | _ -> mk_coerce ltyp t
-      end
-    | _ -> mk_coerce ltyp t
+  match t.term_node with
+  | TLogic_coerce(lt,e) when Cil.no_op_coerce lt e ->
+    (* coercion hidden by the printer, but still present *)
+    numeric_coerce ltyp e
+  | TConst(LEnum _) | TConst(Integer _) when ltyp = Linteger
+    -> { t with term_type = Linteger }
+  | TConst(LReal _ ) when ltyp = Lreal ->
+    { t with term_type = Lreal }
+  | TCastE(ty,e) ->
+    begin match ltyp, Cil.unrollType ty, e.term_node with
+      | Linteger, TInt(ik,_), TConst(Integer(v,_))
+        when Cil.fitsInInt ik v -> { e with term_type = Linteger }
+      | Lreal, TFloat(fk,_), TConst(LReal r)
+        when Cil.isExactFloat fk r -> { e with term_type = Lreal }
+      | Linteger, TInt(ik,_), TConst(LEnum { eival }) ->
+        ( match Cil.constFoldToInt eival with
+          | Some i when Cil.fitsInInt ik i -> { e with term_type = Linteger }
+          | _ -> mk_coerce ltyp t )
+      | _ -> mk_coerce ltyp t
+    end
+  | Trange(a,b) ->
+    let ra = numeric_bound ltyp a in
+    let rb = numeric_bound ltyp b in
+    { t with term_node = Trange(ra,rb) ;
+             term_type = Logic_const.make_set_type ltyp }
+  | Tunion ts ->
+    { t with term_node = Tunion (List.map (numeric_coerce ltyp) ts) ;
+             term_type = Logic_const.make_set_type ltyp }
+  | Tinter ts ->
+    { t with term_node = Tinter (List.map (numeric_coerce ltyp) ts) ;
+             term_type = Logic_const.make_set_type ltyp }
+  | Tcomprehension(t,qs,cond) ->
+    { t with term_node = Tcomprehension (numeric_coerce ltyp t,qs,cond) ;
+             term_type = Logic_const.make_set_type ltyp }
+  | _ ->
+    if Cil_datatype.Logic_type.equal oldt ltyp then t
+    else mk_coerce ltyp t
+
+and numeric_bound ltyp = function
+  | None -> None
+  | Some a -> Some (numeric_coerce ltyp a)
 
 (* Don't forget to keep is_zero_comparable
    and scalar_term_to_predicate in sync. *)
diff --git a/src/kernel_services/ast_queries/logic_utils.mli b/src/kernel_services/ast_queries/logic_utils.mli
index 81a7c454d54c33c4ad33a2b1ffeefd2b32dbd6f4..6817dfd937164f1a08a797feef81a6ea32d4f20b 100644
--- a/src/kernel_services/ast_queries/logic_utils.mli
+++ b/src/kernel_services/ast_queries/logic_utils.mli
@@ -85,7 +85,9 @@ val logicCType : logic_type -> typ
 (** transforms an array into pointer. *)
 val array_to_ptr : logic_type -> logic_type
 
-(** C type to logic type, with implicit conversion for arithmetic types. *)
+(** C type to logic type, with implicit conversion for arithmetic types.
+    @since Frama-C+dev
+*)
 val coerce_type : typ -> logic_type
 
 (** {2 Predicates} *)
@@ -122,9 +124,7 @@ val mk_logic_pointer_or_StartOf : term -> term
     be inserted. Otherwise (which is the default), [mk_cast typ t] will return
     [t] if it is already of type [typ]
 
-    @modify Aluminium-20160501 added [force] optional argument
-
-*)
+    @modify Aluminium-20160501 added [force] optional argument *)
 val mk_cast: ?loc:location -> ?force:bool -> typ -> term -> term
 
 
@@ -141,7 +141,12 @@ val remove_logic_coerce: term -> term
     in [t]. In particular, [numeric_coerce (int)cst Linteger], where [cst]
     fits in int will be directly [cst], without any coercion.
 
+    Also coerce recursively the sub-terms of t-set expressions
+    (range, union, inter and comprehension) and lift the associated
+    set type.
+
     @since Magnesium-20151001
+    @modify Frama-C+dev
 *)
 val numeric_coerce: logic_type -> term -> term