diff options
| author | Hugo Herbelin | 2020-04-13 09:19:49 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-12-09 11:04:47 +0100 |
| commit | df45fe3b4990ee64cb5ff13b00f3a2fac4623585 (patch) | |
| tree | 92b1fe303e8a6142930922ca90df3a862279a53b /interp/implicit_quantifiers.ml | |
| parent | c8c93bfea6e3c75ebce256f44043a34fe8933b5e (diff) | |
Constrintern cleanup: Centralizing calls to find_appl_head.
There are calls now in intern_impargs and CAppExpl.
This seems clearer and eventually allow to factorize code between term
and pattern interning.
Diffstat (limited to 'interp/implicit_quantifiers.ml')
0 files changed, 0 insertions, 0 deletions