diff options
Diffstat (limited to 'theories/Compat/Coq88.v')
| -rw-r--r-- | theories/Compat/Coq88.v | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/theories/Compat/Coq88.v b/theories/Compat/Coq88.v index 4142af05..950cd824 100644 --- a/theories/Compat/Coq88.v +++ b/theories/Compat/Coq88.v @@ -9,3 +9,19 @@ (************************************************************************) (** 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. +Require Coq.ZArith.BinIntDef Coq.PArith.BinPosDef Coq.NArith.BinNatDef. +Require Coq.Reals.Rdefinitions. +Require Coq.Numbers.Cyclic.Int31.Int31. +Declare ML Module "string_syntax_plugin". +Declare ML Module "ascii_syntax_plugin". +Declare ML Module "r_syntax_plugin". +Declare ML Module "int31_syntax_plugin". +Numeral Notation BinNums.Z BinIntDef.Z.of_int BinIntDef.Z.to_int : Z_scope. +Numeral Notation BinNums.positive BinPosDef.Pos.of_int BinPosDef.Pos.to_int : positive_scope. +Numeral Notation BinNums.N BinNatDef.N.of_int BinNatDef.N.to_int : N_scope. |