diff options
| author | Pierre-Marie Pédrot | 2018-06-12 17:02:34 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-02-28 10:27:59 +0100 |
| commit | 8cdaa1b5c485ed351f9b3bf212ec5d88f8561908 (patch) | |
| tree | 7377c112460a11b4432f7bf0f9ac75a772be688b /doc | |
| parent | aeca986089d005054496ed4bcf1b920e8fa02173 (diff) | |
Deprecating the declaration of arbitrary terms as hints.
We restrict hints to be global references, so as to further simplify the
implementation. Allowing arbitrary terms makes it difficult or expensive
to handle properly some actions like universe contexts or hint equality.
Ultimately, the IsConstr constructor for hints should also be removed.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/07-commands-and-options/7791-deprecate-hint-constr.rst | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/doc/changelog/07-commands-and-options/7791-deprecate-hint-constr.rst b/doc/changelog/07-commands-and-options/7791-deprecate-hint-constr.rst new file mode 100644 index 0000000000..d2af6a4ca7 --- /dev/null +++ b/doc/changelog/07-commands-and-options/7791-deprecate-hint-constr.rst @@ -0,0 +1,5 @@ +- **Deprecated:** + Deprecated the declaration of arbitrary terms as hints. Global + references are now mandatory. + (`#7791 <https://github.com/coq/coq/pull/7791>`_, + by Pierre-Marie Pédrot). |