diff --git a/formal/Drift.v b/formal/Drift.v
index d9730be..6d7ce59 100644
--- a/formal/Drift.v
+++ b/formal/Drift.v
@@ -32,9 +32,6 @@ Require Import Coq.Init.Logic.
    split a longer axiom type across lines and silently escape the check. *)
 Set Printing Width 400.
 
-(* Keep Print Assumptions output on one line per axiom: the CI and Justfile
-   guards match /^name :/ with awk, and Coq's default ~78-column wrap would
-   split a longer axiom type across lines and silently escape the check. *)
 
 (** ** Domain *)
 
diff --git a/formal/Normalizer.v b/formal/Normalizer.v
index b86c7d6..0d7dadd 100644
--- a/formal/Normalizer.v
+++ b/formal/Normalizer.v
@@ -52,9 +52,6 @@ Require Import Coq.Bool.Bool.
    split a longer axiom type across lines and silently escape the check. *)
 Set Printing Width 400.
 
-(* Keep Print Assumptions output on one line per axiom: the CI and Justfile
-   guards match /^name :/ with awk, and Coq's default ~78-column wrap would
-   split a longer axiom type across lines and silently escape the check. *)
 
 (** ** Domain *)
 
diff --git a/formal/Octad.v b/formal/Octad.v
index cf4154f..f3f13e3 100644
--- a/formal/Octad.v
+++ b/formal/Octad.v
@@ -95,9 +95,6 @@ Require Import Coq.Logic.FunctionalExtensionality.
    split a longer axiom type across lines and silently escape the check. *)
 Set Printing Width 400.
 
-(* Keep Print Assumptions output on one line per axiom: the CI and Justfile
-   guards match /^name :/ with awk, and Coq's default ~78-column wrap would
-   split a longer axiom type across lines and silently escape the check. *)
 Import ListNotations.
 
 (** ** [def:modset] — Modality Set
diff --git a/formal/Planner.v b/formal/Planner.v
index 093eb6a..56e9072 100644
--- a/formal/Planner.v
+++ b/formal/Planner.v
@@ -38,9 +38,6 @@ Require Import Coq.Sorting.Permutation.
    split a longer axiom type across lines and silently escape the check. *)
 Set Printing Width 400.
 
-(* Keep Print Assumptions output on one line per axiom: the CI and Justfile
-   guards match /^name :/ with awk, and Coq's default ~78-column wrap would
-   split a longer axiom type across lines and silently escape the check. *)
 Import ListNotations.
 
 (** ** Domain *)
diff --git a/formal/PlannerSemantic.v b/formal/PlannerSemantic.v
index 81cf126..95fe4b9 100644
--- a/formal/PlannerSemantic.v
+++ b/formal/PlannerSemantic.v
@@ -56,9 +56,6 @@ Require Import Coq.Sorting.Permutation.
    split a longer axiom type across lines and silently escape the check. *)
 Set Printing Width 400.
 
-(* Keep Print Assumptions output on one line per axiom: the CI and Justfile
-   guards match /^name :/ with awk, and Coq's default ~78-column wrap would
-   split a longer axiom type across lines and silently escape the check. *)
 Import ListNotations.
 
 (** ** Domain (reusing Planner.v abstractions) *)
diff --git a/formal/Provenance.v b/formal/Provenance.v
index 8caaefd..7bb1bfb 100644
--- a/formal/Provenance.v
+++ b/formal/Provenance.v
@@ -41,9 +41,6 @@ Require Import Coq.Lists.List.
    split a longer axiom type across lines and silently escape the check. *)
 Set Printing Width 400.
 
-(* Keep Print Assumptions output on one line per axiom: the CI and Justfile
-   guards match /^name :/ with awk, and Coq's default ~78-column wrap would
-   split a longer axiom type across lines and silently escape the check. *)
 Import ListNotations.
 
 (** ** Domain *)
diff --git a/formal/Transaction.v b/formal/Transaction.v
index b100dc6..1753771 100644
--- a/formal/Transaction.v
+++ b/formal/Transaction.v
@@ -43,9 +43,6 @@ Require Import Coq.Init.Logic.
    split a longer axiom type across lines and silently escape the check. *)
 Set Printing Width 400.
 
-(* Keep Print Assumptions output on one line per axiom: the CI and Justfile
-   guards match /^name :/ with awk, and Coq's default ~78-column wrap would
-   split a longer axiom type across lines and silently escape the check. *)
 
 (** ** Domain *)
 
diff --git a/formal/VCL.v b/formal/VCL.v
index 4530de9..86db14b 100644
--- a/formal/VCL.v
+++ b/formal/VCL.v
@@ -48,9 +48,6 @@ Require Import Coq.Init.Logic.
    split a longer axiom type across lines and silently escape the check. *)
 Set Printing Width 400.
 
-(* Keep Print Assumptions output on one line per axiom: the CI and Justfile
-   guards match /^name :/ with awk, and Coq's default ~78-column wrap would
-   split a longer axiom type across lines and silently escape the check. *)
 
 (** ** Syntax *)
 
diff --git a/formal/WAL.v b/formal/WAL.v
index 4df1c67..ec7b890 100644
--- a/formal/WAL.v
+++ b/formal/WAL.v
@@ -51,9 +51,6 @@ Require Import Coq.Logic.FunctionalExtensionality.
    split a longer axiom type across lines and silently escape the check. *)
 Set Printing Width 400.
 
-(* Keep Print Assumptions output on one line per axiom: the CI and Justfile
-   guards match /^name :/ with awk, and Coq's default ~78-column wrap would
-   split a longer axiom type across lines and silently escape the check. *)
 Import ListNotations.
 
 (** ** Domain *)