diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/doc/changes.md | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md index f30b4107b6..c5632411d1 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -27,6 +27,11 @@ Coqlib: command then enables to locate the registered constant through its name. The name resolution is dynamic. +Macros: + +- The RAW_TYPED AS and GLOB_TYPED AS stanzas of the ARGUMENT EXTEND macro are + deprecated. Use TYPED AS instead. + ## Changes between Coq 8.8 and Coq 8.9 ### ML API |