diff --git a/.gitignore b/.gitignore
index 56dfacb64d1c7007287fed22a2bf3b9071826afc..8e3477e000956eab1fe5eeda7329dcffa726abfa 100644
--- a/.gitignore
+++ b/.gitignore
@@ -4,3 +4,4 @@
 *.html
 *.aux
 Makefile*
+_CoqProject
diff --git a/_CoqProject b/_CoqProject
deleted file mode 100644
index dcdf97e03d88df736a8e2720bf6fb99636751905..0000000000000000000000000000000000000000
--- a/_CoqProject
+++ /dev/null
@@ -1 +0,0 @@
--R . rt
\ No newline at end of file
diff --git a/analysis/apa/bertogna_edf_theory.v b/analysis/apa/bertogna_edf_theory.v
index d232320d723121fcb08770031ddfe09be97d9600..98769ae3545a8ba338a823fdb4fa4434c7dca957 100644
--- a/analysis/apa/bertogna_edf_theory.v
+++ b/analysis/apa/bertogna_edf_theory.v
@@ -919,7 +919,7 @@ Module ResponseTimeAnalysisEDF.
           rewrite -[_ < _]negbK in SUM.
           move: SUM => /negP SUM; apply SUM; rewrite -leqNgt.
           unfold I, total_interference_bound_edf.
-          rewrite big_seq_cond [\sum_(_ <- _ | let _ := _ in _)_]big_seq_cond.
+          rewrite big_seq_cond [X in _ <= X]big_seq_cond.
           apply leq_sum; move => tsk_k /andP [INBOUNDSk INTERFk]; destruct tsk_k as [tsk_k R_k].
           specialize (ALL (tsk_k, R_k) INBOUNDSk).
           unfold interference_bound_edf; simpl in *.
diff --git a/analysis/global/basic/bertogna_edf_theory.v b/analysis/global/basic/bertogna_edf_theory.v
index 4ae30ee049436d4c4f10c9782de61e6d354e7fe0..484620b75400076f36cf33eec4b80ec161067529 100644
--- a/analysis/global/basic/bertogna_edf_theory.v
+++ b/analysis/global/basic/bertogna_edf_theory.v
@@ -719,7 +719,7 @@ Module ResponseTimeAnalysisEDF.
           rewrite -[_ < _]negbK in SUM.
           move: SUM => /negP SUM; apply SUM; rewrite -leqNgt.
           unfold I, total_interference_bound_edf.
-          rewrite big_seq_cond [\sum_(_ <- _ | let _ := _ in _)_]big_seq_cond.
+          rewrite big_seq_cond [X in _ <= X]big_seq_cond.
           apply leq_sum; move => tsk_k /andP [INBOUNDSk INTERFk]; destruct tsk_k as [tsk_k R_k].
           specialize (ALL (tsk_k, R_k) INBOUNDSk).
           unfold interference_bound_edf; simpl in *.
diff --git a/analysis/global/jitter/bertogna_edf_theory.v b/analysis/global/jitter/bertogna_edf_theory.v
index fa969ae1e11b0ac47b61a5bfd32e0d306884146e..639feb34c01cb5574d578cde5d9798d1f3dc8899 100644
--- a/analysis/global/jitter/bertogna_edf_theory.v
+++ b/analysis/global/jitter/bertogna_edf_theory.v
@@ -761,7 +761,7 @@ Module ResponseTimeAnalysisEDFJitter.
             rewrite -[_ < _]negbK in SUM.
             move: SUM => /negP SUM; apply SUM; rewrite -leqNgt.
             unfold I, total_interference_bound_edf.
-            rewrite big_seq_cond [\sum_(_ <- _ | let _ := _ in _)_]big_seq_cond.
+            rewrite big_seq_cond [X in _ <= X]big_seq_cond.
             apply leq_sum; move => tsk_k /andP [INBOUNDSk INTERFk]; destruct tsk_k as [tsk_k R_k].
             specialize (ALL (tsk_k, R_k) INBOUNDSk).
             unfold interference_bound_edf; simpl in *.
diff --git a/analysis/global/parallel/bertogna_edf_theory.v b/analysis/global/parallel/bertogna_edf_theory.v
index a36dc8a557e001269f88993d6e75de93f4637ac7..061a619fd05f1ac89255812e9aa28854688968ec 100644
--- a/analysis/global/parallel/bertogna_edf_theory.v
+++ b/analysis/global/parallel/bertogna_edf_theory.v
@@ -415,7 +415,7 @@ Module ResponseTimeAnalysisEDF.
           rewrite -[_ < _]negbK in SUM.
           move: SUM => /negP SUM; apply SUM; rewrite -leqNgt.
           unfold I, total_interference_bound_edf.
-          rewrite big_seq_cond [\sum_(_ <- _ | let _ := _ in _)_]big_seq_cond.
+          rewrite big_seq_cond [X in _ <= X]big_seq_cond.
           apply leq_sum; move => tsk_k /andP [INBOUNDSk INTERFk]; destruct tsk_k as [tsk_k R_k].
           specialize (ALL (tsk_k, R_k) INBOUNDSk).
           unfold interference_bound_edf; simpl in *.
diff --git a/create_makefile.sh b/create_makefile.sh
index 89c3e0560f1fb060adc857eecfc5e82e00ed9daf..4b9635fa14df45840b183266ebb6121ace5a311f 100755
--- a/create_makefile.sh
+++ b/create_makefile.sh
@@ -1,3 +1,13 @@
+#!/bin/bash 
+
+# Include rt-proofs library in _CoqProject. (For Coq versions >= 8.6, remove spurious warnings.)
+version=$(echo $(coqc -v 1) | grep -o "version .\.." | tail -c 4)
+if ([ "$version" == "8.4" ] || [ "$version" == "8.5" ]) then
+  echo "-R . rt" > _CoqProject
+else
+  echo -R . rt -arg \"-w -notation-overriden,-parsing\" > _CoqProject
+fi
+
 # Compile all *.v files (except the ones that define the decidable equality). Those
 # are directly included in other files.
 coq_makefile -f _CoqProject $(find . -name "*.v" ! -name "*#*" ! -name "*eqdec*.v" -print) -o Makefile
diff --git a/model/schedule/global/jitter/interference.v b/model/schedule/global/jitter/interference.v
index 15b6addb67eba229faa972ab4027b6bd55ff7d46..f4525641fafba114e6e965503ea3a0e046c5b521 100644
--- a/model/schedule/global/jitter/interference.v
+++ b/model/schedule/global/jitter/interference.v
@@ -3,6 +3,8 @@ Require Import rt.model.arrival.basic.task rt.model.priority rt.model.schedule.g
 Require Import rt.model.schedule.global.jitter.job rt.model.schedule.global.jitter.schedule.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
+Require rt.model.schedule.global.basic.interference.
+
 Module Interference.
 
   Import ScheduleOfSporadicTaskWithJitter Priority Workload.
@@ -10,7 +12,7 @@ Module Interference.
   (* We import some of the basic definitions, but we need to re-define almost everything
      since the definition of backlogged (and thus the definition of interference)
      changes with jitter. *)
-  Require Import rt.model.schedule.global.basic.interference.
+  Import rt.model.schedule.global.basic.interference.
   Export Interference.
   
   Section InterferenceDefs.
diff --git a/model/schedule/global/jitter/schedule.v b/model/schedule/global/jitter/schedule.v
index fe904b305eeae49765c599542d873766670af03b..2a7e37f4c073614a607f7529ceb6bdffd6a304a9 100644
--- a/model/schedule/global/jitter/schedule.v
+++ b/model/schedule/global/jitter/schedule.v
@@ -3,11 +3,13 @@ Require Import rt.model.arrival.basic.task.
 Require Import rt.model.schedule.global.jitter.job rt.model.arrival.basic.arrival_sequence.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
+Require rt.model.schedule.global.basic.schedule.
+
 (* Definition, properties and lemmas about schedules. *)
 Module ScheduleWithJitter.
 
   (* We import the original schedule module and redefine whatever is required. *)
-  Require Export rt.model.schedule.global.basic.schedule.
+  Export rt.model.schedule.global.basic.schedule.
   Export ArrivalSequence Schedule.
   
   (* We need to redefine the properties of a job that depend on the arrival time. *)
diff --git a/model/schedule/partitioned/schedulability.v b/model/schedule/partitioned/schedulability.v
index f7994ac526a2b8b4c7d0754e3ba38f2e85523416..42081b6dca83e57ba89b5c01ec581446a92f73db 100644
--- a/model/schedule/partitioned/schedulability.v
+++ b/model/schedule/partitioned/schedulability.v
@@ -5,9 +5,10 @@ Require Import rt.model.schedule.global.basic.schedule.
 Require Import rt.model.schedule.partitioned.schedule.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
-Module PartitionSchedulability.
+Require rt.model.schedule.uni.schedule.
 
-  Require rt.model.schedule.uni.schedule.
+Module PartitionSchedulability.
+  
   Module uni_sched := rt.model.schedule.uni.schedulability.Schedulability.
   Import ArrivalSequence Partitioned Schedule Schedulability.
 
diff --git a/util/tactics.v b/util/tactics.v
index cff319faa75bc1300d11d4577a0ded56fab883e6..3ba97cf5187feed9cdbbbf7583a48f32f64d939f 100644
--- a/util/tactics.v
+++ b/util/tactics.v
@@ -412,7 +412,7 @@ Ltac feed H :=
     assert foo as FOO; [|specialize (H FOO); clear FOO]
   end.
 
-Ltac feed_n n H := match constr:n with
+Ltac feed_n n H := match constr:(n) with
   | O => idtac
   | (S ?m) => feed H ; [| feed_n m H]
                    end.