diff options
| author | Pierre-Marie Pédrot | 2020-10-04 16:16:53 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-11-04 13:43:57 +0100 |
| commit | f4c1b8b9ffdb5e531685130824fc4ce03a3e9794 (patch) | |
| tree | b68dcc1bd537c1108d2aa92642bca3b2725c9333 /engine | |
| parent | be332604f4d495ea875185ff1b5aee1eb12b4178 (diff) | |
Do not try to be clever for term-as-hint interpretation.
The prepare_hint function was trying to requantify over all undefined evars,
but actually this should not happen when defining generic terms as hints through
some Hint vernacular command.
Diffstat (limited to 'engine')
0 files changed, 0 insertions, 0 deletions