Library Coq.Compat.Coq88

Compatibility file for making Coq act similar to Coq v8.8

Require Export Coq.Compat.Coq89.

In Coq 8.9, prim token notations follow Import rather than Require. So we make all of the relevant notations accessible in compatibility mode.

Require Coq.Strings.Ascii Coq.Strings.String.
Export String.StringSyntax Ascii.AsciiSyntax.
Require Coq.ZArith.BinIntDef Coq.PArith.BinPosDef Coq.NArith.BinNatDef.
Require Coq.Reals.Rdefinitions.
Require Coq.Numbers.Cyclic.Int63.Int63.
Require Coq.Numbers.Cyclic.Int31.Int31.