(no commit message)

diff --git a/Documentation/notes_on_formal_proofs.mdwn b/Documentation/notes_on_formal_proofs.mdwn
index 01966058c10e1cfd19280bd910a8fce900b2bb85..1186868c8b49d6bb73f9c851709f6f9ea9a7a075 100644 (file)
--- a/Documentation/notes_on_formal_proofs.mdwn
+++ b/Documentation/notes_on_formal_proofs.mdwn
@@ -67,14 +67,15 @@ so I won't spend any more time on this.
 `CompALUOpSubset` is, ultimately, an `nmigen`
 [record](https://github.com/nmigen/nmigen/blob/master/nmigen/hdl/rec.py#L89)
 which contains a number of fields related to telling the pipeline stage
-*what to do*.  (Hence the *Op* in the class name.)  I won't disclose
+*what to do* and providing all the information it needs in order *to*
+"do".  (Hence the *Op* in the class name.)  I won't disclose
 the fields here, because they're liable to change at any time.  What is
 important to know here is that this record exists for one purpose: to
 ensure that when the interface to the ALU pipeline stage changes for
 any reason, *all* consumers of that interface are updated consistently.
 
 Because this is a record, its fields may be introspected.  This happens
-frequently; it is usually the case that an Op-type record is passed
+frequently: it is the case that an Op-type record is passed
 unchanged from stage to stage.  However, `nmigen` does not seem to support
 testing records for equality in formal assertions.  (lkcl: it does) To
 express this constraint without needing to update a pile of use-sites