Fixed warnings

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.

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.
 

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.

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.

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.

analysis/facts/preemption/job/preemptive.v

@@ -65,4 +65,4 @@ Section FullyPreemptiveModel.
   Qed.    
   
 End FullyPreemptiveModel.
-Hint Resolve valid_fully_preemptive_model : basic_facts. 
+Global Hint Resolve valid_fully_preemptive_model : basic_facts. 
\ No newline at end of file

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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

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

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