aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/doc
diff options
context:
space:
mode:
authorGravatar Matej Kosik <matej.kosik@inria.fr>2016-10-20 14:18:01 +0200
committerGravatar Matej Kosik <matej.kosik@inria.fr>2016-10-20 14:18:01 +0200
commit12c78d4e45ccc9b923cd300f981ef205fee1c650 (patch)
tree087369f981446051c40326b5c73ede19b841bc7d /dev/doc
parentf514eb9a44e1c3f7098e79e745c24976e226647d (diff)
COMMENTS: dev/doc/changes.txt
Diffstat (limited to 'dev/doc')
-rw-r--r--dev/doc/changes.txt3
1 files changed, 2 insertions, 1 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index c00167b62..1403b94ac 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -14,7 +14,8 @@ We renamed the following functions:
We removed the following functions:
- Termops.Termops.compact_named_context_reverse
+ Termops.compact_named_context_reverse ... practical substitute is Termops.compact_named_context
+ Namegen.to_avoid ... equivalent substitute is Names.Id.List.mem
We renamed the following modules: