aboutsummaryrefslogtreecommitdiff
path: root/expansion.md
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-06-01 23:59:55 -0400
committerGravatar Jason Gross <jgross@mit.edu>2017-06-02 00:00:09 -0400
commitd3135a69f653034f07b7657486f926a7a20ef3ee (patch)
treee163e017643c1bc8c877ecefaa43299c458d232e /expansion.md
parent3f11f57487ce9e913b36271cee2f8b6b695945cf (diff)
Strip trailing whitespace
With ```bash bash ./etc/coq-scripts/formatting/strip-trailing-whitespace.sh ```
Diffstat (limited to 'expansion.md')
-rw-r--r--expansion.md2
1 files changed, 1 insertions, 1 deletions
diff --git a/expansion.md b/expansion.md
index 15e3b7e3d..ca74dfcdc 100644
--- a/expansion.md
+++ b/expansion.md
@@ -70,7 +70,7 @@ involve register allocation and instruction scheduling.
**loops** for our PHOAS language. Possibly hardcoded to [fold_left] of [seq], or
something else that is sufficient to encode C "for" loops. Importantly, we
-should have a way to reify existing code
+should have a way to reify existing code
**modules** for our PHOAS language so we don't have to inline everything.
Basically we want to allow one Coq-level object to represent a collection of