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 | |
| 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')
| -rw-r--r-- | doc/changelog/07-vernac-commands-and-options/13764-remove_add_injtyp.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 62 |
2 files changed, 6 insertions, 62 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). diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index 38c4886e0f..3bd85d29c8 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -315,68 +315,6 @@ obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid. prints the list of types that supported by :tacn:`zify` i.e., :g:`Z`, :g:`nat`, :g:`positive` and :g:`N`. -.. cmd:: Show Zify Spec - - .. deprecated:: 8.13 - Use :cmd:`Show Zify` ``UnOpSpec`` or :cmd:`Show Zify` ``BinOpSpec`` instead. - -.. cmd:: Add InjTyp @one_term - - .. deprecated:: 8.13 - Use :cmd:`Add Zify` ``InjTyp`` instead. - -.. cmd:: Add BinOp @one_term - - .. deprecated:: 8.13 - Use :cmd:`Add Zify` ``BinOp`` instead. - -.. cmd:: Add BinOpSpec @one_term - - .. deprecated:: 8.13 - Use :cmd:`Add Zify` ``BinOpSpec`` instead. - -.. cmd:: Add UnOp @one_term - - .. deprecated:: 8.13 - Use :cmd:`Add Zify` ``UnOp`` instead. - -.. cmd:: Add UnOpSpec @one_term - - .. deprecated:: 8.13 - Use :cmd:`Add Zify` ``UnOpSpec`` instead. - -.. cmd:: Add CstOp @one_term - - .. deprecated:: 8.13 - Use :cmd:`Add Zify` ``CstOp`` instead. - -.. cmd:: Add BinRel @one_term - - .. deprecated:: 8.13 - Use :cmd:`Add Zify` ``BinRel`` instead. - -.. cmd:: Add PropOp @one_term - - .. deprecated:: 8.13 - Use :cmd:`Add Zify` ``PropOp`` instead. - -.. cmd:: Add PropBinOp @one_term - - .. deprecated:: 8.13 - Use :cmd:`Add Zify` ``PropBinOp`` instead. - -.. cmd:: Add PropUOp @one_term - - .. deprecated:: 8.13 - Use :cmd:`Add Zify` ``PropUOp`` instead. - -.. cmd:: Add Saturate @one_term - - .. deprecated:: 8.13 - Use :cmd:`Add Zify` ``Saturate`` instead. - - - .. [#csdp] Sources and binaries can be found at https://projects.coin-or.org/Csdp .. [#fnpsatz] Variants deal with equalities and strict inequalities. |