From acc353bdc383913a23e213c14e84ee99cd07ea70 Mon Sep 17 00:00:00 2001 From: kimaya <f20171026@goa.bits-pilani.ac.in> Date: Mon, 25 Oct 2021 14:16:42 +0200 Subject: [PATCH] addition to basic facts --- analysis/facts/behavior/arrivals.v | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/analysis/facts/behavior/arrivals.v b/analysis/facts/behavior/arrivals.v index 3ff7f9739..7c7f02d7a 100644 --- a/analysis/facts/behavior/arrivals.v +++ b/analysis/facts/behavior/arrivals.v @@ -118,9 +118,12 @@ Section Arrived. End Arrived. -(** We add the above lemma into a "Hint Database" basic_facts, so Coq - will be able to apply it automatically. *) -Global Hint Resolve valid_schedule_implies_jobs_must_arrive_to_execute : basic_facts. +(** We add some of the above lemmas to the "Hint Database" + [basic_facts], so the [auto] tactic will be able to use them. *) +Global Hint Resolve + valid_schedule_implies_jobs_must_arrive_to_execute + jobs_must_arrive_to_be_ready + : basic_facts. (** In this section, we establish useful facts about arrival sequence prefixes. *) Section ArrivalSequencePrefix. -- GitLab