aboutsummaryrefslogtreecommitdiffstats
path: root/src/Int63/Int63.v
diff options
context:
space:
mode:
authorvblot <24938579+vblot@users.noreply.github.com>2021-07-07 08:55:25 +0200
committerGitHub <noreply@github.com>2021-07-07 08:55:25 +0200
commite2683e1e653a1b6872a886f4b99218e2803f7a74 (patch)
treee5058272d1f912065fd22d41d45d0e93a8c7c5ab /src/Int63/Int63.v
parent6a209bbc1bf5c90adb5f576093129fc62ce84780 (diff)
downloadsmtcoq-e2683e1e653a1b6872a886f4b99218e2803f7a74.tar.gz
smtcoq-e2683e1e653a1b6872a886f4b99218e2803f7a74.zip
use native integers (#96)
Diffstat (limited to 'src/Int63/Int63.v')
-rw-r--r--src/Int63/Int63.v23
1 files changed, 0 insertions, 23 deletions
diff --git a/src/Int63/Int63.v b/src/Int63/Int63.v
deleted file mode 100644
index acee305..0000000
--- a/src/Int63/Int63.v
+++ /dev/null
@@ -1,23 +0,0 @@
-(**************************************************************************)
-(* *)
-(* SMTCoq *)
-(* Copyright (C) 2011 - 2021 *)
-(* *)
-(* See file "AUTHORS" for the list of authors *)
-(* *)
-(* This file is distributed under the terms of the CeCILL-C licence *)
-(* *)
-(**************************************************************************)
-
-
-(** Glue with the Int31 library of standard coq, which is linked to
- native integers during VM computations.
-
- CAUTION: The name "Int63" is given for compatibility reasons, but
- int31 is used. **)
-
-Require Export Ring31.
-Require Export Int63Native.
-Require Export Int63Op.
-Require Export Int63Axioms.
-Require Export Int63Properties.