aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorYishuai Li2018-07-30 13:32:07 -0400
committerYishuai Li2018-07-30 13:32:27 -0400
commit8c14ee1bc5e3daf2c836badf1aadef3ecb87c99c (patch)
treecd4512c377b24989a09451a5399a18e0bd5da90c
parentcc6526b17ca6ee8cd48e83428282421a004c1763 (diff)
CHANGES: unify format
-rw-r--r--CHANGES2
1 files changed, 1 insertions, 1 deletions
diff --git a/CHANGES b/CHANGES
index b0b445b2e8..f0327e74dc 100644
--- a/CHANGES
+++ b/CHANGES
@@ -141,7 +141,7 @@ Display diffs between proof steps
Notations
-- Added [++] infix for [VectorDef.append].
+- Added `++` infix for `VectorDef.append`.
Note that this might cause incompatibilities if you have, e.g., list_scope
and vector_scope both open with vector_scope on top, and expect `++` to
refer to `app`.