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.Int31.Int31
.