diff options
| author | Pierre-Marie Pédrot | 2020-02-03 10:29:14 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-02-28 10:27:59 +0100 |
| commit | 3034319a2f52baeca172a33eb98b20b3e559201f (patch) | |
| tree | 29666c518fd3d1f07a9cc774242866e95a431b02 /tactics/hints.ml | |
| parent | 8cdaa1b5c485ed351f9b3bf212ec5d88f8561908 (diff) | |
Adapt the documentation after deprecation of term hints.
Interestingly, the documentation for Hint Resolve -> qualid was outdated.
It was claiming that any term would be accepted, but actually with this
particular syntax, only qualified names would be parsed already.
Diffstat (limited to 'tactics/hints.ml')
0 files changed, 0 insertions, 0 deletions