aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/reduction.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-02-28 10:00:31 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-02-28 10:00:31 +0100
commit3a7a2b039761e6cd9aaff6be07e62c76a2781e40 (patch)
tree7798dd7da6e8b2cfe648d976f5555b385225c9af /kernel/reduction.ml
parent374e105be93beb2e9353bedf5cdd700a26308ebd (diff)
parent4e18be02a03ab478125aa6f08b30e738c3568572 (diff)
Merge PR #6823: Fixes #6821 (bug in protecting notation printing from infinite eta-expansion)
Diffstat (limited to 'kernel/reduction.ml')
0 files changed, 0 insertions, 0 deletions