aboutsummaryrefslogtreecommitdiff
path: root/dev/base_include
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-08-31 11:40:02 +0000
committerGitHub2020-08-31 11:40:02 +0000
commitb4ff2af4f43a2e0ba40c7f8a6260da1c75859045 (patch)
tree0d7248091fc7283e52fb2f356eae9d90c13bd0d3 /dev/base_include
parent9c9bf136430213eacec8e32ad4909cf501141a48 (diff)
parent427e8cac2c267a7302b71979c0f1019598176e31 (diff)
Merge PR #12935: Drop opaque bodies of abstracted definitions.
Reviewed-by: SkySkimmer
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions