aboutsummaryrefslogtreecommitdiff
path: root/dev/doc
diff options
context:
space:
mode:
Diffstat (limited to 'dev/doc')
-rw-r--r--dev/doc/changes.txt5
1 files changed, 5 insertions, 0 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 5933649daf..f87e76dd1a 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -6,6 +6,11 @@ We renamed the following functions:
Context.Rel.Declaration.fold -> Context.Rel.Declaration.fold_constr
Context.Named.Declaration.fold -> Context.Named.Declaration.fold_constr
+ Printer.pr_var_list_decl -> Printer.pr_compacted_decl
+
+We renamed the following modules:
+
+ Context.ListNamed -> Context.Compacted
The following type aliases where removed