diff options
| author | BESSON Frederic | 2021-01-21 10:45:16 +0100 |
|---|---|---|
| committer | BESSON Frederic | 2021-01-21 10:45:16 +0100 |
| commit | 2f79b58cdbdeb3ff3446168ede042e063a6f6c99 (patch) | |
| tree | c0ad1f57842259fd41a09fdc805b204fdabc4ebf /doc/changelog | |
| parent | dfc6a979bf212067ea1936a569d1d46a19669ec9 (diff) | |
| parent | 43a65423b61b958ae1aa099395797be094dd2c6b (diff) | |
Merge PR #13764: Remove Add InjTyp and 10 other micromega commands (deprecated in 8.13)
Reviewed-by: Zimmi48
Reviewed-by: fajb
Diffstat (limited to 'doc/changelog')
| -rw-r--r-- | doc/changelog/07-vernac-commands-and-options/13764-remove_add_injtyp.rst | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/doc/changelog/07-vernac-commands-and-options/13764-remove_add_injtyp.rst b/doc/changelog/07-vernac-commands-and-options/13764-remove_add_injtyp.rst new file mode 100644 index 0000000000..fc6c88eab6 --- /dev/null +++ b/doc/changelog/07-vernac-commands-and-options/13764-remove_add_injtyp.rst @@ -0,0 +1,6 @@ +- **Removed:** + `Show Zify Spec`, `Add InjTyp` and 11 similar `Add *` commands. + For `Show Zify Spec`, use `Show Zify UnOpSpec` or `Show Zify BinOpSpec` instead. + For `Add *`, `Use Add Zify *` intead of `Add *` + (`#13764 <https://github.com/coq/coq/pull/13764>`_, + by Jim Fehrle). |