aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-12-22 21:32:35 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-12-22 21:54:26 +0100
commitf5575393258492837d3764d07f8290b576f61160 (patch)
tree18d33a63880226185f6fb3cd8b6f31cb3e965a28 /CHANGES
parent59e361cd4118fdb974081fc0b2aec02136fde444 (diff)
Fixing injection in the presence of let-in in constructors.
This also fixes decide equality, discriminate, ... (see e.g. #5279).
Diffstat (limited to 'CHANGES')
0 files changed, 0 insertions, 0 deletions