aboutsummaryrefslogtreecommitdiff
path: root/dev/include_printers
diff options
context:
space:
mode:
authorcoqbot-app[bot]2021-03-23 20:38:58 +0000
committerGitHub2021-03-23 20:38:58 +0000
commit285d5e03a230af7b327cba0b7720217ede664761 (patch)
treed8f3bcac6bce50f5235e5416c7504b1b722a7848 /dev/include_printers
parentd3f78cad1532f000106ed0c0b8be2ac384ce1d3a (diff)
parent01b061f0082a70f66016e78075a5952af8ed5431 (diff)
Merge PR #13978: Do not match on record types with mutable fields in function arguments.
Reviewed-by: gares
Diffstat (limited to 'dev/include_printers')
0 files changed, 0 insertions, 0 deletions