diff options
Diffstat (limited to 'dev/doc/changes.txt')
| -rw-r--r-- | dev/doc/changes.txt | 15 |
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 ** |