diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
commit | 9ebf44d84754adc5b64fcf612c6816c02c80462d (patch) | |
tree | bf5e06a28488e0e06a2f2011ff0d110e2e02f8fc /theories/Compat | |
parent | 9043add656177eeac1491a73d2f3ab92bec0013c (diff) |
Imported Upstream version 8.9.0upstream/8.9.0upstream
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 *) |