diff options
Diffstat (limited to 'theories/Compat')
| -rw-r--r-- | theories/Compat/Coq88.v | 16 | ||||
| -rw-r--r-- | theories/Compat/Coq89.v (renamed from theories/Compat/Coq86.v) | 6 |
2 files changed, 17 insertions, 5 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. diff --git a/theories/Compat/Coq86.v b/theories/Compat/Coq89.v index 666be207..d2567188 100644 --- a/theories/Compat/Coq86.v +++ b/theories/Compat/Coq89.v @@ -8,8 +8,4 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(** Compatibility file for making Coq act similar to Coq v8.6 *) -Require Export Coq.Compat.Coq87. - -Require Export Coq.extraction.Extraction. -Require Export Coq.funind.FunInd. +(** Compatibility file for making Coq act similar to Coq v8.9 *) |