aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-11-27 17:04:01 +0000
committerGitHub2020-11-27 17:04:01 +0000
commit0501761b95f4fd3e22b93aa6bce8c9f96b88495b (patch)
tree672b5f5916402923ac59329f3f068d7d758ecf19 /kernel
parentf733414e59afb37cad41c65b11bc4c817bd137f9 (diff)
parentce8569a3713536e510381e4d49d534a447cfe637 (diff)
Merge PR #13483: Fix #13283: improved error on `clear implicit` flag
Reviewed-by: Zimmi48
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions