diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-02-28 10:00:31 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-02-28 10:00:31 +0100 |
| commit | 3a7a2b039761e6cd9aaff6be07e62c76a2781e40 (patch) | |
| tree | 7798dd7da6e8b2cfe648d976f5555b385225c9af /interp/constrintern.ml | |
| parent | 374e105be93beb2e9353bedf5cdd700a26308ebd (diff) | |
| parent | 4e18be02a03ab478125aa6f08b30e738c3568572 (diff) | |
Merge PR #6823: Fixes #6821 (bug in protecting notation printing from infinite eta-expansion)
Diffstat (limited to 'interp/constrintern.ml')
0 files changed, 0 insertions, 0 deletions