Compile with coq dev

.gitignore

 *.d
 *.glob
 *.vo
+*.vos
+*.vok
 *.html
 /html
 *.aux

.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

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

analysis/facts/preemption/task/floating.v

 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

analysis/facts/preemption/task/limited.v

 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