diff options
Diffstat (limited to 'src/versions/standard/Int63/Int63_standard.v')
-rw-r--r-- | src/versions/standard/Int63/Int63_standard.v | 26 |
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. |