diff --git a/theories/tree_borrows/examples/protected/mutable_reorder_read_down.v b/theories/tree_borrows/examples/protected/mutable_reorder_read_down.v
index e9b73792c03fe48031a2e4412c6159bbef2c1524..73d7c59688c60d32d20c389f02f67b402503b68c 100755
--- a/theories/tree_borrows/examples/protected/mutable_reorder_read_down.v
+++ b/theories/tree_borrows/examples/protected/mutable_reorder_read_down.v
@@ -123,8 +123,10 @@ Section closed.
   Qed.
 End closed.
 
+(*
 Check prot_mutable_reorder_read_down_ctx.
 Print Assumptions prot_mutable_reorder_read_down_ctx.
+*)
 (* 
 prot_mutable_reorder_read_down_ctx
      : ctx_ref prot_mutable_reorder_read_down_opt prot_mutable_reorder_read_down_unopt
diff --git a/theories/tree_borrows/examples/protected/mutable_reorder_read_up.v b/theories/tree_borrows/examples/protected/mutable_reorder_read_up.v
index fce0c9e8e270429bbd84220c414dfb08e453b6b8..a31f72c9df7827cd121910b493307e39bcb353f4 100755
--- a/theories/tree_borrows/examples/protected/mutable_reorder_read_up.v
+++ b/theories/tree_borrows/examples/protected/mutable_reorder_read_up.v
@@ -124,8 +124,10 @@ Section closed.
   Qed.
 End closed.
 
+(*
 Check prot_mutable_reorder_read_up_ctx.
 Print Assumptions prot_mutable_reorder_read_up_ctx.
+*)
 (* 
 prot_mutable_reorder_read_up_ctx
      : ctx_ref prot_mutable_reorder_read_up_opt prot_mutable_reorder_read_up_unopt
diff --git a/theories/tree_borrows/examples/protected/mutable_reorder_write_down_activated.v b/theories/tree_borrows/examples/protected/mutable_reorder_write_down_activated.v
index 1ad1d78a0c40084d8c78bedb8225e2fac12b3437..41fd8d98f8f69ce21df03eb4580b5110c5d8d2af 100755
--- a/theories/tree_borrows/examples/protected/mutable_reorder_write_down_activated.v
+++ b/theories/tree_borrows/examples/protected/mutable_reorder_write_down_activated.v
@@ -174,8 +174,10 @@ Section closed.
   Qed.
 End closed.
 
+(*
 Check prot_mutable_reorder_write_down_activated_ctx.
 Print Assumptions prot_mutable_reorder_write_down_activated_ctx.
+*)
 (* 
 prot_mutable_reorder_write_down_activated_ctx
      : ctx_ref prot_mutable_reorder_write_down_activated_opt prot_mutable_reorder_write_down_activated_unopt
diff --git a/theories/tree_borrows/examples/protected/mutable_reorder_write_up_activated.v b/theories/tree_borrows/examples/protected/mutable_reorder_write_up_activated.v
index 5e02c635270619c3bb79bb8bc8fc7066ef6f538a..9c3532c516b738bc99b2fa3b350b69c6ec5de26f 100755
--- a/theories/tree_borrows/examples/protected/mutable_reorder_write_up_activated.v
+++ b/theories/tree_borrows/examples/protected/mutable_reorder_write_up_activated.v
@@ -132,8 +132,10 @@ Section closed.
   Qed.
 End closed.
 
+(*
 Check prot_mutable_reorder_write_up_activated_ctx.
 Print Assumptions prot_mutable_reorder_write_up_activated_ctx.
+*)
 (* 
 prot_mutable_reorder_write_up_activated_ctx
      : ctx_ref prot_mutable_reorder_write_up_activated_opt prot_mutable_reorder_write_up_activated_unopt
diff --git a/theories/tree_borrows/examples/protected/mutable_reorder_write_up_activated_paper.v b/theories/tree_borrows/examples/protected/mutable_reorder_write_up_activated_paper.v
index dc7f4e69b3b039d0db18b6b34cd16d9798069600..3a5ee20d6b10baf028a78dd5fae284796ee605ef 100644
--- a/theories/tree_borrows/examples/protected/mutable_reorder_write_up_activated_paper.v
+++ b/theories/tree_borrows/examples/protected/mutable_reorder_write_up_activated_paper.v
@@ -146,8 +146,10 @@ Section closed.
   Qed.
 End closed.
 
+(*
 Check prot_mutable_reorder_write_up_activated_paper_ctx.
 Print Assumptions prot_mutable_reorder_write_up_activated_paper_ctx.
+*)
 (* 
 prot_mutable_reorder_write_up_activated_paper_ctx
      : ctx_ref prot_mutable_reorder_write_up_activated_paper_opt prot_mutable_reorder_write_up_activated_paper_unopt
diff --git a/theories/tree_borrows/examples/protected/shared_insert_read.v b/theories/tree_borrows/examples/protected/shared_insert_read.v
index 3cec5d577ed7ac7c6b53ecefc25e2af5cf44f3e2..bdf9d3bbaf377b4847c6443de70e512338b30dab 100644
--- a/theories/tree_borrows/examples/protected/shared_insert_read.v
+++ b/theories/tree_borrows/examples/protected/shared_insert_read.v
@@ -157,8 +157,10 @@ Section closed.
   Qed.
 End closed.
 
+(*
 Check prot_shared_insert_read_ctx.
 Print Assumptions prot_shared_insert_read_ctx.
+*)
 (* 
 prot_shared_insert_read_ctx
      : ctx_ref prot_shared_insert_read_opt prot_shared_insert_read_unopt
diff --git a/theories/tree_borrows/examples/protected/shared_reorder_read_down_escaped.v b/theories/tree_borrows/examples/protected/shared_reorder_read_down_escaped.v
index 3aef44004067acdc6c5b7f08314b8a0131faf722..4574666711631c6c3bfda780ff0df9ad1a63e957 100755
--- a/theories/tree_borrows/examples/protected/shared_reorder_read_down_escaped.v
+++ b/theories/tree_borrows/examples/protected/shared_reorder_read_down_escaped.v
@@ -135,8 +135,10 @@ Section closed.
   Qed.
 End closed.
 
+(*
 Check prot_shared_reorder_read_down_escaped_ctx.
 Print Assumptions prot_shared_reorder_read_down_escaped_ctx.
+*)
 (* 
 prot_shared_reorder_read_down_escaped_ctx
      : ctx_ref prot_shared_reorder_read_down_escaped_opt prot_shared_reorder_read_down_escaped_unopt
diff --git a/theories/tree_borrows/examples/protected/shared_reorder_read_up_escaped.v b/theories/tree_borrows/examples/protected/shared_reorder_read_up_escaped.v
index 8b1634f49c80bdd921280aaa8f46ab0980c56fcd..71e9eb6e283ba568e76edfeb6733fdfdeeae84fd 100755
--- a/theories/tree_borrows/examples/protected/shared_reorder_read_up_escaped.v
+++ b/theories/tree_borrows/examples/protected/shared_reorder_read_up_escaped.v
@@ -138,9 +138,10 @@ Section closed.
     apply prot_shared_reorder_read_up_escaped.
   Qed.
 End closed.
-
+(*
 Check prot_shared_reorder_read_up_escaped_ctx.
 Print Assumptions prot_shared_reorder_read_up_escaped_ctx.
+*)
 (* 
 prot_shared_reorder_read_up_escaped_ctx
      : ctx_ref prot_shared_reorder_read_up_escaped_opt prot_shared_reorder_read_up_escaped_unopt
diff --git a/theories/tree_borrows/examples/unprotected/mutable_delete_read.v b/theories/tree_borrows/examples/unprotected/mutable_delete_read.v
index 09d2f2e22bf5a059e5759761e3bc00fad404f79c..a8a40a91584eb3fd275cf8cd70883cb864d7bda3 100644
--- a/theories/tree_borrows/examples/unprotected/mutable_delete_read.v
+++ b/theories/tree_borrows/examples/unprotected/mutable_delete_read.v
@@ -134,8 +134,10 @@ Section closed.
   Qed.
 End closed.
 
+(*
 Check unprot_mutable_delete_read_ctx.
 Print Assumptions unprot_mutable_delete_read_ctx.
+*)
 (*
 unprot_mutable_delete_read_ctx
      : ctx_ref unprot_mutable_delete_read_opt unprot_mutable_delete_read_unopt
diff --git a/theories/tree_borrows/examples/unprotected/shared_delete_read_escaped.v b/theories/tree_borrows/examples/unprotected/shared_delete_read_escaped.v
index a82d996b26755a7e8dcd3a93fceb49922436a3d3..adc95c916df633dfce7c929950ff8f4e6ab649d1 100644
--- a/theories/tree_borrows/examples/unprotected/shared_delete_read_escaped.v
+++ b/theories/tree_borrows/examples/unprotected/shared_delete_read_escaped.v
@@ -138,8 +138,10 @@ Section closed.
   Qed.
 End closed.
 
+(*
 Check unprot_shared_delete_read_escaped_ctx.
 Print Assumptions unprot_shared_delete_read_escaped_ctx.
+*)
 (* 
 unprot_shared_delete_read_escaped_ctx
      : ctx_ref unprot_shared_delete_read_escaped_opt unprot_shared_delete_read_escaped_unopt
diff --git a/theories/tree_borrows/examples/unprotected/shared_delete_read_escaped_coinductive.v b/theories/tree_borrows/examples/unprotected/shared_delete_read_escaped_coinductive.v
index 4d17427ef202db8f0148b0da752a144768e1c3a8..72891e222eaeb2d65559044c15dd696d52cb1bf3 100755
--- a/theories/tree_borrows/examples/unprotected/shared_delete_read_escaped_coinductive.v
+++ b/theories/tree_borrows/examples/unprotected/shared_delete_read_escaped_coinductive.v
@@ -323,9 +323,10 @@ Section closed.
   Qed.
 End closed.
 
-
+(*
 Check unprot_shared_delete_read_escaped_coinductive_ctx.
 Print Assumptions unprot_shared_delete_read_escaped_coinductive_ctx.
+*)
 (* 
 unprot_shared_delete_read_escaped_coinductive_ctx
      : ctx_ref unprot_shared_delete_read_escaped_coinductive_opt unprot_shared_delete_read_escaped_coinductive_unopt
diff --git a/theories/tree_borrows/read_read_reorder/read_reorder.v b/theories/tree_borrows/read_read_reorder/read_reorder.v
index a4f42a9c841cbf6a6ef0a2f8e5b5d2405d3234a1..7c46d17b470650ca95dfcdb2288804b783634e16 100644
--- a/theories/tree_borrows/read_read_reorder/read_reorder.v
+++ b/theories/tree_borrows/read_read_reorder/read_reorder.v
@@ -228,5 +228,6 @@ Proof.
   split; eapply read_reorder_onesided; done.
 Qed.
 
-
+(*
 Print Assumptions read_reorder.
+*)
\ No newline at end of file