Require Export Coq.Compat.Coq88.