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 /plugins | |
| 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 'plugins')
0 files changed, 0 insertions, 0 deletions