CHANGES: markdown 1, dholland 0 (fix formatting)

Whitespace only.

CHANGES.md

@@ -12,52 +12,52 @@
 ## Bug fixes
 
 * Unexpected special-case type behavior of monad binds in the
-syntactic top level has been removed.
-(This was _not_ specifically associated with the TopLevel monad, so
-top-level binds and binds in functions in TopLevel, or in nested
-do-blocks, would behave differently.)
-See issue #2162.
-
-There are three primary visible consequences.
-The first is that the REPL no longer accepts
-non-monadic expressions.
-These can still be evaluated and printed; just prefix them with
-```return```.
-(Affordances specifically for the REPL so this is not required there
-may be restored in the future.)
-
-The second is that statements of the form ```x <- e;``` where ```e```
-is a pure (non-monadic) term used to be (improperly) accepted at the
-top level of scripts.
-These statements now generate a warning.
-This will become an error in a future release and such statements
-should be rewritten as ```let x = e;```.
-For example, ```t <- unfold_term ["reverse"] {{ reverse 0b01 }};```
-should be changed to ```let t = unfold_term ["reverse"] {{ reverse 0b01 }};```.
-
-The third is that statements of the form ```x <- s;``` or just ```s;```
-where ```s``` is a term in the _wrong_ monad also used to be
-improperly accepted at the top level of scripts.
-These statements silently did nothing.
-They will now generate a warning.
-This will become an error in a future release.
-Such statements should be removed or rewritten.
-For example, it used to be possible to write ```llvm_assert {{ False }};```
-at the top level (outside any specification) and it would be ignored.
-```llvm_assert``` is only meaningful within an LLVM specification.
+  syntactic top level has been removed.
+  (This was _not_ specifically associated with the TopLevel monad, so
+  top-level binds and binds in functions in TopLevel, or in nested
+  do-blocks, would behave differently.)
+  See issue #2162.
+
+  There are three primary visible consequences.
+  The first is that the REPL no longer accepts
+  non-monadic expressions.
+  These can still be evaluated and printed; just prefix them with
+  ```return```.
+  (Affordances specifically for the REPL so this is not required there
+  may be restored in the future.)
+
+  The second is that statements of the form ```x <- e;``` where ```e```
+  is a pure (non-monadic) term used to be (improperly) accepted at the
+  top level of scripts.
+  These statements now generate a warning.
+  This will become an error in a future release and such statements
+  should be rewritten as ```let x = e;```.
+  For example, ```t <- unfold_term ["reverse"] {{ reverse 0b01 }};```
+  should be changed to ```let t = unfold_term ["reverse"] {{ reverse 0b01 }};```.
+
+  The third is that statements of the form ```x <- s;``` or just ```s;```
+  where ```s``` is a term in the _wrong_ monad also used to be
+  improperly accepted at the top level of scripts.
+  These statements silently did nothing.
+  They will now generate a warning.
+  This will become an error in a future release.
+  Such statements should be removed or rewritten.
+  For example, it used to be possible to write ```llvm_assert {{ False }};```
+  at the top level (outside any specification) and it would be ignored.
+  ```llvm_assert``` is only meaningful within an LLVM specification.
 
 * A number of SAWScript type checking problems have been fixed,
-including issue #2077.
-Some previously accepted scripts and specs may be rejected and need
-(generally minor) adjustment.
-Prior to these changes the typechecker allowed unbound type variables
-in a number of places (such as on the right-hand side of typedefs, and
-in function signatures), so for example type names contaning typos
-would not necessarily have been caught and will now fail.
-```typedef t = nonexistent``` was previously accepted and now is not.
-These problems could trigger panics, but there does not appear to have
-been any way to produce unsoundness in the sense of false
-verifications.
+  including issue #2077.
+  Some previously accepted scripts and specs may be rejected and need
+  (generally minor) adjustment.
+  Prior to these changes the typechecker allowed unbound type variables
+  in a number of places (such as on the right-hand side of typedefs, and
+  in function signatures), so for example type names contaning typos
+  would not necessarily have been caught and will now fail.
+  ```typedef t = nonexistent``` was previously accepted and now is not.
+  These problems could trigger panics, but there does not appear to have
+  been any way to produce unsoundness in the sense of false
+  verifications.
 
 * Counterexamples including SMT arrays are now printed with the array
   contents instead of placeholder text.