diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/Compat88.v | 18 | ||||
| -rw-r--r-- | test-suite/success/NumeralNotations.v | 19 |
2 files changed, 37 insertions, 0 deletions
diff --git a/test-suite/success/Compat88.v b/test-suite/success/Compat88.v new file mode 100644 index 0000000000..e2045900d5 --- /dev/null +++ b/test-suite/success/Compat88.v @@ -0,0 +1,18 @@ +(* -*- coq-prog-args: ("-compat" "8.8") -*- *) +(** Check that various syntax usage is available without importing + relevant files. *) +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.Cyclic31. + +Require Import Coq.Compat.Coq88. (* XXX FIXME Should not need [Require], see https://github.com/coq/coq/issues/8311 *) + +Check String.String "a" String.EmptyString. +Check String.eqb "a" "a". +Check Nat.eqb 1 1. +Check BinNat.N.eqb 1 1. +Check BinInt.Z.eqb 1 1. +Check BinPos.Pos.eqb 1 1. +Check Rdefinitions.Rplus 1 1. +Check Int31.iszero 1. diff --git a/test-suite/success/NumeralNotations.v b/test-suite/success/NumeralNotations.v index 5a58a1b72d..bacc982ccc 100644 --- a/test-suite/success/NumeralNotations.v +++ b/test-suite/success/NumeralNotations.v @@ -228,3 +228,22 @@ Module Test13. Fail Numeral Notation unit of_uint to_uint'' : test13''_scope. Fail Check let v := 0%test13'' in v : unit. End Test13. + +Module Test14. + (* Test that numeral notations follow [Import], not [Require], and + also test for current (INCORRECT!!) behavior that [Local] has no + effect in modules. *) + Delimit Scope test14_scope with test14. + Delimit Scope test14'_scope with test14'. + Module Inner. + Definition to_uint (x : unit) : Decimal.uint := Nat.to_uint O. + Definition of_uint (x : Decimal.uint) : unit := tt. + Local Numeral Notation unit of_uint to_uint : test14_scope. + Global Numeral Notation unit of_uint to_uint : test14'_scope. + End Inner. + Fail Check let v := 0%test14 in v : unit. + Fail Check let v := 0%test14' in v : unit. + Import Inner. + Check let v := 0%test14 in v : unit. (* THIS SHOULD FAIL!! *) + Check let v := 0%test14' in v : unit. +End Test14. |