From 12f79735364abc04302929bfa86a35a308e15bc1 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Thu, 23 Jan 2020 16:57:26 +0100
Subject: [PATCH] Compile with coq dev
---
.gitignore | 2 ++
.gitlab-ci.yml | 2 +-
analysis/facts/preemption/rtc_threshold/limited.v | 2 +-
analysis/facts/preemption/task/floating.v | 2 +-
analysis/facts/preemption/task/limited.v | 2 +-
5 files changed, 6 insertions(+), 4 deletions(-)
diff --git a/.gitignore b/.gitignore
index 0c9b184f1..9db2c48a6 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 d1d476a50..4ff3e3be7 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 b35e55b2a..1d09527ff 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 fa828062e..3b1bb7118 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 40ecb21cb..98919f802 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
--
GitLab