diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 85791ec2176013fee96e509a2a6545dd209db0b0..c3044b80fdd1f73b70d21983a6858bbd2519cdbd 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -381,13 +381,15 @@ Tactic Notation "iSplitL" constr(Hs) :=
   eapply tac_sep_split with _ _ false Hs _ _; (* (js:=Hs) *)
     [let P := match goal with |- FromSep ?P _ _ => P end in
      apply _ || fail "iSplitL:" P "not a separating conjunction"
-    |env_cbv; reflexivity || fail "iSplitL: hypotheses" Hs "not found"| |].
+    |env_cbv; reflexivity || fail "iSplitL: hypotheses" Hs
+                                  "not found in the spatial context"| |].
 Tactic Notation "iSplitR" constr(Hs) :=
   let Hs := words Hs in
   eapply tac_sep_split with _ _ true Hs _ _; (* (js:=Hs) *)
     [let P := match goal with |- FromSep ?P _ _ => P end in
      apply _ || fail "iSplitR:" P "not a separating conjunction"
-    |env_cbv; reflexivity || fail "iSplitR: hypotheses" Hs "not found"| |].
+    |env_cbv; reflexivity || fail "iSplitR: hypotheses" Hs
+                                  "not found in the spatial context"| |].
 
 Tactic Notation "iSplitL" := iSplitR "".
 Tactic Notation "iSplitR" := iSplitL "".