diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 68e72e5fc2ae4048bd286b7958a3240ad63544cc..dc2e3c01a2eabc33d71343c20a936a0f15aa426c 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -9,15 +9,10 @@ stages:
     - ./create_makefile.sh
     - make -j ${NJOBS}
 
-1.8.0-coq-8.8:
-  extends: .build
-
-1.9.0-coq-dev:
+1.9.0-coq-8.9:
   extends: .build
-  # it's ok to fail with an unreleased version of Coq
-  allow_failure: true 
 
-1.9.0-coq-8.9:
+1.9.0-coq-8.10:
   extends: .build
   # Keep track of all compiled output and the build infrastructure
   artifacts:
@@ -46,19 +41,24 @@ stages:
     - "*/*/*/*/*/*/*/*/*.glob"
     - "*/*/*/*/*/*/*/*/*/*.glob"
     expire_in: 1 week
+
+1.9.0-coq-dev:
+  extends: .build
+  # it's ok to fail with an unreleased version of Coq
+  allow_failure: true
    
 validate:
   stage: process
-  image: mathcomp/mathcomp:1.9.0-coq-8.9
+  image: mathcomp/mathcomp:1.9.0-coq-8.10
   dependencies:
-    - 1.9.0-coq-8.9
+    - 1.9.0-coq-8.10
   script: make validate
 
 doc:
   stage: process
-  image: mathcomp/mathcomp:1.9.0-coq-8.9
+  image: mathcomp/mathcomp:1.9.0-coq-8.10
   dependencies:
-    - 1.9.0-coq-8.9
+    - 1.9.0-coq-8.10
   script:
     - make html -j ${NJOBS}
     - mv html with-proofs
diff --git a/analysis/apa/bertogna_edf_comp.v b/analysis/apa/bertogna_edf_comp.v
index b12a361eccb5e5d6b8da80a9c34e2cba630622ae..c90a956617545ccccc4b27f843bd608ef1ab2585 100755
--- a/analysis/apa/bertogna_edf_comp.v
+++ b/analysis/apa/bertogna_edf_comp.v
@@ -539,7 +539,7 @@ Module ResponseTimeIterationEDF.
         (exists k, k <= max_steps ts /\ f k = f k.+1) ->
         f (max_steps ts) = f (max_steps ts).+1.
       Proof.
-        by intros EX; des; apply iter_fix with (k := k).
+        by intros EX; des; apply (@fixedpoint.iter_fix _ _ _ k).
       Qed.
 
       (* Else, we derive a contradiction. *)
@@ -999,4 +999,4 @@ Module ResponseTimeIterationEDF.
 
   End Analysis.
 
-End ResponseTimeIterationEDF.
\ No newline at end of file
+End ResponseTimeIterationEDF.
diff --git a/analysis/apa/bertogna_fp_comp.v b/analysis/apa/bertogna_fp_comp.v
index 2d73ff8321bdc5063faf33cc6a68687c4298183b..a1b9315e19db0981bed0ac98f0892d9421291b61 100644
--- a/analysis/apa/bertogna_fp_comp.v
+++ b/analysis/apa/bertogna_fp_comp.v
@@ -379,7 +379,7 @@ Module ResponseTimeIterationFP.
         (exists k, k <= max_steps tsk /\ f k = f k.+1) ->
         f (max_steps tsk) = f (max_steps tsk).+1.
       Proof.
-        by intros EX; des; apply iter_fix with (k := k).
+        by intros EX; des; apply fixedpoint.iter_fix with (k := k).
       Qed.
 
       (* Else, we derive a contradiction. *)
@@ -723,4 +723,4 @@ Module ResponseTimeIterationFP.
 
   End Analysis.
 
-End ResponseTimeIterationFP.
\ No newline at end of file
+End ResponseTimeIterationFP.
diff --git a/analysis/global/basic/bertogna_edf_comp.v b/analysis/global/basic/bertogna_edf_comp.v
index 534f815b9ca4b9bccc73dc442c242c2db458b3e0..9e4b91ebf5a135e20a9d91916c02073488fd87f0 100755
--- a/analysis/global/basic/bertogna_edf_comp.v
+++ b/analysis/global/basic/bertogna_edf_comp.v
@@ -532,7 +532,7 @@ Module ResponseTimeIterationEDF.
         (exists k, k <= max_steps ts /\ f k = f k.+1) ->
         f (max_steps ts) = f (max_steps ts).+1.
       Proof.
-        by intros EX; des; apply iter_fix with (k := k).
+        by intros EX; des; apply fixedpoint.iter_fix with (k := k).
       Qed.
 
       (* Else, we derive a contradiction. *)
@@ -987,4 +987,4 @@ Module ResponseTimeIterationEDF.
 
   End Analysis.
 
-End ResponseTimeIterationEDF.
\ No newline at end of file
+End ResponseTimeIterationEDF.
diff --git a/analysis/global/basic/bertogna_fp_comp.v b/analysis/global/basic/bertogna_fp_comp.v
index 4f7af25d41fc1f459be455d72b33d4e4f288ac34..c9114c22e6ad6193390f16df39895750485524a4 100644
--- a/analysis/global/basic/bertogna_fp_comp.v
+++ b/analysis/global/basic/bertogna_fp_comp.v
@@ -372,7 +372,7 @@ Module ResponseTimeIterationFP.
         (exists k, k <= max_steps tsk /\ f k = f k.+1) ->
         f (max_steps tsk) = f (max_steps tsk).+1.
       Proof.
-        by intros EX; des; apply iter_fix with (k := k).
+        by intros EX; des; apply fixedpoint.iter_fix with (k := k).
       Qed.
 
       (* Else, we derive a contradiction. *)
@@ -703,4 +703,4 @@ Module ResponseTimeIterationFP.
 
   End Analysis.
 
-End ResponseTimeIterationFP.
\ No newline at end of file
+End ResponseTimeIterationFP.
diff --git a/analysis/global/jitter/bertogna_edf_comp.v b/analysis/global/jitter/bertogna_edf_comp.v
index c1970889b39c9cf609b2e896b940d54e4864c7c1..fbd879c4b786eed2b3c97e79a0a68a397b3fc951 100755
--- a/analysis/global/jitter/bertogna_edf_comp.v
+++ b/analysis/global/jitter/bertogna_edf_comp.v
@@ -586,7 +586,7 @@ Module ResponseTimeIterationEDF.
         (exists k, k <= max_steps ts /\ f k = f k.+1) ->
         f (max_steps ts) = f (max_steps ts).+1.
       Proof.
-        by intros EX; des; apply iter_fix with (k := k).
+        by intros EX; des; apply fixedpoint.iter_fix with (k := k).
       Qed.
 
       (* Else, we derive a contradiction. *)
@@ -1081,4 +1081,4 @@ Module ResponseTimeIterationEDF.
 
   End Analysis.
 
-End ResponseTimeIterationEDF.
\ No newline at end of file
+End ResponseTimeIterationEDF.
diff --git a/analysis/global/jitter/bertogna_fp_comp.v b/analysis/global/jitter/bertogna_fp_comp.v
index dd320475b64bfc3a8994d539b360c05a659f84b0..fd69f2d63c4ca61c664ab05f826791031115e3ec 100644
--- a/analysis/global/jitter/bertogna_fp_comp.v
+++ b/analysis/global/jitter/bertogna_fp_comp.v
@@ -372,7 +372,7 @@ Module ResponseTimeIterationFP.
         (exists k, k <= max_steps tsk /\ f k = f k.+1) ->
         f (max_steps tsk) = f (max_steps tsk).+1.
       Proof.
-        by intros EX; des; apply iter_fix with (k := k).
+        by intros EX; des; apply fixedpoint.iter_fix with (k := k).
       Qed.
 
       (* Else, we derive a contradiction. *)
@@ -723,4 +723,4 @@ Module ResponseTimeIterationFP.
 
   End Analysis.
 
-End ResponseTimeIterationFP.
\ No newline at end of file
+End ResponseTimeIterationFP.
diff --git a/analysis/global/parallel/bertogna_edf_comp.v b/analysis/global/parallel/bertogna_edf_comp.v
index 8534205f8372b6064e92a0660f8992fd49a5d924..520341bd78a7f62341c1bc83b08192e44f0386a2 100755
--- a/analysis/global/parallel/bertogna_edf_comp.v
+++ b/analysis/global/parallel/bertogna_edf_comp.v
@@ -531,7 +531,7 @@ Module ResponseTimeIterationEDF.
         (exists k, k <= max_steps ts /\ f k = f k.+1) ->
         f (max_steps ts) = f (max_steps ts).+1.
       Proof.
-        by intros EX; des; apply iter_fix with (k := k).
+        by intros EX; des; apply fixedpoint.iter_fix with (k := k).
       Qed.
 
       (* Else, we derive a contradiction. *)
@@ -982,4 +982,4 @@ Module ResponseTimeIterationEDF.
 
   End Analysis.
 
-End ResponseTimeIterationEDF.
\ No newline at end of file
+End ResponseTimeIterationEDF.
diff --git a/analysis/global/parallel/bertogna_fp_comp.v b/analysis/global/parallel/bertogna_fp_comp.v
index a13338789a7698eb63beecc36c977653617f6a8c..b398a1e7847b157064a06cd13471ca6e603f8d63 100644
--- a/analysis/global/parallel/bertogna_fp_comp.v
+++ b/analysis/global/parallel/bertogna_fp_comp.v
@@ -362,7 +362,7 @@ Module ResponseTimeIterationFP.
         (exists k, k <= max_steps tsk /\ f k = f k.+1) ->
         f (max_steps tsk) = f (max_steps tsk).+1.
       Proof.
-        by intros EX; des; apply iter_fix with (k := k).
+        by intros EX; des; apply fixedpoint.iter_fix with (k := k).
       Qed.
 
       (* Else, we derive a contradiction. *)
@@ -686,4 +686,4 @@ Module ResponseTimeIterationFP.
 
   End Analysis.
 
-End ResponseTimeIterationFP.
\ No newline at end of file
+End ResponseTimeIterationFP.
diff --git a/restructuring/analysis/abstract/core/abstract_seq_rta.v b/restructuring/analysis/abstract/core/abstract_seq_rta.v
index f8da173fe6afbab499e29b0fcbfc658dd02d663c..1f028a88d2456f4a68298dc324f0ad35252d1596 100644
--- a/restructuring/analysis/abstract/core/abstract_seq_rta.v
+++ b/restructuring/analysis/abstract/core/abstract_seq_rta.v
@@ -429,7 +429,7 @@ Section Sequential_Abstract_RTA.
                 { by move: H_not_job_of_tsk => /eqP TSK; rewrite TSK. }
                 { by move: H_sched => /eqP SCHEDt; apply scheduled_implies_pending;
                                        auto using ideal_proc_model_ensures_ideal_progress. }
-                case ARRNEQ: (job_arrival j' <= job_arrival j).
+                case_eq (job_arrival j' <= job_arrival j) => ARRNEQ.
                 { move: ARR => /andP [РР _].
                   eapply arrived_between_implies_in_arrivals; eauto 2.
                     by apply/andP; split; last rewrite /A subnKC // addn1 ltnS.
@@ -498,7 +498,7 @@ Section Sequential_Abstract_RTA.
             2: by apply interference_plus_sched_le_serv_of_task_plus_task_interference_idle.
             have ARRs: arrives_in arr_seq j1;
               first by apply H_jobs_come_from_arrival_sequence with t; apply/eqP.
-            case TSK: (job_task j1 == tsk).
+            case_eq (job_task j1 == tsk) => TSK.
             2: by eapply interference_plus_sched_le_serv_of_task_plus_task_interference_task; [edone| apply/negbT].
             case EQ: (j == j1); [move: EQ => /eqP EQ; subst j1 | ].
             1: by apply interference_plus_sched_le_serv_of_task_plus_task_interference_j.
@@ -709,4 +709,4 @@ Section Sequential_Abstract_RTA.
 
   End ResponseTimeBound.
   
-End Sequential_Abstract_RTA.
\ No newline at end of file
+End Sequential_Abstract_RTA.
diff --git a/restructuring/model/processor/ideal.v b/restructuring/model/processor/ideal.v
index 0fdfb301230b927bd6938ca2d93e8970aa614d03..a08ca228ec8a46794cf8117e152acf5b8a36b87d 100644
--- a/restructuring/model/processor/ideal.v
+++ b/restructuring/model/processor/ideal.v
@@ -9,12 +9,12 @@ Section State.
 
   Definition processor_state := option Job.
 
-  Global Instance pstate_instance : ProcessorState Job (option Job) :=
+  Global Program Instance pstate_instance : ProcessorState Job (option Job) :=
     {
       scheduled_in j s := s == Some j;
-      service_in j s   := s == Some j
+      service_in j s   := s == Some j;
     }.
-  Proof.
-      by move=> j [j'->|].
+  Next Obligation.
+    by rewrite H.
   Defined.
 End State.
diff --git a/restructuring/model/processor/multiprocessor.v b/restructuring/model/processor/multiprocessor.v
index 77b1abbbf49f7523dc6c0a51a9369afa0bca79fd..f9a4dc60d85e216f5e6dbc5c12d4a6f0056195b1 100644
--- a/restructuring/model/processor/multiprocessor.v
+++ b/restructuring/model/processor/multiprocessor.v
@@ -13,12 +13,13 @@ Section Schedule.
 
   Definition identical_state := processor num_cpus -> processor_state.
 
-  Global Instance multiproc_state : ProcessorState Job (identical_state) :=
+  Global Program Instance multiproc_state : ProcessorState Job (identical_state) :=
     {
       scheduled_in j s := [exists cpu, scheduled_in j (s cpu)];
       service_in j s := \sum_(cpu < num_cpus) service_in j (s cpu)
     }.
-  Proof.
+  Next Obligation.
+    move: j s H0.
     move=> j s /existsP Hsched.
     apply/eqP.
     rewrite sum_nat_eq0.
diff --git a/restructuring/model/processor/spin.v b/restructuring/model/processor/spin.v
index c544709bc239b40d0c2469cf90b5a7e31e166a05..12108fc33cdd8edcaf0792fcbc7fa1fb1afd3655 100644
--- a/restructuring/model/processor/spin.v
+++ b/restructuring/model/processor/spin.v
@@ -31,12 +31,12 @@ Section State.
 
   End Service.
 
-  Global Instance pstate_instance : ProcessorState Job (processor_state) :=
+  Global Program Instance pstate_instance : ProcessorState Job (processor_state) :=
     {
       scheduled_in := scheduled_in;
       service_in   := service_in
     }.
-  Proof.
-    by move=> j [|j'|j']//=->.
+  Next Obligation.
+    by move: H; case s => //= j' ->.
   Defined.
 End State.
diff --git a/restructuring/model/processor/varspeed.v b/restructuring/model/processor/varspeed.v
index ed1e9cbd3f34db5112a98b505cfe8cbe660406f5..b31855d7fe2c8998479508e84a9cde9887c20c74 100644
--- a/restructuring/model/processor/varspeed.v
+++ b/restructuring/model/processor/varspeed.v
@@ -27,12 +27,13 @@ Section State.
 
   End Service.
 
-  Global Instance pstate_instance : ProcessorState Job processor_state :=
+  Global Program Instance pstate_instance : ProcessorState Job processor_state :=
     {
       scheduled_in := scheduled_in;
       service_in   := service_in
     }.
-  Proof.
+  Next Obligation.
+      move: j s H.
       by move=> j []//= j' s->.
   Defined.
   
diff --git a/restructuring/model/readiness/basic.v b/restructuring/model/readiness/basic.v
index 2852f526a9b916e7895d3f416211e6296c7ee369..ccda30e461d77f017c2eaacf34179526002c692c 100644
--- a/restructuring/model/readiness/basic.v
+++ b/restructuring/model/readiness/basic.v
@@ -17,11 +17,10 @@ Section LiuAndLaylandReadiness.
   Context `{JobArrival Job} `{JobCost Job}.
 
   (* In the basic Liu & Layland model, a job is ready iff it is pending. *)
-  Global Instance basic_ready_instance : JobReady Job PState :=
+  Global Program Instance basic_ready_instance : JobReady Job PState :=
     {
       job_ready sched j t := pending sched j t
     }.
-  Proof. trivial. Defined.
 
 
   (* Under this definition, a schedule satisfies that only ready jobs execute
diff --git a/restructuring/model/readiness/jitter.v b/restructuring/model/readiness/jitter.v
index 7d135dc97f4a4e2c9267c2bde11c1ccb3d17df3e..c2761cc1964341e5d8929a031bc35106be3e99bb 100644
--- a/restructuring/model/readiness/jitter.v
+++ b/restructuring/model/readiness/jitter.v
@@ -23,12 +23,12 @@ Section ReadinessOfJitteryJobs.
 
   (* A job that experiences jitter is ready only when the jitter-induced delay
      has passed after its arrival and if it is not yet complete. *)
-  Global Instance jitter_ready_instance : JobReady Job PState :=
+  Global Program Instance jitter_ready_instance : JobReady Job PState :=
     {
       job_ready sched j t := is_released j t && ~~ completed_by sched j t
     }.
-  Proof.
-    move=> sched j t /andP [REL UNFINISHED].
+  Next Obligation.
+    move: H3 => /andP [REL UNFINISHED].
     rewrite /pending. apply /andP. split => //.
     move: REL. rewrite /is_released /has_arrived.
     by apply leq_addk.
diff --git a/util/seqset.v b/util/seqset.v
index af3a5ffe58cdce34d40a023835ec1decf499d8a3..e43e47f33bb834ac161060bed7aa35da1e794515 100644
--- a/util/seqset.v
+++ b/util/seqset.v
@@ -16,7 +16,7 @@ Section SeqSet.
   Canonical Structure setSubType := [subType for _set_seq].
   Definition set_eqMixin := [eqMixin of set by <:].
   Canonical Structure set_eqType := EqType set set_eqMixin.
-  Canonical Structure mem_set_predType := mkPredType (fun (l : set) => mem_seq (_set_seq l)).
+  Canonical Structure mem_set_predType := PredType (fun (l : set) => mem_seq (_set_seq l)).
   Definition set_of of phant T := set.
 
 End SeqSet.
@@ -51,4 +51,4 @@ Section LemmasFinType.
     by move: UNIQ => /card_uniqP ->.
   Qed.
   
-End LemmasFinType.
\ No newline at end of file
+End LemmasFinType.