diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index eaaa3c9630f329329bd4abef67ef0e964d8701fc..5c56f67f3c583257cc461fa005d42e69d08b504d 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -86,6 +86,16 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
   --------------------------------------∗
   WP "x" {{ _, True }}
   
+The command has indeed failed with message:
+In nested Ltac calls to "iIntros (constr)", "iIntros_go",
+"iDestructHyp (constr) as (constr)",
+"<iris.proofmode.ltac_tactics.iDestructHypFindPat>",
+"<iris.proofmode.ltac_tactics.iDestructHypGo>" and
+"iAndDestruct (constr) as (constr) (constr)", last call failed.
+Tactic failure: iAndDestruct: cannot destruct (l ↦∗ (vs1 ++ vs2))%I.
+The command has indeed failed with message:
+Ltac call to "iSplitL (constr)" failed.
+Tactic failure: iSplitL: (l ↦∗ (vs1 ++ vs2))%I not a separating conjunction.
 1 subgoal
   
   Σ : gFunctors
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 9d7f906bb5d582fc82a734b2f9b7371886889747..ace30598780595a9466f2f0949ff892114f0883f 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -158,7 +158,10 @@ Section tests.
   Lemma test_array_app l vs1 vs2 :
     l ↦∗ (vs1 ++ vs2) -∗ l ↦∗ (vs1 ++ vs2).
   Proof.
-    iIntros "[H1 H2]". iSplitL "H1"; done.
+    Fail iIntros "[H1 H2]". (* this should, one day, split at the fraction. *)
+    iIntros "H". iDestruct (array_app with "H") as "[H1 H2]".
+    Fail iSplitL "H1".
+    iApply array_app. iSplitL "H1"; done.
   Qed.
 
 End tests.
diff --git a/theories/heap_lang/array.v b/theories/heap_lang/array.v
index c7dee76969db036a68a8b42a2def4710bc65d3c8..32cd79f3b2ff16ad42a8e0d8d34320d571eb0269 100644
--- a/theories/heap_lang/array.v
+++ b/theories/heap_lang/array.v
@@ -61,24 +61,8 @@ Proof.
   rewrite drop_insert; last by lia. done.
 Qed.
 
-(** Proofmode instances *)
-Global Instance into_sep_array_cons l vs v vs' :
-  IsCons vs v vs' →
-  IntoSep (l ↦∗ vs) (l ↦ v) ((l +ₗ 1) ↦∗ vs').
-Proof. rewrite /IsCons=>->. by rewrite /IntoSep array_cons. Qed.
-Global Instance into_sep_array_app l vs vs1 vs2 :
-  IsApp vs vs1 vs2 →
-  IntoSep (l ↦∗ vs) (l ↦∗ vs1) ((l +ₗ length vs1) ↦∗ vs2).
-Proof. rewrite /IsApp=>->. by rewrite /IntoSep array_app. Qed.
-
-Global Instance from_sep_array_cons l vs v vs' :
-  IsCons vs v vs' →
-  FromSep (l ↦∗ vs) (l ↦ v) ((l +ₗ 1) ↦∗ vs').
-Proof. rewrite /IsCons=> ->. by rewrite /FromSep array_cons. Qed.
-Global Instance from_sep_array_app l vs vs1 vs2 :
-  IsApp vs vs1 vs2 →
-  FromSep (l ↦∗ vs) (l ↦∗ vs1) ((l +ₗ length vs1) ↦∗ vs2).
-Proof. rewrite /IsApp=> ->. by rewrite /FromSep array_app. Qed.
+(** No [FromSep] or [IntoSep] instances to remain forwards compatible with a
+fractional array assertion, that will split the fraction, not the list. *)
 
 (** Allocation *)
 Lemma mapsto_seq_array l v n :
@@ -240,3 +224,5 @@ Proof.
 Qed.
 
 End lifting.
+
+Typeclasses Opaque array.