Learn
Platform
Packages
Community
Consortium
News
Learn
Platform
Packages
Community
Consortium
News
Get started
Core Library
Table of contents
Index
▾
Table of contents
Index
Library Corelib.Compat.Coq820
Compatibility file for making Rocq act similar to Coq v8.20
When removing this file, please cleanup the "-compat" option code in sysinit/coqargs.ml
#[
export
]
Set
Warnings
"-deprecated-since-9.0".