diff options
| author | coqbot-app[bot] | 2020-10-12 16:29:32 +0000 |
|---|---|---|
| committer | GitHub | 2020-10-12 16:29:32 +0000 |
| commit | 60e8fa2c4120a1f95e873c49929f4b879a814ddd (patch) | |
| tree | 064cf39dcc1d5df17a1ea618d9a7c5342f238696 /lib/pp_diff.ml | |
| parent | 917ac8b0dc8e0c9855cf3e9829d57e0ca1aaf13f (diff) | |
| parent | e58642678bcc40fba51dd012d51c8518b639d0ab (diff) | |
Merge PR #13163: [printing] make detyping resilient to "let x : _ := t in"
Reviewed-by: herbelin
Ack-by: SkySkimmer
Diffstat (limited to 'lib/pp_diff.ml')
0 files changed, 0 insertions, 0 deletions