Update comments based on @jung's suggestion.
Passed
Robbert Krebbers
created pipeline for commit
036103ab
, finished
Related merge request !469 to merge robbert/coq817
4 minutes 14 seconds, queued for 2 seconds