From e8f5fb9a90ab977994ace727b812ec5d9bdc96a3 Mon Sep 17 00:00:00 2001
From: Sergey Bozhko <sbozhko@mpi-sws.org>
Date: Fri, 13 Oct 2023 15:02:21 +0000
Subject: [PATCH] import ssreflect only once
Prosa redefines ssreflect's tactic [done] in file [util/tactics.v]. To prevent shadowing of the new [done] by ssreflect's [done], [tactics.v] should be imported _after_ ssreflect
---
README.md | 10 ++++++++++
analysis/abstract/ideal/abstract_rta.v | 2 --
analysis/abstract/search_space.v | 1 -
analysis/definitions/carry_in.v | 1 -
analysis/definitions/completion_sequence.v | 1 -
analysis/definitions/hyperperiod.v | 1 -
analysis/facts/model/ideal/service_of_jobs.v | 2 --
analysis/facts/model/service_of_jobs.v | 4 +---
analysis/facts/tdma.v | 1 -
analysis/facts/transform/edf_opt.v | 1 -
analysis/facts/transform/wc_correctness.v | 2 --
analysis/transform/prefix.v | 1 -
behavior/arrival_sequence.v | 1 -
behavior/job.v | 2 +-
behavior/ready.v | 1 -
behavior/schedule.v | 1 -
doc/guidelines.md | 2 +-
.../definitions/extrapolated_arrival_curve.v | 1 -
implementation/facts/extrapolated_arrival_curve.v | 1 -
implementation/facts/generic_schedule.v | 1 -
model/priority/definitions.v | 2 --
model/processor/ideal.v | 1 -
model/processor/multiprocessor.v | 1 -
model/processor/spin.v | 1 -
model/processor/varspeed.v | 1 -
model/readiness/jitter.v | 2 --
model/schedule/edf.v | 1 -
model/schedule/tdma.v | 1 -
results/edf/rta/bounded_pi.v | 2 --
results/edf/rta/floating_nonpreemptive.v | 2 --
results/edf/rta/fully_nonpreemptive.v | 2 --
results/edf/rta/fully_preemptive.v | 2 --
results/edf/rta/limited_preemptive.v | 2 --
results/elf/generality.v | 1 -
results/elf/rta/bounded_pi.v | 2 --
results/fifo/rta.v | 2 --
results/fixed_priority/rta/comp/fully_preemptive.v | 2 --
results/fixed_priority/rta/floating_nonpreemptive.v | 2 --
results/fixed_priority/rta/fully_nonpreemptive.v | 2 --
results/fixed_priority/rta/fully_preemptive.v | 2 --
results/fixed_priority/rta/limited_preemptive.v | 2 --
results/gel/generality.v | 1 -
results/gel/rta/bounded_pi.v | 1 -
util/all.v | 4 +++-
44 files changed, 16 insertions(+), 62 deletions(-)
diff --git a/README.md b/README.md
index fcf386b3a..e1c750a57 100644
--- a/README.md
+++ b/README.md
@@ -40,6 +40,16 @@ Furthermore, there are a couple of additional folders and modules.
- [`util`](util/): A collection of miscellaneous "helper" lemmas and tactics. Used throughout the rest of Prosa.
- [`scripts/`](scripts/): Scripts and supporting resources required for continuous integration and documentation generation.
+
+## Side-effects
+
+Importing Prosa changes the behavior of ssreflect's `done` tactic by adding basic lemmas about real-time systems.
+
+```
+Ltac done := solve [ ssreflect.done | eauto 4 with basic_rt_facts ].
+```
+
+
## Installation
### With the OCaml Package Manager (`opam`)
diff --git a/analysis/abstract/ideal/abstract_rta.v b/analysis/abstract/ideal/abstract_rta.v
index 50695a0e0..18d4ab502 100644
--- a/analysis/abstract/ideal/abstract_rta.v
+++ b/analysis/abstract/ideal/abstract_rta.v
@@ -1,5 +1,3 @@
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
Require Export prosa.analysis.facts.model.ideal.schedule.
Require Export prosa.analysis.definitions.schedulability.
Require Export prosa.analysis.abstract.search_space.
diff --git a/analysis/abstract/search_space.v b/analysis/abstract/search_space.v
index b52a3559c..6e3291a51 100644
--- a/analysis/abstract/search_space.v
+++ b/analysis/abstract/search_space.v
@@ -1,4 +1,3 @@
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
Require Import prosa.util.epsilon.
Require Import prosa.util.tactics.
Require Import prosa.model.task.concept.
diff --git a/analysis/definitions/carry_in.v b/analysis/definitions/carry_in.v
index dc49b2269..8196290f3 100644
--- a/analysis/definitions/carry_in.v
+++ b/analysis/definitions/carry_in.v
@@ -1,4 +1,3 @@
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Require Export prosa.model.priority.classes.
(** * No Carry-In *)
diff --git a/analysis/definitions/completion_sequence.v b/analysis/definitions/completion_sequence.v
index c3a34a49e..5c86391f1 100644
--- a/analysis/definitions/completion_sequence.v
+++ b/analysis/definitions/completion_sequence.v
@@ -1,4 +1,3 @@
-From mathcomp Require Export ssreflect seq ssrnat ssrbool eqtype.
Require Import prosa.behavior.service.
(** This module contains basic definitions and properties of job
diff --git a/analysis/definitions/hyperperiod.v b/analysis/definitions/hyperperiod.v
index a3754188b..158ebeb5e 100644
--- a/analysis/definitions/hyperperiod.v
+++ b/analysis/definitions/hyperperiod.v
@@ -1,4 +1,3 @@
-From mathcomp Require Import div.
Require Export prosa.model.task.arrival.periodic.
Require Export prosa.util.lcmseq.
diff --git a/analysis/facts/model/ideal/service_of_jobs.v b/analysis/facts/model/ideal/service_of_jobs.v
index 8fd510e37..e2d9ff4ab 100644
--- a/analysis/facts/model/ideal/service_of_jobs.v
+++ b/analysis/facts/model/ideal/service_of_jobs.v
@@ -1,5 +1,3 @@
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
-
Require Export prosa.model.schedule.scheduled.
Require Export prosa.model.aggregate.workload.
Require Export prosa.model.aggregate.service_of_jobs.
diff --git a/analysis/facts/model/service_of_jobs.v b/analysis/facts/model/service_of_jobs.v
index 54256026c..d59a9cb21 100644
--- a/analysis/facts/model/service_of_jobs.v
+++ b/analysis/facts/model/service_of_jobs.v
@@ -1,5 +1,3 @@
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
-
Require Export prosa.model.aggregate.workload.
Require Export prosa.model.aggregate.service_of_jobs.
Require Export prosa.analysis.facts.behavior.completion.
@@ -270,7 +268,7 @@ Section UnitServiceModelLemmas.
[by left |right]; apply negbT in EQU; rewrite leqNgt. }
move: (F1 t_compl t1) => /orP [LT | GT].
- rewrite /service_of_jobs /service_during in EQ.
- rewrite exchange_big big_geq //= in EQ; last by rewrite ltnW.
+ rewrite exchange_big big_geq //= in EQ.
rewrite /workload_of_jobs in EQ.
rewrite (big_rem j) ?Pj //= in EQ.
move: EQ => /eqP; rewrite addn_eq0; move => /andP [CZ _].
diff --git a/analysis/facts/tdma.v b/analysis/facts/tdma.v
index b10aa7954..6df95f339 100644
--- a/analysis/facts/tdma.v
+++ b/analysis/facts/tdma.v
@@ -1,4 +1,3 @@
-From mathcomp Require Import div.
Require Export prosa.model.schedule.tdma.
Require Import prosa.util.all.
diff --git a/analysis/facts/transform/edf_opt.v b/analysis/facts/transform/edf_opt.v
index 5c21cd52f..688aefebe 100644
--- a/analysis/facts/transform/edf_opt.v
+++ b/analysis/facts/transform/edf_opt.v
@@ -1,4 +1,3 @@
-From mathcomp Require Import ssrnat ssrbool fintype.
Require Import prosa.model.readiness.basic.
Require Export prosa.model.schedule.edf.
Require Export prosa.analysis.definitions.schedulability.
diff --git a/analysis/facts/transform/wc_correctness.v b/analysis/facts/transform/wc_correctness.v
index 9c6670110..2eee23eb7 100644
--- a/analysis/facts/transform/wc_correctness.v
+++ b/analysis/facts/transform/wc_correctness.v
@@ -1,5 +1,3 @@
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
-
Require Export prosa.model.schedule.work_conserving.
Require Import prosa.model.readiness.basic.
Require Export prosa.analysis.facts.model.ideal.schedule.
diff --git a/analysis/transform/prefix.v b/analysis/transform/prefix.v
index 82f976f51..08f5e2738 100644
--- a/analysis/transform/prefix.v
+++ b/analysis/transform/prefix.v
@@ -1,4 +1,3 @@
-From mathcomp Require Import ssrnat ssrbool fintype.
Require Export prosa.analysis.facts.behavior.all.
(** This file provides an operation that transforms a finite prefix of
diff --git a/behavior/arrival_sequence.v b/behavior/arrival_sequence.v
index 4e9fde5ad..c10efb323 100644
--- a/behavior/arrival_sequence.v
+++ b/behavior/arrival_sequence.v
@@ -1,4 +1,3 @@
-From mathcomp Require Export ssreflect seq ssrnat ssrbool bigop eqtype ssrfun.
Require Export prosa.behavior.job.
Require Export prosa.util.notation.
diff --git a/behavior/job.v b/behavior/job.v
index d008c8219..d9355ee3e 100644
--- a/behavior/job.v
+++ b/behavior/job.v
@@ -1,4 +1,4 @@
-From mathcomp Require Export eqtype ssrnat.
+Require Export prosa.util.all.
Require Export prosa.behavior.time.
(** * Notion of a Job Type *)
diff --git a/behavior/ready.v b/behavior/ready.v
index d41858ae4..bc759ae88 100644
--- a/behavior/ready.v
+++ b/behavior/ready.v
@@ -1,4 +1,3 @@
-From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
Require Export prosa.behavior.service.
(** * Readiness of a Job *)
diff --git a/behavior/schedule.v b/behavior/schedule.v
index 5b8fcc5a4..9cb5b819e 100644
--- a/behavior/schedule.v
+++ b/behavior/schedule.v
@@ -1,4 +1,3 @@
-From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
Require Export prosa.behavior.arrival_sequence.
(** * Generic Processor State Interface *)
diff --git a/doc/guidelines.md b/doc/guidelines.md
index 52e3cb331..0505a0284 100644
--- a/doc/guidelines.md
+++ b/doc/guidelines.md
@@ -96,7 +96,7 @@ Exception to this rule: ssreflect and other standard library imports.
3. As an important exception to the prior rule, do not re-export modules that contain type class instance definitions. Prosa uses type class instances to express key modeling choices; such assumptions should be made explicitly.
4. Always require external libraries first, i.e., *before* stating any Prosa-internal dependencies. This way, an addition in external libraries
cannot shadow a definition in Prosa. For example, require `mathcomp` modules before any modules in the `prosa` namespace.
-
+5. Do not import `mathcomp` modules outside of the `util/all.v` file. The file `util/tactics.v` redefined the behavior of the `done` tactic; hence, it must be imported after the `mathcomp` modules.
## Stating Lemmas and Theorems
diff --git a/implementation/definitions/extrapolated_arrival_curve.v b/implementation/definitions/extrapolated_arrival_curve.v
index 3cfa60b36..91e7c7ddf 100644
--- a/implementation/definitions/extrapolated_arrival_curve.v
+++ b/implementation/definitions/extrapolated_arrival_curve.v
@@ -1,4 +1,3 @@
-From mathcomp Require Export ssreflect ssrbool eqtype ssrnat div seq path fintype bigop.
Require Export prosa.behavior.time.
Require Export prosa.util.all.
diff --git a/implementation/facts/extrapolated_arrival_curve.v b/implementation/facts/extrapolated_arrival_curve.v
index 1f77ace05..97e120f0e 100644
--- a/implementation/facts/extrapolated_arrival_curve.v
+++ b/implementation/facts/extrapolated_arrival_curve.v
@@ -1,4 +1,3 @@
-From mathcomp Require Export ssreflect ssrbool eqtype ssrnat div seq path fintype bigop.
Require Export prosa.behavior.time.
Require Export prosa.util.all.
Require Export prosa.implementation.definitions.extrapolated_arrival_curve.
diff --git a/implementation/facts/generic_schedule.v b/implementation/facts/generic_schedule.v
index 6de5e8de0..8b368c3e1 100644
--- a/implementation/facts/generic_schedule.v
+++ b/implementation/facts/generic_schedule.v
@@ -1,4 +1,3 @@
-From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
Require Export prosa.implementation.definitions.generic_scheduler.
Require Export prosa.analysis.facts.transform.replace_at.
diff --git a/model/priority/definitions.v b/model/priority/definitions.v
index 92f63fa1d..c35939f6c 100644
--- a/model/priority/definitions.v
+++ b/model/priority/definitions.v
@@ -1,5 +1,3 @@
-From mathcomp Require Export seq.
-
Require Export prosa.model.task.concept.
Require Export prosa.util.rel.
Require Export prosa.util.list.
diff --git a/model/processor/ideal.v b/model/processor/ideal.v
index 5f76b4afc..c9576e175 100644
--- a/model/processor/ideal.v
+++ b/model/processor/ideal.v
@@ -1,4 +1,3 @@
-From mathcomp Require Import all_ssreflect.
Require Export prosa.behavior.all.
(** * The Ideal Uniprocessor Model *)
diff --git a/model/processor/multiprocessor.v b/model/processor/multiprocessor.v
index abe5efbab..a0faaa1cc 100644
--- a/model/processor/multiprocessor.v
+++ b/model/processor/multiprocessor.v
@@ -1,4 +1,3 @@
-From mathcomp Require Export fintype.
Require Export prosa.behavior.all.
Require Import prosa.analysis.facts.behavior.service.
diff --git a/model/processor/spin.v b/model/processor/spin.v
index ec68bf12c..9cce1357f 100644
--- a/model/processor/spin.v
+++ b/model/processor/spin.v
@@ -1,4 +1,3 @@
-From mathcomp Require Import all_ssreflect.
Require Export prosa.behavior.all.
(** In the following, we define a processor state that includes the possibility
diff --git a/model/processor/varspeed.v b/model/processor/varspeed.v
index 817fdaa88..87393a987 100644
--- a/model/processor/varspeed.v
+++ b/model/processor/varspeed.v
@@ -1,4 +1,3 @@
-From mathcomp Require Import all_ssreflect.
Require Export prosa.behavior.all.
(** In the following, we define a model of processors with variable execution
diff --git a/model/readiness/jitter.v b/model/readiness/jitter.v
index 816cf6cb1..ee35fef54 100644
--- a/model/readiness/jitter.v
+++ b/model/readiness/jitter.v
@@ -1,5 +1,3 @@
-From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
-
Require Export prosa.behavior.all.
Require Import prosa.util.nat.
diff --git a/model/schedule/edf.v b/model/schedule/edf.v
index 947d79c58..dcfcf7193 100644
--- a/model/schedule/edf.v
+++ b/model/schedule/edf.v
@@ -1,4 +1,3 @@
-From mathcomp Require Import ssrnat ssrbool fintype.
Require Export prosa.behavior.all.
(** * Fully-Preemptive EDF Schedules *)
diff --git a/model/schedule/tdma.v b/model/schedule/tdma.v
index 2441b1e7e..c2d4a485b 100644
--- a/model/schedule/tdma.v
+++ b/model/schedule/tdma.v
@@ -1,4 +1,3 @@
-From mathcomp Require Import div.
Require Export prosa.model.task.concept.
Require Export prosa.util.seqset.
Require Export prosa.util.rel.
diff --git a/results/edf/rta/bounded_pi.v b/results/edf/rta/bounded_pi.v
index 9b0bc644d..c3be107a7 100644
--- a/results/edf/rta/bounded_pi.v
+++ b/results/edf/rta/bounded_pi.v
@@ -1,5 +1,3 @@
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
Require Export prosa.analysis.facts.priority.edf.
Require Export prosa.analysis.definitions.schedulability.
Require Import prosa.model.readiness.basic.
diff --git a/results/edf/rta/floating_nonpreemptive.v b/results/edf/rta/floating_nonpreemptive.v
index 61e215582..15f0d4090 100644
--- a/results/edf/rta/floating_nonpreemptive.v
+++ b/results/edf/rta/floating_nonpreemptive.v
@@ -1,5 +1,3 @@
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
Require Import prosa.model.readiness.basic.
Require Export prosa.results.edf.rta.bounded_nps.
Require Export prosa.analysis.facts.preemption.rtc_threshold.floating.
diff --git a/results/edf/rta/fully_nonpreemptive.v b/results/edf/rta/fully_nonpreemptive.v
index 03912bdb2..b8fecdff0 100644
--- a/results/edf/rta/fully_nonpreemptive.v
+++ b/results/edf/rta/fully_nonpreemptive.v
@@ -1,5 +1,3 @@
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
Require Import prosa.model.readiness.basic.
Require Export prosa.results.edf.rta.bounded_nps.
Require Export prosa.analysis.facts.preemption.task.nonpreemptive.
diff --git a/results/edf/rta/fully_preemptive.v b/results/edf/rta/fully_preemptive.v
index c3942cf47..06ac3de45 100644
--- a/results/edf/rta/fully_preemptive.v
+++ b/results/edf/rta/fully_preemptive.v
@@ -1,5 +1,3 @@
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
Require Import prosa.model.readiness.basic.
Require Import prosa.results.edf.rta.bounded_nps.
Require Export prosa.analysis.facts.preemption.task.preemptive.
diff --git a/results/edf/rta/limited_preemptive.v b/results/edf/rta/limited_preemptive.v
index f70c1b064..2d96af80c 100644
--- a/results/edf/rta/limited_preemptive.v
+++ b/results/edf/rta/limited_preemptive.v
@@ -1,5 +1,3 @@
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
Require Export prosa.model.readiness.basic.
Require Export prosa.results.edf.rta.bounded_nps.
Require Export prosa.analysis.facts.preemption.rtc_threshold.limited.
diff --git a/results/elf/generality.v b/results/elf/generality.v
index c9d31d347..4185cd03a 100644
--- a/results/elf/generality.v
+++ b/results/elf/generality.v
@@ -1,4 +1,3 @@
-From mathcomp Require Import eqtype ssrnat seq path fintype bigop.
Require Export prosa.util.int.
Require Export prosa.model.schedule.priority_driven.
Require Export prosa.model.priority.elf.
diff --git a/results/elf/rta/bounded_pi.v b/results/elf/rta/bounded_pi.v
index 805e7b7e5..c72931a47 100644
--- a/results/elf/rta/bounded_pi.v
+++ b/results/elf/rta/bounded_pi.v
@@ -1,5 +1,3 @@
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop ssrZ.
-
Require Import prosa.util.int.
Require Export prosa.analysis.abstract.ideal.cumulative_bounds.
Require Export prosa.analysis.facts.priority.elf.
diff --git a/results/fifo/rta.v b/results/fifo/rta.v
index b1f874465..acf80934b 100644
--- a/results/fifo/rta.v
+++ b/results/fifo/rta.v
@@ -1,5 +1,3 @@
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
Require Import prosa.model.readiness.basic.
Require Import prosa.model.priority.fifo.
Require Import prosa.analysis.facts.priority.fifo.
diff --git a/results/fixed_priority/rta/comp/fully_preemptive.v b/results/fixed_priority/rta/comp/fully_preemptive.v
index ca6dc82b0..e8f17ffe4 100644
--- a/results/fixed_priority/rta/comp/fully_preemptive.v
+++ b/results/fixed_priority/rta/comp/fully_preemptive.v
@@ -1,5 +1,3 @@
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
Require Export prosa.util.fixpoint.
Require Export prosa.results.fixed_priority.rta.fully_preemptive.
diff --git a/results/fixed_priority/rta/floating_nonpreemptive.v b/results/fixed_priority/rta/floating_nonpreemptive.v
index 431649a01..862e36446 100644
--- a/results/fixed_priority/rta/floating_nonpreemptive.v
+++ b/results/fixed_priority/rta/floating_nonpreemptive.v
@@ -1,5 +1,3 @@
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
Require Export prosa.results.fixed_priority.rta.bounded_nps.
Require Export prosa.analysis.facts.preemption.rtc_threshold.floating.
Require Export prosa.analysis.facts.readiness.sequential.
diff --git a/results/fixed_priority/rta/fully_nonpreemptive.v b/results/fixed_priority/rta/fully_nonpreemptive.v
index f9557ec2a..9d71593e2 100644
--- a/results/fixed_priority/rta/fully_nonpreemptive.v
+++ b/results/fixed_priority/rta/fully_nonpreemptive.v
@@ -1,5 +1,3 @@
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
Require Export prosa.results.fixed_priority.rta.bounded_nps.
Require Export prosa.analysis.facts.preemption.task.nonpreemptive.
Require Export prosa.analysis.facts.preemption.rtc_threshold.nonpreemptive.
diff --git a/results/fixed_priority/rta/fully_preemptive.v b/results/fixed_priority/rta/fully_preemptive.v
index f32f85490..50300c5c2 100644
--- a/results/fixed_priority/rta/fully_preemptive.v
+++ b/results/fixed_priority/rta/fully_preemptive.v
@@ -1,5 +1,3 @@
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
Require Export prosa.results.fixed_priority.rta.bounded_nps.
Require Export prosa.analysis.facts.preemption.task.preemptive.
Require Export prosa.analysis.facts.preemption.rtc_threshold.preemptive.
diff --git a/results/fixed_priority/rta/limited_preemptive.v b/results/fixed_priority/rta/limited_preemptive.v
index e7ee5be84..e99c04f08 100644
--- a/results/fixed_priority/rta/limited_preemptive.v
+++ b/results/fixed_priority/rta/limited_preemptive.v
@@ -1,5 +1,3 @@
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
Require Export prosa.results.fixed_priority.rta.bounded_nps.
Require Export prosa.analysis.facts.preemption.rtc_threshold.limited.
Require Export prosa.analysis.facts.readiness.sequential.
diff --git a/results/gel/generality.v b/results/gel/generality.v
index 4427c84c8..fdee5d13e 100644
--- a/results/gel/generality.v
+++ b/results/gel/generality.v
@@ -1,4 +1,3 @@
-From mathcomp Require Import eqtype ssrnat seq path fintype bigop.
Require Export prosa.util.int.
Require Export prosa.model.schedule.priority_driven.
Require Export prosa.model.priority.gel.
diff --git a/results/gel/rta/bounded_pi.v b/results/gel/rta/bounded_pi.v
index 81366f9e2..55ce7a7d5 100644
--- a/results/gel/rta/bounded_pi.v
+++ b/results/gel/rta/bounded_pi.v
@@ -1,4 +1,3 @@
-From mathcomp Require Import eqtype ssrnat seq path fintype bigop.
Require Import prosa.util.int.
Require Import prosa.model.readiness.basic.
Require Import prosa.analysis.abstract.ideal.cumulative_bounds.
diff --git a/util/all.v b/util/all.v
index ca17d35f7..41809cc80 100644
--- a/util/all.v
+++ b/util/all.v
@@ -1,5 +1,6 @@
+From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
+
Require Export mathcomp.zify.zify.
-Require Export prosa.util.tactics.
Require Export prosa.util.notation.
Require Export prosa.util.bigcat.
Require Export prosa.util.div_mod.
@@ -15,3 +16,4 @@ Require Export prosa.util.minmax.
Require Export prosa.util.supremum.
Require Export prosa.util.nondecreasing.
Require Export prosa.util.setoid.
+Require Export prosa.util.tactics.
--
GitLab