blob: 1233a4b8f5f4476935268e5fcf2a7bea2041a9c4 (
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.Int63.Cyclic63.
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 Int63.is_zero 1.
|
