diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-15 19:38:34 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-15 19:41:09 +0200 |
| commit | 7bd00a63015c4017d8209a4d495b9683d33d1d53 (patch) | |
| tree | 5cd41ad079b5941b06c417c55f2ce78d5d2bf3b3 /dev | |
| parent | 108fbe13e3c07c283e2cb972ac96679632bcd84a (diff) | |
Documenting API changes.
Diffstat (limited to 'dev')
| -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 ** |