diff --git a/behavior/schedule/completion_facts.v b/behavior/facts/completion.v similarity index 99% rename from behavior/schedule/completion_facts.v rename to behavior/facts/completion.v index 90a8709275b7ecc9659d3a1617d63e0fb4a92450..0caad7209f3419b2b26b20e269475e0c4ff6d579 100644 --- a/behavior/schedule/completion_facts.v +++ b/behavior/facts/completion.v @@ -1,4 +1,5 @@ -From rt.behavior.schedule Require Export schedule service_facts. +From rt.behavior.schedule Require Export schedule. +From rt.behavior.facts Require Export service. (** In this file, we establish basic facts about job completions. *) diff --git a/behavior/schedule/service_facts.v b/behavior/facts/service.v similarity index 100% rename from behavior/schedule/service_facts.v rename to behavior/facts/service.v