diff options
| author | Gaëtan Gilbert | 2018-11-06 23:15:03 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-16 15:08:46 +0100 |
| commit | e2f1be274afa823e05c12878f9111bcfe60e3b50 (patch) | |
| tree | 049787bda6baf9aeaebeda9b3bc69ef339f89a33 /kernel/type_errors.mli | |
| parent | fa1301c9364a3f34fa6b7d6c7e54b5a8c1db19e9 (diff) | |
Termops.iter_constr_with_full_binders = EConstr.iter_with_full_binders
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions