aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/doc
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-06-29 14:30:33 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-06-29 14:30:33 +0200
commit2ca003899ea4a24a470c32dc186b95ef3de3ca19 (patch)
treee7444295b47223d16db6db5beafde4839a0cf926 /dev/doc
parentacbc42ad1da48be53456c0d41ec2e60ae2d6e642 (diff)
parent21ed95122a088cab6808200778719270d9cc9078 (diff)
Merge PR #7080: Swapping Context and Constr and defining declarations on constr in Constr
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