docs(formal): remove the duplicated Set Printing Width comment (9 modules) (#205)

docs(formal): remove the duplicated Set Printing Width comment (9
modules)

#202 landed the same three-line explanatory comment twice in every
module —
once above `Set Printing Width 400.` where it belongs, and once orphaned
immediately below it. My fault: I ran the insertion, then deleted only
the
`Set Printing Width 400.` line to A/B-test whether the ~78-column wrap
was
actually hiding any axiom from the guard, then re-ran the insertion. The
sed
that undid the test matched only the directive, not its comment, so the
second
pass stacked a fresh copy on top of the leftover.

Comment-only; no directive, no proof and no guard changes.
`formal/Justfile`
is untouched.

To be accurate about scope, since the obvious worry is that a text edit
near
the imports clipped something: it did not. `Import ListNotations.` and
every
`Require Import` are intact in all nine modules — verified before and
after.
(A *different* cleanup attempt of mine did briefly eat that import by
skipping
a fixed three lines past the marker, which in `Planner.v` overran the
comment.
That version was reset and never committed; it is mentioned only so the
next
person knows the offset-based approach is the wrong tool here. This
commit
removes the second matched block specifically, keyed on occurrence
count.)

Verified: real coqc 8.20.1 -> `check-assumptions` exits 0, 9/9 OK; stub
coqc
-> exit 127, so the gate from #202 still fails when it should;
`Normalizer.out`
still prints at 157 columns, so the wrap fix is unaffected; `reuse lint`
compliant.

Author: hyperpolymath

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 *)
 

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 *)
 

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

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 *)

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) *)

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 *)

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 *)
 

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 *)
 

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 *)