diff options
Diffstat (limited to 'dev/doc/changes.txt')
| -rw-r--r-- | dev/doc/changes.txt | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 8d2d05590..12c3ec454 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -39,6 +39,8 @@ important things: instead - Some printing functions were moved from Pptactic to Pputils - A part of Tacexpr has been moved to Tactypes +- The TacFun tactic expression constructor now takes a `Name.t list` for the + variable list rather than an `Id.t option list`. The folder itself has been turned into a plugin. This does not change much, but because it is a packed plugin, it may wreak havoc for third-party plugins |