diff options
| author | Hugo Herbelin | 2015-10-18 19:35:57 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-10-18 20:10:38 +0200 |
| commit | 14edc57ac5ad75bbc4ea8559111606aea8978f48 (patch) | |
| tree | b7c719062d46b1cca9bcd6f3ff1a81583b68e85e /kernel/type_errors.ml | |
| parent | 28297a3994779fda9b9208cb90bd6f8f08d652c5 (diff) | |
Adding a function to mirror decompose_prod_n_assum in that it counts let-ins,
to compensate decompose_lam_n_assum which does not count let-ins.
Any idea on a uniform and clear naming scheme for this kind of
decomposition functions?
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions