diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index 896f30bbd7b8214147c076cbbabae9ddca34ef11..cf1934d1e049824f31ae271281701a52a06300b0 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -743,6 +743,20 @@ struct
   let is_pfalse = is_false
   let is_equal a b = is_true (e_eq a b)
 
+  let is_int e =
+    try typeof e = Qed.Logic.Int with Not_found -> false
+
+  let is_real e =
+    try typeof e = Qed.Logic.Real with Not_found -> false
+
+  let is_prop e =
+    try match typeof e with Qed.Logic.Prop | Qed.Logic.Bool -> true | _ -> false
+    with Not_found -> false
+
+  let is_arith e =
+    try match typeof e with Qed.Logic.Int | Qed.Logic.Real -> true | _ -> false
+    with Not_found -> false
+
   let p_equal = e_eq
   let p_equals = List.map (fun (x,y) -> p_equal x y)
   let p_neq = e_neq
diff --git a/src/plugins/wp/TacSplit.ml b/src/plugins/wp/TacSplit.ml
index 91484aa918fd0494b496c942362a430880329c48..df18c879a4fa263f3ef91d51675738da444f4a10 100644
--- a/src/plugins/wp/TacSplit.ml
+++ b/src/plugins/wp/TacSplit.ml
@@ -192,7 +192,7 @@ class split =
                 split_cmp "Split (eq.)" x y
             | Neq(x,y) when not (is_prop x || is_prop y) ->
                 split_cmp "Split (neq.)" x y
-            | _ when F.is_prop e->
+            | _ when F.is_prop e ->
                 feedback#set_title "Split (true,false)" ;
                 feedback#set_descr "Decompose between True and False values" ;
                 let cases = ["True",F.p_bool e;"False",F.p_not (F.p_bool e)] in