diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 4e296ed41c5e626aa6e3f8b9d618611fea8f167d..85f803ed20b7beb7280e0a17e6e90043eb6b7726 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -66,11 +66,6 @@ stages:
 
 ###################### The Jobs ######################
 
-1.16.0-coq-8.16:
-  extends:
-    - .build
-    - .not_in_wip_branches
-
 1.17.0-coq-8.17:
   extends:
     - .build
diff --git a/README.md b/README.md
index e1c750a572af8ad63ad68a67efddba8715adeae9..3cb8e845073ddd5394b8c380bd4138fffbdf672e 100644
--- a/README.md
+++ b/README.md
@@ -1,12 +1,12 @@
 # Prosa: Formally Proven Schedulability Analysis
 
-This repository contains the main Coq specification & proof development of the [Prosa open-source project](https://prosa.mpi-sws.org), which was launched in 2016. 
+This repository contains the main Coq specification & proof development of the [Prosa open-source project](https://prosa.mpi-sws.org), which was launched in 2016.
 
-From 2018–201, Prosa was further developed in the context of the [RT-Proofs research project](https://rt-proofs.inria.fr/) (funded jointly by ANR and DFG, projects ANR-17-CE25-0016 and DFG-391919384, respectively). 
+From 2018–201, Prosa was further developed in the context of the [RT-Proofs research project](https://rt-proofs.inria.fr/) (funded jointly by ANR and DFG, projects ANR-17-CE25-0016 and DFG-391919384, respectively).
 
 <center><img alt="RT-Proofs logo" src="http://prosa.mpi-sws.org/figures/rt-proofs-logo.png" width="300px"></center>
 
-Prosa continues to be maintained and developed by the MPI-SWS Real-Time Systems group and contributors. Patches and merge requests are very welcome! 
+Prosa continues to be maintained and developed by the MPI-SWS Real-Time Systems group and contributors. Patches and merge requests are very welcome!
 
 ## Documentation
 
@@ -16,21 +16,21 @@ Up-to-date documentation for all branches of the main Prosa repository is availa
 
 ## Publications
 
-Please see the [list of publications](https://prosa.mpi-sws.org/publications.html) on the Prosa project's homepage. 
+Please see the [list of publications](https://prosa.mpi-sws.org/publications.html) on the Prosa project's homepage.
 
 ### Classic Prosa
 
-All results published prior to 2020 used the "classic" version of Prosa as first presented at ECRTS'16. Classic Prosa has been superseded by this development and is no longer being maintained. Refer to [the `classic-prosa` branch](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/tree/classic-prosa) to find this original version of Prosa. 
+All results published prior to 2020 used the "classic" version of Prosa as first presented at ECRTS'16. Classic Prosa has been superseded by this development and is no longer being maintained. Refer to [the `classic-prosa` branch](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/tree/classic-prosa) to find this original version of Prosa.
 
 
 ## Directory and Module Structure
 
 The directory and module structure is organized as follows. First, the main parts, of which there are currently six.
 
-- [`behavior`](behavior/): The `behavior` namespace collects basic definitions and properties of system behavior (i.e., it defines Prosa's **trace-based semantics**). There are *no* proofs here. This module is mandatory: *all* results in Prosa rely on the basic trace-based semantics defined in this module. 
+- [`behavior`](behavior/): The `behavior` namespace collects basic definitions and properties of system behavior (i.e., it defines Prosa's **trace-based semantics**). There are *no* proofs here. This module is mandatory: *all* results in Prosa rely on the basic trace-based semantics defined in this module.
 - [`model`](model/): The `model` namespace collects all definitions and basic properties of various **system models** (e.g., sporadic tasks, arrival curves, various scheduling policies, etc.). There are only few proofs here. This module contains multiple, mutually exclusive alternatives (e.g., periodic vs. sporadic tasks, uni- vs. multiprocessor models, constrained vs. arbitrary deadlines, etc.), and higher-level results are expected "pick and choose" whatever definitions and assumptions are appropriate. These models are *axiomatic* in the sense that they are collections of hypotheses and not necessarily backed by concrete implementations (but see below).
 - [`analysis`](analysis/): The `analysis` namespace collects all definitions and proof libraries needed to establish **system properties** (e.g., schedulability, response time, etc.). This includes a substantial library of *basic facts* that follow directly from the trace-based semantics or specific modelling assumptions. Virtually all intermediate steps and low-level proofs will be found here.
-- [`results`](results/): The `results` namespace contains all **high-level analysis results**. 
+- [`results`](results/): The `results` namespace contains all **high-level analysis results**.
 - [`implementation`](implementation/): This module collects concrete implementations of some of the axiomatic models and scheduling policies to which the results apply. These are used to instantiate  (i.e., apply) high-level results in an assumption-free environment for concrete job and task types, which establishes the absence of contradictions in the axiomatic models refined by the implementations.
 - [`implementation.refinements`](implementation/refinements/): The refinements needed by [POET](https://drops.dagstuhl.de/opus/volltexte/2022/16336/) to compute with large numbers, based on [CoqEAL](https://github.com/coq-community/CoqEAL).
 
@@ -48,6 +48,7 @@ Importing Prosa changes the behavior of ssreflect's `done` tactic by adding basi
 ```
 Ltac done := solve [ ssreflect.done | eauto 4 with basic_rt_facts ].
 ```
+Prosa overwrites the default obligation tactic of Coq with `idtac`. Refer [`util.tactics`](util/tactics.v) for details.
 
 
 ## Installation
@@ -104,7 +105,7 @@ Alternatively, `esy shell` opens a shell within its environment.
 
 #### Dependencies
 
-Besides on Coq itself, Prosa depends on 
+Besides on Coq itself, Prosa depends on
 
 1. the `ssreflect` library of the [Mathematical Components project](https://math-comp.github.io),
 2. the [Micromega support for the Mathematical Components library](https://github.com/math-comp/mczify) provided by `mczify`, and
@@ -165,13 +166,13 @@ To make things as smooth as possible, here are a couple of rules and guidelines
 
 1. Always follow the project [coding and writing guidelines](doc/guidelines.md).
 
-2. Make sure the master branch "compiles" at each commit. This is not true for the early history of the repository, and during certain stretches of heavy refactoring, but going forward we should strive to keep it working at all times. 
+2. Make sure the master branch "compiles" at each commit. This is not true for the early history of the repository, and during certain stretches of heavy refactoring, but going forward we should strive to keep it working at all times.
 
 3. It's okay (and even recommended) to develop in a (private) dirty branch, but please clean up and re-base your branch (i.e., `git-rebase -i`) on top of the current master branch before opening a merge request.
 
 4. Create merge requests liberally. No improvement is too small or too insignificant for a merge request. This applies to documentation fixes (e.g., typo fixes, grammar fixes, clarifications, etc.)  as well.
 
-5. If you are unsure whether a proposed change is even acceptable or the right way to go about things, create a work-in-progress (WIP) merge request as a basis for discussion. A WIP merge request is prefixed by "WIP:" or "Draft:". 
+5. If you are unsure whether a proposed change is even acceptable or the right way to go about things, create a work-in-progress (WIP) merge request as a basis for discussion. A WIP merge request is prefixed by "WIP:" or "Draft:".
 
 6. We strive to have only "fast-forward merges" without merge commits, so always re-base your branch to linearize the history before merging. (WIP branches do not need to be linear.)
 
@@ -179,4 +180,4 @@ To make things as smooth as possible, here are a couple of rules and guidelines
 
 8. If something seems confusing, please help with improving the documentation. :-)
 
-9. If you don't know how to fix or improve something, or if you have an open-ended suggestion in need of discussion, please file a ticket. 
+9. If you don't know how to fix or improve something, or if you have an open-ended suggestion in need of discussion, please file a ticket.
diff --git a/behavior/ready.v b/behavior/ready.v
index bc759ae88dd5dd56afb34eb19cffe6d63c694971..e4dc9e5b2ba5f1bfdcdf2a62b183af732a157578 100644
--- a/behavior/ready.v
+++ b/behavior/ready.v
@@ -79,5 +79,3 @@ Section ValidSchedule.
      properties are implied by jobs_must_be_ready_to_execute. *)
 
 End ValidSchedule.
-
-Obligation Tactic := try done.
diff --git a/behavior/schedule.v b/behavior/schedule.v
index 9cb5b819ede1eccdf60ea82471bf2f9f5a812f43..4f166384556aa9b2e48b17c35d7d3db54fe3742b 100644
--- a/behavior/schedule.v
+++ b/behavior/schedule.v
@@ -104,5 +104,3 @@ Definition schedule {Job : JobType} (PState : ProcessorState Job) :=
     [scheduled_on] and [service_on] are defined. Instead,
     proofs must rely on basic lemmas about processor state classes. *)
 Global Opaque scheduled_on service_on.
-
-Obligation Tactic := try done.
diff --git a/model/processor/multiprocessor.v b/model/processor/multiprocessor.v
index a0faaa1ccd61d0c024f7542f8b88b85462dacae4..995e7c6a59db166210c0545afcf71ed372181430 100644
--- a/model/processor/multiprocessor.v
+++ b/model/processor/multiprocessor.v
@@ -52,7 +52,7 @@ Section Schedule.
       [mps] on a given core [cpu] is exactly the supply provided by the
       core-local state [(mps cpu)]. *)
   Definition multiproc_supply_on
-      (mps : multiprocessor_state) (cpu : processor num_cpus)
+    (mps : multiprocessor_state) (cpu : processor num_cpus)
     := supply_in (mps cpu).
 
   (** Next, the service received by a given job [j] in a given
@@ -60,7 +60,7 @@ Section Schedule.
       exactly the service given by [j] in the processor-local state
       [(mps cpu)]. *)
   Definition multiproc_service_on
-      (j : Job) (mps : multiprocessor_state) (cpu : processor num_cpus)
+    (j : Job) (mps : multiprocessor_state) (cpu : processor num_cpus)
     := service_in j (mps cpu).
 
   (** Finally, we connect the above definitions with the generic Prosa
@@ -82,7 +82,7 @@ Section Schedule.
       [mps] is given by the sum of the service received across all individual
       processors of the multiprocessor. *)
   Lemma multiproc_service_in_eq : forall (j : Job) (mps : multiprocessor_state),
-    service_in j mps = \sum_(cpu < num_cpus) service_in j (mps cpu).
+      service_in j mps = \sum_(cpu < num_cpus) service_in j (mps cpu).
   Proof. reflexivity. Qed.
 
 End Schedule.
diff --git a/model/processor/spin.v b/model/processor/spin.v
index 9cce1357f93f9095ac21ca6a3a68a20df67cc969..083351ba7ab5d066f79229f0fb58e7744dd8e946 100644
--- a/model/processor/spin.v
+++ b/model/processor/spin.v
@@ -57,7 +57,7 @@ Section State.
       end.
 
   End Service.
-
+  
   (** Finally, we connect the above definitions with the generic Prosa
       interface for abstract processor states. *)
   Program Definition pstate_instance : ProcessorState Job :=
@@ -68,6 +68,6 @@ Section State.
       service_on   := spin_service_on
     |}.
   Next Obligation. by move => j [] // s [] /=; case: eqP. Qed.
-  Next Obligation. by move=> j [] //= j' _ /negbTE ->. Qed.
+  Next Obligation. by move => j [] // s [] /=; case: eqP. Qed.
 
 End State.
diff --git a/model/processor/varspeed.v b/model/processor/varspeed.v
index 87393a987985db74f6a58275e0c373d2a743bf6a..098e7f4ca240473203922f554739633a4a479bba 100644
--- a/model/processor/varspeed.v
+++ b/model/processor/varspeed.v
@@ -64,7 +64,7 @@ Section State.
       supply_on    := varspeed_supply_on;
       service_on   := varspeed_service_on
     |}.
-  Next Obligation. by move=> j [] //= s n; case: eqP. Qed.
+  Next Obligation. by move=> j [] //= s ; case: eqP. Qed.
   Next Obligation. by move=> j [] //= j' v _; case: ifP. Qed.
 
 End State.
diff --git a/model/readiness/basic.v b/model/readiness/basic.v
index 7595ca7b80b570bedd44440343502550d78061fe..032bb14f978d89bfb66687a5aca1e3ae38aed048 100644
--- a/model/readiness/basic.v
+++ b/model/readiness/basic.v
@@ -21,5 +21,6 @@ Section LiuAndLaylandReadiness.
   {
     job_ready sched j t := pending sched j t
   }.
+  Next Obligation. by done. Qed.
 
 End LiuAndLaylandReadiness.
diff --git a/results/elf/rta/bounded_pi.v b/results/elf/rta/bounded_pi.v
index c72931a4764b0bfd2e4357e73babeca3e3da868f..c510de7112d47d7726a7faf2c097da300f67c2dc 100644
--- a/results/elf/rta/bounded_pi.v
+++ b/results/elf/rta/bounded_pi.v
@@ -286,8 +286,8 @@ Section AbstractRTAforELFwithArrivalCurves.
         move=> /andP[HEPj EP]; rewrite -TSK'; apply/andP; split =>//.
         move: HEPj.
         have -> : hep_job j0 j = (@hep_job _ (GEL Job Task) j0 j) by apply: hep_job_elf_gel.
-        rewrite /is_ep_causing_intf ler_subr_addl addrAC ler_subr_addl addr0 -TSK'.
-        apply: le_trans; rewrite ler_add2r ler_nat.
+        rewrite /is_ep_causing_intf lerBrDl addrAC lerBrDl addr0 -TSK'.
+        apply: le_trans; rewrite lerD2r ler_nat.
         apply: job_arrival_between_ge=>//. }}
     { exists t1, t2; split=> [//|]; split=> [//|].
       eapply instantiated_busy_interval_equivalent_busy_interval => //. }
diff --git a/util/tactics.v b/util/tactics.v
index 17afea968c04392774fc9db9f00b5b8b7b342ea6..92f48f02e2890e1b511a76339b28efb2212ac41a 100644
--- a/util/tactics.v
+++ b/util/tactics.v
@@ -104,6 +104,13 @@ Ltac rt_eauto := eauto 4 with basic_rt_facts.
 Ltac done := solve [ ssreflect.done | eauto 4 with basic_rt_facts ].
 #[export] Hint Resolve I : basic_rt_facts.  (* ensure the database exists *)
 
+(** Note: [idtac] is a no-op. However, it suppresses the default obligation tactic,
+    which uses [intros] to introduce unnamed variables. This is a Coq technicality
+    that a casual reader may safely ignore. It is necessary to avoid triggering one
+    of Prosa's continuous integration checks that validates that no proof scripts
+    depend on automatically generated names.  *)
+#[global] Obligation Tactic := idtac.
+
 (* ************************************************************************** *)
 (** * Handier movement of inequalities. *)
 (* ************************************************************************** *)