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

Require Export Corelib.Compat.Rocq90.

#[export] Set Warnings "-deprecated-since-9.0".