diff options
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/changes.txt | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index f54f3fcc8e..12c3ec4546 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -39,6 +39,26 @@ 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 +depending on any module defined in the ltac/ directory. Namely, even if +everything looks OK at compile time, a plugin can fail to load at link time +because it mistakenly looks for a module Foo instead of Ltac_plugin.Foo, with +an error of the form: + +Error: while loading myplugin.cmxs, no implementation available for Foo. + +In particular, most EXTEND macros will trigger this problem even if they +seemingly do not use any Ltac module, as their expansion do. + +The solution is simple, and consists in adding a statement "open Ltac_plugin" +in each file using a Ltac module, before such a module is actually called. An +alternative solution would be to fully qualify Ltac modules, e.g. turning any +call to Tacinterp into Ltac_plugin.Tacinterp. Note that this solution does not +work for EXTEND macros though. ** Error handling ** |