aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/doc
diff options
context:
space:
mode:
Diffstat (limited to 'dev/doc')
-rw-r--r--dev/doc/changes.md10
1 files changed, 10 insertions, 0 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index f3fc126f9..cbb95625f 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -53,6 +53,16 @@ Printer.ml API
pr_subgoal and pr_goal was removed to simplify the code. It was
earlierly used by PCoq.
+Kernel
+
+ The following renamings happened:
+ - `Context.Rel.t` into `Constr.rel_context`
+ - `Context.Named.t` into `Constr.named_context`
+ - `Context.Compacted.t` into `Constr.compacted_context`
+ - `Context.Rel.Declaration.t` into `Constr.rel_declaration`
+ - `Context.Named.Declaration.t` into `Constr.named_declaration`
+ - `Context.Compacted.Declaration.t` into `Constr.compacted_declaration`
+
Source code organization
- We have eliminated / fused some redundant modules and relocated a