diff options
| author | Pierre-Marie Pédrot | 2018-10-11 18:13:12 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-15 22:54:37 +0200 |
| commit | 6b5b4db599333546334bcdbd852be72ddb39d9dc (patch) | |
| tree | 5aff3505ee428bff94035d8484d5d1672ac3a78d /dev/doc | |
| parent | da4c6c4022625b113b7df4a61c93ec351a6d194b (diff) | |
Deprecating the RAW_TYPED and GLOB_TYPED stanzas of the ARGUMENT EXTEND macro.
Those optional arguments did not really make sense. It was pretty clear from
our code base, as all instances where triplicating the same type for TYPED,
RAW_TYPED and GLOB_TYPED.
Diffstat (limited to 'dev/doc')
| -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 |