Please ensure compatibility with Coq/Rocq 9.0
Please ensure compatibility with Coq/Rocq 9.0