From 18ec53fbb5751df009c067a39e2e3b8a551b8b03 Mon Sep 17 00:00:00 2001
From: Marco Maida <mmaida@mpi-sws.org>
Date: Mon, 26 Jul 2021 16:22:32 +0200
Subject: [PATCH] Fixed warnings

---
 analysis/facts/edf.v                                      | 2 +-
 analysis/facts/model/ideal_schedule.v                     | 2 +-
 analysis/facts/periodic/sporadic.v                        | 2 +-
 analysis/facts/preemption/job/limited.v                   | 2 +-
 analysis/facts/preemption/job/nonpreemptive.v             | 2 +-
 analysis/facts/preemption/job/preemptive.v                | 2 +-
 analysis/facts/preemption/rtc_threshold/floating.v        | 2 +-
 analysis/facts/preemption/rtc_threshold/job_preemptable.v | 2 +-
 analysis/facts/preemption/rtc_threshold/limited.v         | 2 +-
 analysis/facts/preemption/rtc_threshold/nonpreemptive.v   | 2 +-
 analysis/facts/preemption/rtc_threshold/preemptive.v      | 2 +-
 analysis/facts/preemption/task/floating.v                 | 2 +-
 analysis/facts/preemption/task/limited.v                  | 2 +-
 analysis/facts/preemption/task/nonpreemptive.v            | 2 +-
 analysis/facts/preemption/task/preemptive.v               | 2 +-
 classic/util/tactics.v                                    | 4 ++--
 model/priority/classes.v                                  | 2 +-
 model/priority/deadline_monotonic.v                       | 2 +-
 model/priority/edf.v                                      | 2 +-
 model/priority/fifo.v                                     | 2 +-
 model/priority/numeric_fixed_priority.v                   | 2 +-
 model/priority/rate_monotonic.v                           | 2 +-
 22 files changed, 23 insertions(+), 23 deletions(-)

diff --git a/analysis/facts/edf.v b/analysis/facts/edf.v
index 7f3948983..7969e812e 100644
--- a/analysis/facts/edf.v
+++ b/analysis/facts/edf.v
@@ -31,4 +31,4 @@ End PropertiesOfEDF.
 
 (** We add the above lemma into a "Hint Database" basic_facts, so Coq
     will be able to apply them automatically. *)
-Hint Resolve EDF_respects_sequential_tasks : basic_facts.
+Global Hint Resolve EDF_respects_sequential_tasks : basic_facts.
diff --git a/analysis/facts/model/ideal_schedule.v b/analysis/facts/model/ideal_schedule.v
index f2c7ed3f6..a68a582f7 100644
--- a/analysis/facts/model/ideal_schedule.v
+++ b/analysis/facts/model/ideal_schedule.v
@@ -196,7 +196,7 @@ End IncrementalService.
 (** * Automation *)
 (** We add the above lemmas into a "Hint Database" basic_facts, so Coq 
     will be able to apply them automatically. *)
-Hint Resolve ideal_proc_model_is_a_uniprocessor_model
+Global Hint Resolve ideal_proc_model_is_a_uniprocessor_model
      ideal_proc_model_ensures_ideal_progress
      ideal_proc_model_provides_unit_service : basic_facts.
 
diff --git a/analysis/facts/periodic/sporadic.v b/analysis/facts/periodic/sporadic.v
index 62e377af8..35e96896e 100644
--- a/analysis/facts/periodic/sporadic.v
+++ b/analysis/facts/periodic/sporadic.v
@@ -89,4 +89,4 @@ End PeriodicTasksAsSporadicTasks.
 
 (** We add the [periodic_task_respects_sporadic_task_model] lemma into a "Hint Database" basic_facts,
     so Coq will be able to apply it automatically. *)
-Hint Extern 1 => apply periodic_task_respects_sporadic_task_model : basic_facts.
+Global Hint Extern 1 => apply periodic_task_respects_sporadic_task_model : basic_facts.
diff --git a/analysis/facts/preemption/job/limited.v b/analysis/facts/preemption/job/limited.v
index b78c8890a..9f86d27a1 100644
--- a/analysis/facts/preemption/job/limited.v
+++ b/analysis/facts/preemption/job/limited.v
@@ -225,4 +225,4 @@ Section ModelWithLimitedPreemptions.
   Qed.
   
 End ModelWithLimitedPreemptions.
-Hint Resolve valid_fixed_preemption_points_model_lemma : basic_facts.
+Global Hint Resolve valid_fixed_preemption_points_model_lemma : basic_facts.
diff --git a/analysis/facts/preemption/job/nonpreemptive.v b/analysis/facts/preemption/job/nonpreemptive.v
index a0d723ea0..be03b3fb3 100644
--- a/analysis/facts/preemption/job/nonpreemptive.v
+++ b/analysis/facts/preemption/job/nonpreemptive.v
@@ -126,4 +126,4 @@ Section FullyNonPreemptiveModel.
   Qed.
   
 End FullyNonPreemptiveModel.
-Hint Resolve valid_fully_nonpreemptive_model : basic_facts.
+Global Hint Resolve valid_fully_nonpreemptive_model : basic_facts.
diff --git a/analysis/facts/preemption/job/preemptive.v b/analysis/facts/preemption/job/preemptive.v
index 30c83ac5d..95319c424 100644
--- a/analysis/facts/preemption/job/preemptive.v
+++ b/analysis/facts/preemption/job/preemptive.v
@@ -65,4 +65,4 @@ Section FullyPreemptiveModel.
   Qed.    
   
 End FullyPreemptiveModel.
-Hint Resolve valid_fully_preemptive_model : basic_facts. 
\ No newline at end of file
+Global Hint Resolve valid_fully_preemptive_model : basic_facts. 
\ No newline at end of file
diff --git a/analysis/facts/preemption/rtc_threshold/floating.v b/analysis/facts/preemption/rtc_threshold/floating.v
index 1e8dc6a5f..90eecedb3 100644
--- a/analysis/facts/preemption/rtc_threshold/floating.v
+++ b/analysis/facts/preemption/rtc_threshold/floating.v
@@ -40,4 +40,4 @@ Section TaskRTCThresholdFloatingNonPreemptiveRegions.
   Qed.
   
 End TaskRTCThresholdFloatingNonPreemptiveRegions.
-Hint Resolve floating_preemptive_valid_task_run_to_completion_threshold : basic_facts.
+Global Hint Resolve floating_preemptive_valid_task_run_to_completion_threshold : basic_facts.
diff --git a/analysis/facts/preemption/rtc_threshold/job_preemptable.v b/analysis/facts/preemption/rtc_threshold/job_preemptable.v
index 59c647e3a..62e23bfaf 100644
--- a/analysis/facts/preemption/rtc_threshold/job_preemptable.v
+++ b/analysis/facts/preemption/rtc_threshold/job_preemptable.v
@@ -261,4 +261,4 @@ End RunToCompletionThreshold.
 
 (** We add the above lemmas into a "Hint Database" basic_facts, so Coq 
     will be able to apply them automatically. *)   
-Hint Resolve job_run_to_completion_threshold_le_job_cost : basic_facts.
+Global Hint Resolve job_run_to_completion_threshold_le_job_cost : basic_facts.
diff --git a/analysis/facts/preemption/rtc_threshold/limited.v b/analysis/facts/preemption/rtc_threshold/limited.v
index 5763cb37f..0d557fd07 100644
--- a/analysis/facts/preemption/rtc_threshold/limited.v
+++ b/analysis/facts/preemption/rtc_threshold/limited.v
@@ -140,4 +140,4 @@ Section TaskRTCThresholdLimitedPreemptions.
   Qed.
   
 End TaskRTCThresholdLimitedPreemptions.
-Hint Resolve limited_valid_task_run_to_completion_threshold : basic_facts.
+Global Hint Resolve limited_valid_task_run_to_completion_threshold : basic_facts.
diff --git a/analysis/facts/preemption/rtc_threshold/nonpreemptive.v b/analysis/facts/preemption/rtc_threshold/nonpreemptive.v
index 2fba6e34c..607b14b6f 100644
--- a/analysis/facts/preemption/rtc_threshold/nonpreemptive.v
+++ b/analysis/facts/preemption/rtc_threshold/nonpreemptive.v
@@ -77,4 +77,4 @@ Section TaskRTCThresholdFullyNonPreemptive.
   Qed.
     
 End TaskRTCThresholdFullyNonPreemptive.
-Hint Resolve fully_nonpreemptive_valid_task_run_to_completion_threshold : basic_facts.
+Global Hint Resolve fully_nonpreemptive_valid_task_run_to_completion_threshold : basic_facts.
diff --git a/analysis/facts/preemption/rtc_threshold/preemptive.v b/analysis/facts/preemption/rtc_threshold/preemptive.v
index 083ef8c0e..cb6846f79 100644
--- a/analysis/facts/preemption/rtc_threshold/preemptive.v
+++ b/analysis/facts/preemption/rtc_threshold/preemptive.v
@@ -38,4 +38,4 @@ Section TaskRTCThresholdFullyPreemptiveModel.
   Qed.
     
 End TaskRTCThresholdFullyPreemptiveModel.
-Hint Resolve fully_preemptive_valid_task_run_to_completion_threshold : basic_facts.
+Global Hint Resolve fully_preemptive_valid_task_run_to_completion_threshold : basic_facts.
diff --git a/analysis/facts/preemption/task/floating.v b/analysis/facts/preemption/task/floating.v
index 3b1bb7118..92ced12af 100644
--- a/analysis/facts/preemption/task/floating.v
+++ b/analysis/facts/preemption/task/floating.v
@@ -107,7 +107,7 @@ Section FloatingNonPreemptiveRegionsModel.
 End FloatingNonPreemptiveRegionsModel.
 
 (** We add the above lemma into a "Hint Database" basic_facts, so Coq will be able to apply them automatically. *)
-Hint Resolve
+Global Hint Resolve
      valid_fixed_preemption_points_model_lemma
      floating_preemption_points_model_is_model_with_bounded_nonpreemptive_regions
      floating_preemption_points_model_is_valid_model_with_bounded_nonpreemptive_regions : basic_facts.
diff --git a/analysis/facts/preemption/task/limited.v b/analysis/facts/preemption/task/limited.v
index 98919f802..983c8c61b 100644
--- a/analysis/facts/preemption/task/limited.v
+++ b/analysis/facts/preemption/task/limited.v
@@ -109,7 +109,7 @@ Section LimitedPreemptionsModel.
 End LimitedPreemptionsModel. 
 
 (** We add the above lemma into a "Hint Database" basic_facts, so Coq will be able to apply them automatically. *)
-Hint Resolve
+Global Hint Resolve
      valid_fixed_preemption_points_model_lemma
      fixed_preemption_points_model_is_model_with_bounded_nonpreemptive_regions
      fixed_preemption_points_model_is_valid_model_with_bounded_nonpreemptive_regions : basic_facts.
diff --git a/analysis/facts/preemption/task/nonpreemptive.v b/analysis/facts/preemption/task/nonpreemptive.v
index affb46ccb..286756642 100644
--- a/analysis/facts/preemption/task/nonpreemptive.v
+++ b/analysis/facts/preemption/task/nonpreemptive.v
@@ -86,7 +86,7 @@ Section FullyNonPreemptiveModel.
 End FullyNonPreemptiveModel.
 
 (** We add the above lemma into a "Hint Database" basic_facts, so Coq will be able to apply them automatically. *)
-Hint Resolve
+Global Hint Resolve 
      valid_fully_nonpreemptive_model
      fully_nonpreemptive_model_is_model_with_bounded_nonpreemptive_regions
      fully_nonpreemptive_model_is_valid_model_with_bounded_nonpreemptive_regions : basic_facts.
diff --git a/analysis/facts/preemption/task/preemptive.v b/analysis/facts/preemption/task/preemptive.v
index 5f91aee54..8c073c259 100644
--- a/analysis/facts/preemption/task/preemptive.v
+++ b/analysis/facts/preemption/task/preemptive.v
@@ -59,7 +59,7 @@ Section FullyPreemptiveModel.
 End FullyPreemptiveModel.
 
 (** We add the above lemma into a "Hint Database" basic_facts, so Coq will be able to apply them automatically. *)
-Hint Resolve
+Global Hint Resolve
      valid_fully_preemptive_model
      fully_preemptive_model_is_model_with_bounded_nonpreemptive_regions
      fully_preemptive_model_is_valid_model_with_bounded_nonpreemptive_segments : basic_facts.
diff --git a/classic/util/tactics.v b/classic/util/tactics.v
index 35e3200f7..f334c77c3 100644
--- a/classic/util/tactics.v
+++ b/classic/util/tactics.v
@@ -69,7 +69,7 @@ Proof. by intros; case eqP. Qed.
 Lemma beq_sym : forall (T : eqType) (x y : T), (x == y) = (y == x).
 Proof. intros; do 2 case eqP; congruence. Qed.
 
-Hint Resolve beq_refl : vlib.
+Global Hint Resolve beq_refl : vlib.
 Hint Rewrite beq_refl : vlib_trivial.
 
 Notation eqxx := beq_refl.
@@ -112,7 +112,7 @@ Proof. by intros; apply/andP; split. Qed.
 
 Create HintDb vlib_refl discriminated.
 
-Hint Resolve andP orP nandP norP negP vlib__internal_eqP neqP : vlib_refl.
+Global Hint Resolve andP orP nandP norP negP vlib__internal_eqP neqP : vlib_refl.
 
 (* Add x <= y <= z splitting to the core hint database. *)
 Hint Immediate vlib__leq_split vlib__ltn_split1 vlib__ltn_split2 : core.
diff --git a/model/priority/classes.v b/model/priority/classes.v
index 900563904..8646455a9 100644
--- a/model/priority/classes.v
+++ b/model/priority/classes.v
@@ -153,4 +153,4 @@ End Priorities.
 
 (** We add the above observation into the "Hint Database" basic_facts, so Coq
     will be able to apply it automatically. *)
-Hint Resolve respects_sequential_tasks : basic_facts.
+Global Hint Resolve respects_sequential_tasks : basic_facts.
diff --git a/model/priority/deadline_monotonic.v b/model/priority/deadline_monotonic.v
index 692e65267..625606f0c 100644
--- a/model/priority/deadline_monotonic.v
+++ b/model/priority/deadline_monotonic.v
@@ -37,7 +37,7 @@ End Properties.
 
 (** We add the above lemmas into a "Hint Database" basic_facts, so Coq
     will be able to apply them automatically. *)
-Hint Resolve
+Global Hint Resolve
      DM_is_reflexive
      DM_is_transitive
      DM_is_total
diff --git a/model/priority/edf.v b/model/priority/edf.v
index 964896e05..24b052b46 100644
--- a/model/priority/edf.v
+++ b/model/priority/edf.v
@@ -37,7 +37,7 @@ End PropertiesOfEDF.
 
 (** We add the above lemmas into a "Hint Database" basic_facts, so Coq
     will be able to apply them automatically. *)
-Hint Resolve
+Global Hint Resolve
      EDF_is_reflexive
      EDF_is_transitive
      EDF_is_total
diff --git a/model/priority/fifo.v b/model/priority/fifo.v
index d146deec9..a89e24c90 100644
--- a/model/priority/fifo.v
+++ b/model/priority/fifo.v
@@ -33,7 +33,7 @@ End Properties.
 
 (** We add the above lemmas into a "Hint Database" basic_facts, so Coq
     will be able to apply them automatically. *)
-Hint Resolve
+Global Hint Resolve
      FIFO_is_reflexive
      FIFO_is_transitive
      FIFO_is_total
diff --git a/model/priority/numeric_fixed_priority.v b/model/priority/numeric_fixed_priority.v
index d5e2d2ce9..7dfb26e93 100644
--- a/model/priority/numeric_fixed_priority.v
+++ b/model/priority/numeric_fixed_priority.v
@@ -48,7 +48,7 @@ End Properties.
 
 (** We add the above lemmas into a "Hint Database" basic_facts, so Coq
     will be able to apply them automatically. *)
-Hint Resolve
+Global Hint Resolve
      NFP_is_reflexive
      NFP_is_transitive
      NFP_is_total
diff --git a/model/priority/rate_monotonic.v b/model/priority/rate_monotonic.v
index e03e80307..0af602c49 100644
--- a/model/priority/rate_monotonic.v
+++ b/model/priority/rate_monotonic.v
@@ -39,7 +39,7 @@ End Properties.
 
 (** We add the above lemmas into a "Hint Database" basic_facts, so Coq
     will be able to apply them automatically. *)
-Hint Resolve
+Global Hint Resolve
      RM_is_reflexive
      RM_is_transitive
      RM_is_total
-- 
GitLab