From dd28d249acb2162c2538909a27229d9f653e5d30 Mon Sep 17 00:00:00 2001
From: Johannes Hostert <jhostert@ethz.ch>
Date: Fri, 14 Mar 2025 17:25:00 +0100
Subject: [PATCH] remove "Print Assumptions" things

---
 .../examples/protected/mutable_reorder_read_down.v             | 2 ++
 .../tree_borrows/examples/protected/mutable_reorder_read_up.v  | 2 ++
 .../examples/protected/mutable_reorder_write_down_activated.v  | 2 ++
 .../examples/protected/mutable_reorder_write_up_activated.v    | 2 ++
 .../protected/mutable_reorder_write_up_activated_paper.v       | 2 ++
 theories/tree_borrows/examples/protected/shared_insert_read.v  | 2 ++
 .../examples/protected/shared_reorder_read_down_escaped.v      | 2 ++
 .../examples/protected/shared_reorder_read_up_escaped.v        | 3 ++-
 .../tree_borrows/examples/unprotected/mutable_delete_read.v    | 2 ++
 .../examples/unprotected/shared_delete_read_escaped.v          | 2 ++
 .../unprotected/shared_delete_read_escaped_coinductive.v       | 3 ++-
 theories/tree_borrows/read_read_reorder/read_reorder.v         | 3 ++-
 12 files changed, 24 insertions(+), 3 deletions(-)

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 e9b73792..73d7c596 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 fce0c9e8..a31f72c9 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 1ad1d78a..41fd8d98 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 5e02c635..9c3532c5 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 dc7f4e69..3a5ee20d 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 3cec5d57..bdf9d3bb 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 3aef4400..45746667 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 8b1634f4..71e9eb6e 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 09d2f2e2..a8a40a91 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 a82d996b..adc95c91 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 4d17427e..72891e22 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 a4f42a9c..7c46d17b 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
-- 
GitLab