aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/term.mli
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-09-23 12:46:35 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-12-14 15:57:51 +0100
commit42610a4659cf35e6a005d79eec273c606bdf87dd (patch)
tree8a3168b468796527f8c95ab358534ff094d78388 /kernel/term.mli
parentc248228f5e910e19114e827661abb255c77a2b01 (diff)
Vm_compute: taking into account let-ins in parameters of constructors.
Diffstat (limited to 'kernel/term.mli')
0 files changed, 0 insertions, 0 deletions