blob: e2045900d5cdb17a6c6465f798dfc797879e8d8d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
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.
|
