diff options
| author | Théo Zimmermann | 2019-11-27 20:29:29 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-11-27 20:29:29 +0100 |
| commit | ac99c6aba0091d5c1ee9511508e25d399425b61b (patch) | |
| tree | d21fb562b7a6f73b00f803909e2ecf181da4aa50 /lib/pp_diff.ml | |
| parent | 353b601323ffd7d5b4acc3c02de985b27cddc8e5 (diff) | |
| parent | 597a8a0e0f1bc50a0f1eb5fbdce52881df14aada (diff) | |
Merge PR #11199: Correcting unintended changelog message for #11090 (coercion+notation regression)
Reviewed-by: Zimmi48
Diffstat (limited to 'lib/pp_diff.ml')
0 files changed, 0 insertions, 0 deletions