diff options
| author | Pierre-Marie Pédrot | 2020-06-23 15:50:16 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-08-19 14:06:31 +0200 |
| commit | c5e68b50c6b4d7301acb437d0a439136f025868f (patch) | |
| tree | 98a366bd87198bc55457a558a92736ce4add093b /dev/include_printers | |
| parent | a9541e2ee557c04c4bc3476a36a87bc7fcdb06bb (diff) | |
Simplify the computation of the head global for hint patterns.
Instead of having to go through the pattern translation, we compute the
pattern directly from the term.
Diffstat (limited to 'dev/include_printers')
0 files changed, 0 insertions, 0 deletions