aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativelambda.mli
diff options
context:
space:
mode:
authorGaëtan Gilbert2018-11-06 23:15:03 +0100
committerGaëtan Gilbert2018-11-16 15:08:46 +0100
commite2f1be274afa823e05c12878f9111bcfe60e3b50 (patch)
tree049787bda6baf9aeaebeda9b3bc69ef339f89a33 /kernel/nativelambda.mli
parentfa1301c9364a3f34fa6b7d6c7e54b5a8c1db19e9 (diff)
Termops.iter_constr_with_full_binders = EConstr.iter_with_full_binders
Diffstat (limited to 'kernel/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions