aboutsummaryrefslogtreecommitdiffstats
path: root/src/versions/standard/Int63/Int63_standard.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/versions/standard/Int63/Int63_standard.v')
-rw-r--r--src/versions/standard/Int63/Int63_standard.v26
1 files changed, 0 insertions, 26 deletions
diff --git a/src/versions/standard/Int63/Int63_standard.v b/src/versions/standard/Int63/Int63_standard.v
deleted file mode 100644
index 52be2c3..0000000
--- a/src/versions/standard/Int63/Int63_standard.v
+++ /dev/null
@@ -1,26 +0,0 @@
-(**************************************************************************)
-(* *)
-(* SMTCoq *)
-(* Copyright (C) 2011 - 2015 *)
-(* *)
-(* Chantal Keller *)
-(* *)
-(* from the Int63 library of native-coq *)
-(* by Benjamin Gregoire and Laurent Thery *)
-(* *)
-(* Inria - École Polytechnique - MSR-Inria Joint Lab *)
-(* *)
-(* This file is distributed under the terms of the CeCILL-C licence *)
-(* *)
-(**************************************************************************)
-
-
-(** Naive software representation of Int63. To improve. Anyway, if you
- want efficiency, rather use native-coq. **)
-
-(* Require Export Cyclic31. *)
-Require Export Ring31.
-Require Export Int63Native.
-Require Export Int63Op.
-Require Export Int63Axioms.
-Require Export Int63Properties.