aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rw-r--r--dev/doc/changes.txt15
1 files changed, 14 insertions, 1 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index fb1e805c1..00078c69f 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -2,6 +2,8 @@
= CHANGES BETWEEN COQ V8.6 AND COQ V8.7 =
=========================================
+* ML API *
+
We renamed the following functions:
Context.Rel.Declaration.fold -> Context.Rel.Declaration.fold_constr
@@ -21,7 +23,18 @@ The following type aliases where removed
Context.section_context ... it was just an alias for "Context.Named.t" which is still available
-* ML API *
+** Ltac API **
+
+Many Ltac specific API has been moved in its own ltac/ folder. Amongst other
+important things:
+
+- Pcoq.Tactic -> Pltac
+- Constrarg.wit_tactic -> Tacarg.wit_tactic
+- Constrarg.wit_ltac -> Tacarg.wit_ltac
+- API below ltac/ that accepted a *_tactic_expr now accept a *_generic_argument
+ instead
+- Some printing functions were moved from Pptactic to Pputils
+- A part of Tacexpr has been moved to Tactypes
** Error handling **