diff options
Diffstat (limited to 'lib/rites/rite_ef/precedence_ef.mli')
| -rw-r--r-- | lib/rites/rite_ef/precedence_ef.mli | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/lib/rites/rite_ef/precedence_ef.mli b/lib/rites/rite_ef/precedence_ef.mli index 7d0bc98..6a96c4e 100644 --- a/lib/rites/rite_ef/precedence_ef.mli +++ b/lib/rites/rite_ef/precedence_ef.mli @@ -80,8 +80,11 @@ val entry_14_fixed_band : int was built to beat. {!band}'s own entries now use the real RG 91 number TIMES TEN throughout, reserving genuine headroom before every entry -- see precedence_ef.ml's own comment for the full citation, the counter- - example that found this, and why entries 12 and 20 may need the same - treatment if their own "movable then fixed" halves ever get a witness. *) + example that found this, and why entries 13, 20, 23 and 24 may need the + same treatment if their own "movable then fixed" halves ever get a + witness. (Corrected: this previously said "entries 12 and 20". RG 91 + puts that clause at entry 13, not 12, and the split occurs at five rows + in all -- 13, 14, 20, 23's third sub-item and 24.) *) val entry_14_movable_band : int (** [band ctx c]: RG 91's Table of Precedence. Returns the table's own entry |