diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index e5af6aef4d1abfa468a63f4a5dd6a2630fcba346..2cf9ac222f035deeae5075af0599ac7b9c7f0473 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -267,64 +267,6 @@ goal 2 is:
 --------------------------------------∗
 WP #() #() @ E ∖ ↑N {{ _, |={E ∖ ↑N}=> ▷ P ∗ True }}
 
-1 goal
-  
-  Σ : gFunctors
-  heapGS0 : heapGS Σ
-  ============================
-  --------------------------------------∗
-  WP let: "f" := λ: "x", "x" in ref ("f" #10) {{ _, True }}
-  
-1 goal
-  
-  Σ : gFunctors
-  heapGS0 : heapGS Σ
-  fun1, fun2, fun3 : expr
-  ============================
-  --------------------------------------∗
-  WP let: "val1" := fun1 #() in
-     let: "val2" := fun2 "val1" in
-     let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
-  {{ _, True }}
-  
-1 goal
-  
-  Σ : gFunctors
-  heapGS0 : heapGS Σ
-  fun1, fun2, fun3 : expr
-  Φ : language.val heap_lang → iPropI Σ
-  ============================
-  --------------------------------------∗
-  WP let: "val1" := fun1 #() in
-     let: "val2" := fun2 "val1" in
-     let: "v" := fun3 "v" in if: "v" = "v" then "v" else "v" 
-  {{ v, Φ v }}
-  
-1 goal
-  
-  Σ : gFunctors
-  heapGS0 : heapGS Σ
-  fun1, fun2, fun3 : expr
-  Φ : language.val heap_lang → iPropI Σ
-  E : coPset
-  ============================
-  --------------------------------------∗
-  WP let: "val1" := fun1 #() in
-     let: "val2" := fun2 "val1" in
-     let: "v" := fun3 "v" in if: "v" = "v" then "v" else "v" 
-  @ E {{ v, Φ v }}
-  
-1 goal
-  
-  Σ : gFunctors
-  heapGS0 : heapGS Σ
-  fun1, fun2, fun3 : expr
-  ============================
-  {{{ True }}}
-    let: "val1" := fun1 #() in
-    let: "val2" := fun2 "val1" in
-    let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
-  {{{ (x y : val) (z : Z), RET (x, y, #z); True }}}
 "not_cmpxchg"
      : string
 The command has indeed failed with message:
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index da4831eb227392734bf0602bc15cfe6e4d974861..a83b6662da4ebea358c75f8b695bb7c5edd55a64 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -416,57 +416,6 @@ Section atomic.
 
 End atomic.
 
-Section printing_tests.
-  Context `{!heapGS Σ}.
-
-  Lemma ref_print :
-    True -∗ WP let: "f" := (λ: "x", "x") in ref ("f" #10) {{ _, True }}.
-  Proof.
-    iIntros "_". Show.
-  Abort.
-
-  (* These terms aren't even closed, but that's not what this is about.  The
-  length of the variable names etc. has been carefully chosen to trigger
-  particular behavior of the Coq pretty printer. *)
-
-  Lemma wp_print_long_expr (fun1 fun2 fun3 : expr) :
-    True -∗ WP let: "val1" := fun1 #() in
-       let: "val2" := fun2 "val1" in
-       let: "val3" := fun3 "val2" in
-       if: "val1" = "val2" then "val" else "val3"  {{ _, True }}.
-  Proof.
-    iIntros "_". Show.
-  Abort.
-
-  Lemma wp_print_long_expr (fun1 fun2 fun3 : expr) Φ :
-    True -∗ WP let: "val1" := fun1 #() in
-       let: "val2" := fun2 "val1" in
-       let: "v" := fun3 "v" in
-       if: "v" = "v" then "v" else "v"  {{ Φ }}.
-  Proof.
-    iIntros "_". Show.
-  Abort.
-
-  Lemma wp_print_long_expr (fun1 fun2 fun3 : expr) Φ E :
-    True -∗ WP let: "val1" := fun1 #() in
-       let: "val2" := fun2 "val1" in
-       let: "v" := fun3 "v" in
-       if: "v" = "v" then "v" else "v" @ E {{ Φ }}.
-  Proof.
-    iIntros "_". Show.
-  Abort.
-
-  Lemma texan_triple_long_expr (fun1 fun2 fun3 : expr) :
-    {{{ True }}}
-       let: "val1" := fun1 #() in
-       let: "val2" := fun2 "val1" in
-       let: "val3" := fun3 "val2" in
-       if: "val1" = "val2" then "val" else "val3"
-    {{{ (x y : val) (z : Z), RET (x, y, #z); True }}}.
-  Proof. Show. Abort.
-
-End printing_tests.
-
 Section error_tests.
   Context `{!heapGS Σ}.
 
diff --git a/tests/heap_lang_printing.ref b/tests/heap_lang_printing.ref
new file mode 100644
index 0000000000000000000000000000000000000000..df425cad2f0aac41f7656d1a9cc95a1e99df61f5
--- /dev/null
+++ b/tests/heap_lang_printing.ref
@@ -0,0 +1,58 @@
+1 goal
+  
+  Σ : gFunctors
+  heapGS0 : heapGS Σ
+  ============================
+  --------------------------------------∗
+  WP let: "f" := λ: "x", "x" in ref ("f" #10) {{ _, True }}
+  
+1 goal
+  
+  Σ : gFunctors
+  heapGS0 : heapGS Σ
+  fun1, fun2, fun3 : expr
+  ============================
+  --------------------------------------∗
+  WP let: "val1" := fun1 #() in
+     let: "val2" := fun2 "val1" in
+     let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
+  {{ _, True }}
+  
+1 goal
+  
+  Σ : gFunctors
+  heapGS0 : heapGS Σ
+  fun1, fun2, fun3 : expr
+  Φ : language.val heap_lang → iPropI Σ
+  ============================
+  --------------------------------------∗
+  WP let: "val1" := fun1 #() in
+     let: "val2" := fun2 "val1" in
+     let: "v" := fun3 "v" in if: "v" = "v" then "v" else "v" 
+  {{ v, Φ v }}
+  
+1 goal
+  
+  Σ : gFunctors
+  heapGS0 : heapGS Σ
+  fun1, fun2, fun3 : expr
+  Φ : language.val heap_lang → iPropI Σ
+  E : coPset
+  ============================
+  --------------------------------------∗
+  WP let: "val1" := fun1 #() in
+     let: "val2" := fun2 "val1" in
+     let: "v" := fun3 "v" in if: "v" = "v" then "v" else "v" 
+  @ E {{ v, Φ v }}
+  
+1 goal
+  
+  Σ : gFunctors
+  heapGS0 : heapGS Σ
+  fun1, fun2, fun3 : expr
+  ============================
+  {{{ True }}}
+    let: "val1" := fun1 #() in
+    let: "val2" := fun2 "val1" in
+    let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
+  {{{ (x y : val) (z : Z), RET (x, y, #z); True }}}
diff --git a/tests/heap_lang_printing.v b/tests/heap_lang_printing.v
new file mode 100644
index 0000000000000000000000000000000000000000..31e92bd610f33697be896eb618178bd55f51f4c4
--- /dev/null
+++ b/tests/heap_lang_printing.v
@@ -0,0 +1,59 @@
+From iris.base_logic.lib Require Import gen_inv_heap invariants.
+From iris.program_logic Require Export weakestpre total_weakestpre.
+From iris.heap_lang Require Import lang adequacy proofmode notation.
+(* Import lang *again*. This used to break notation. *)
+From iris.heap_lang Require Import lang.
+From iris.prelude Require Import options.
+
+Unset Mangle Names.
+
+Section printing_tests.
+  Context `{!heapGS Σ}.
+
+  Lemma ref_print :
+    True -∗ WP let: "f" := (λ: "x", "x") in ref ("f" #10) {{ _, True }}.
+  Proof.
+    iIntros "_". Show.
+  Abort.
+
+  (* These terms aren't even closed, but that's not what this is about.  The
+  length of the variable names etc. has been carefully chosen to trigger
+  particular behavior of the Coq pretty printer. *)
+
+  Lemma wp_print_long_expr (fun1 fun2 fun3 : expr) :
+    True -∗ WP let: "val1" := fun1 #() in
+       let: "val2" := fun2 "val1" in
+       let: "val3" := fun3 "val2" in
+       if: "val1" = "val2" then "val" else "val3"  {{ _, True }}.
+  Proof.
+    iIntros "_". Show.
+  Abort.
+
+  Lemma wp_print_long_expr (fun1 fun2 fun3 : expr) Φ :
+    True -∗ WP let: "val1" := fun1 #() in
+       let: "val2" := fun2 "val1" in
+       let: "v" := fun3 "v" in
+       if: "v" = "v" then "v" else "v"  {{ Φ }}.
+  Proof.
+    iIntros "_". Show.
+  Abort.
+
+  Lemma wp_print_long_expr (fun1 fun2 fun3 : expr) Φ E :
+    True -∗ WP let: "val1" := fun1 #() in
+       let: "val2" := fun2 "val1" in
+       let: "v" := fun3 "v" in
+       if: "v" = "v" then "v" else "v" @ E {{ Φ }}.
+  Proof.
+    iIntros "_". Show.
+  Abort.
+
+  Lemma texan_triple_long_expr (fun1 fun2 fun3 : expr) :
+    {{{ True }}}
+       let: "val1" := fun1 #() in
+       let: "val2" := fun2 "val1" in
+       let: "val3" := fun3 "val2" in
+       if: "val1" = "val2" then "val" else "val3"
+    {{{ (x y : val) (z : Z), RET (x, y, #z); True }}}.
+  Proof. Show. Abort.
+
+End printing_tests.
diff --git a/tests/heap_lang2.ref b/tests/heap_lang_printing2.ref
similarity index 100%
rename from tests/heap_lang2.ref
rename to tests/heap_lang_printing2.ref
diff --git a/tests/heap_lang2.v b/tests/heap_lang_printing2.v
similarity index 91%
rename from tests/heap_lang2.v
rename to tests/heap_lang_printing2.v
index a4b12e368b056c0242b0b80707320beff339d5f3..48a1f14c81f2969749f5b1d94c63389a9d76779c 100644
--- a/tests/heap_lang2.v
+++ b/tests/heap_lang_printing2.v
@@ -1,5 +1,4 @@
-(* Test yet another way of importing heap_lang modules that used to break
-printing *)
+(* Test another way of importing heap_lang modules that used to break printing *)
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Export primitive_laws notation.
 From iris.heap_lang Require Import proofmode notation.