diff options
| -rw-r--r-- | CHANGES | 4 |
1 files changed, 4 insertions, 0 deletions
@@ -142,6 +142,10 @@ Display diffs between proof steps Notations - 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`. + Solution: wrap `_ ++ _` in `(_ ++ _)%list` (or whichever scope you want). Changes from 8.8.0 to 8.8.1 =========================== |