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