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