diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-10-18 19:35:57 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-10-18 20:10:38 +0200 |
| commit | 14edc57ac5ad75bbc4ea8559111606aea8978f48 (patch) | |
| tree | b7c719062d46b1cca9bcd6f3ff1a81583b68e85e /pretyping/detyping.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 'pretyping/detyping.ml')
0 files changed, 0 insertions, 0 deletions