diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/doc/changes.txt | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 8ea1638c99..7db5647c30 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -93,6 +93,12 @@ 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. +** Additional changes in tactic extensions ** + +Entry "constr_with_bindings" has been renamed into +"open_constr_with_bindings". New entry "constr_with_bindings" now +uses type classes and rejects terms with unresolved holes. + ** Error handling ** - All error functions now take an optional parameter `?loc:Loc.t`. For |