aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorMaxime Dénès2017-04-03 15:21:16 +0200
committerMaxime Dénès2017-04-03 15:22:40 +0200
commit9da03d38249a2716e7ede5d20948759e6d975138 (patch)
treed6666937b32e3b65e71caaf4511f164e7818ef04 /dev
parent3fe764dd8d6578adddb01b02bafc7f31d9cb776c (diff)
parenteec5145a5c6575d04b5ab442597fb52913daed29 (diff)
Merge PR#417: No cast surgery in let in
Diffstat (limited to 'dev')
-rw-r--r--dev/doc/changes.txt11
1 files changed, 11 insertions, 0 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 03742fb8ad..af077bbb40 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -33,6 +33,17 @@ The following type aliases where removed
The module Constrarg was merged into Stdarg.
+The following types have been moved and modified:
+
+ local_binder -> local_binder_expr
+ glob_binder merged with glob_decl
+
+The following constructors have been renamed:
+
+ LocalRawDef -> CLocalDef
+ LocalRawAssum -> CLocalAssum
+ LocalPattern -> CLocalPattern
+
** Ltac API **
Many Ltac specific API has been moved in its own ltac/ folder. Amongst other