diff options
| author | Pierre-Marie Pédrot | 2020-06-23 16:15:46 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-08-19 14:06:31 +0200 |
| commit | dc8b5beeb1d12d5c0e30143db468599ce0f1c1cc (patch) | |
| tree | 8bd1522e90d50428eb970e910ff61474d8269728 /dev | |
| parent | c5e68b50c6b4d7301acb437d0a439136f025868f (diff) | |
Replace Hints.head_constr_bound with Hints.head_bound.
The two implementations are essentially the same except for potential
interleaving of let-bindings and pattern-matchings. The only place
the removed function was called probably does not rely on this difference
of behaviour.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions