diff --git a/.gitignore b/.gitignore
index 0c9b184f16e43415dc597977e9636868a75480a6..9db2c48a6d4d5b5a7b959467112a00f777d7d6ad 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,6 +1,8 @@
 *.d
 *.glob
 *.vo
+*.vos
+*.vok
 *.html
 /html
 *.aux
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index d1d476a50da9a3efa0f19b26ce4fd35248fed55c..4ff3e3be7a308db6f096fa2a7811b6fbadcf7ddd 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -69,7 +69,7 @@ spell-check:
 1.9.0-coq-8.9:
   extends: .build
 
-1.9.0-coq-dev:
+1.10.0-coq-dev:
   extends:
     - .build
   # it's ok to fail with an unreleased version of Coq
diff --git a/analysis/facts/preemption/rtc_threshold/limited.v b/analysis/facts/preemption/rtc_threshold/limited.v
index b35e55b2a256ed8327c2309ad38a5db6e40baf1f..1d09527ff4d906642b9afed91798cb6582ba06ff 100644
--- a/analysis/facts/preemption/rtc_threshold/limited.v
+++ b/analysis/facts/preemption/rtc_threshold/limited.v
@@ -2,8 +2,8 @@ Require Export prosa.analysis.facts.preemption.task.limited.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.job_preemptable.
 
 (** Furthermore, we assume the task model with fixed preemption points. *)
-Require Import prosa.model.preemption.limited_preemptive.
 Require Import prosa.model.task.preemption.limited_preemptive.
+Require Import prosa.model.preemption.limited_preemptive.
 
 (** * Task's Run to Completion Threshold *)
 (** In this section, we prove that instantiation of function [task run
diff --git a/analysis/facts/preemption/task/floating.v b/analysis/facts/preemption/task/floating.v
index fa828062e89ab2ba72d252b4ddffc4b637d650d7..3b1bb7118097836344f9c085624a8ceb788d1542 100644
--- a/analysis/facts/preemption/task/floating.v
+++ b/analysis/facts/preemption/task/floating.v
@@ -1,8 +1,8 @@
 Require Export prosa.analysis.facts.preemption.job.limited.
 
 (** Furthermore, we assume the task model with floating non-preemptive regions. *)
-Require Import prosa.model.preemption.limited_preemptive.
 Require Import prosa.model.task.preemption.floating_nonpreemptive.
+Require Import prosa.model.preemption.limited_preemptive.
 
 (** * Platform for Floating Non-Preemptive Regions Model *)
 (** In this section, we prove that instantiation of functions
diff --git a/analysis/facts/preemption/task/limited.v b/analysis/facts/preemption/task/limited.v
index 40ecb21cbb818ac9b75019d764d17d54b3af6a05..98919f8026dcce0782052ddd0d49a079d9893348 100644
--- a/analysis/facts/preemption/task/limited.v
+++ b/analysis/facts/preemption/task/limited.v
@@ -1,8 +1,8 @@
 Require Export prosa.analysis.facts.preemption.job.limited.
 
 (** Furthermore, we assume the task model with fixed preemption points. *)
-Require Import prosa.model.preemption.limited_preemptive.
 Require Import prosa.model.task.preemption.limited_preemptive.
+Require Import prosa.model.preemption.limited_preemptive.
 
 (** * Platform for Models with Limited Preemptions *)
 (** In this section, we prove that instantiation of functions