aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-02-02 21:30:43 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-03-24 12:22:21 +0100
commitb496309c7d4707a4377c72b0543faa025d993589 (patch)
tree030d4a77d069e95e5730c1625a040c6bfc78b7e4
parentf9a4ca41bc1313300f5f9b9092fe24825f435706 (diff)
Documenting main changes of API.
-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 03742fb8a..af077bbb4 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