From fe7f53ce835f2957d565033b584d7129393e526c Mon Sep 17 00:00:00 2001
From: Sergei Bozhko <sbozhko@mpi-sws.org>
Date: Sat, 5 Apr 2025 18:24:42 +0200
Subject: [PATCH] remove some prints and warnings

---
 rt/analysis/WCET_is_pWCET.v        | 2 --
 rt/analysis/axiomatic_pWCET_full.v | 2 --
 rt/analysis/pRTA/pRTA.v            | 2 --
 rt/analysis/work_bound.v           | 6 +++---
 4 files changed, 3 insertions(+), 9 deletions(-)

diff --git a/rt/analysis/WCET_is_pWCET.v b/rt/analysis/WCET_is_pWCET.v
index 4d28873..eb03985 100644
--- a/rt/analysis/WCET_is_pWCET.v
+++ b/rt/analysis/WCET_is_pWCET.v
@@ -145,5 +145,3 @@ Section WCETisAxiomaticPWCET.
   Qed.
 
 End WCETisAxiomaticPWCET.
-
-Print Assumptions WCET_is_axiomatic_pWCET.
diff --git a/rt/analysis/axiomatic_pWCET_full.v b/rt/analysis/axiomatic_pWCET_full.v
index e8aeb07..2924fef 100644
--- a/rt/analysis/axiomatic_pWCET_full.v
+++ b/rt/analysis/axiomatic_pWCET_full.v
@@ -105,5 +105,3 @@ Section MainLemma.
   Qed.
 
 End MainLemma.
-
-Print Assumptions probabilistic_rt_monotonicity_of_iid_pWCET.
diff --git a/rt/analysis/pRTA/pRTA.v b/rt/analysis/pRTA/pRTA.v
index 47e83d1..fca5a2e 100644
--- a/rt/analysis/pRTA/pRTA.v
+++ b/rt/analysis/pRTA/pRTA.v
@@ -470,5 +470,3 @@ Section WCDFPIsBounded.
   Qed.
 
 End WCDFPIsBounded.
-
-Print Assumptions probabilistic_rta_fp.
diff --git a/rt/analysis/work_bound.v b/rt/analysis/work_bound.v
index fb98d26..975d34e 100644
--- a/rt/analysis/work_bound.v
+++ b/rt/analysis/work_bound.v
@@ -33,9 +33,9 @@ Section PrTaskWorkloadBoundedNthCost.
 
   (** Assume that job costs are independent of the (prob.) arrival sequence. *)
   Let ξpart := partition_on_ξ μ : Ω_partition.
-  Hypothesis job_costs_independent_arr_seq :
+  Hypothesis H_job_costs_independent_arr_seq :
     let ξpart := partition_on_ξ μ : Ω_partition in
-    forall (ξ : I ξpart) `{!PosProb μ (ξpart◁{ξ})} (jobs : seq Job),
+    forall (ξ : I ξpart) `(!PosProb μ (ξpart◁{ξ})) (jobs : seq Job),
       indep2
         (mkRvar μ (fun ω => [seq job_cost j ω | j <- jobs]))
         (mkRvar μ (fun ω => ξpart◁{ξ} ω)).
@@ -61,7 +61,7 @@ Section PrTaskWorkloadBoundedNthCost.
       { by rewrite //= in IHjobs; rewrite //= !big_cons //= IHjobs. }
     }
     eapply indep2_fn_extl; first by intros; apply: EQ.
-    by apply job_costs_independent_arr_seq, PosProb0.
+    by apply H_job_costs_independent_arr_seq, PosProb0.
   Qed.
 
 
-- 
GitLab