diff options
author | Chantal Keller <Chantal.Keller@inria.fr> | 2015-01-13 17:11:29 +0100 |
---|---|---|
committer | Chantal Keller <Chantal.Keller@inria.fr> | 2015-01-13 17:11:29 +0100 |
commit | 7072c4591668d2c21211a744d3719f6b42d1e7b9 (patch) | |
tree | 800520e1e414e10b29804a998c63764c18f2c1cd /src/versions/native/structures.ml | |
parent | 469a88043ad000403cff5122e27770c130ef77e4 (diff) | |
download | smtcoq-7072c4591668d2c21211a744d3719f6b42d1e7b9.tar.gz smtcoq-7072c4591668d2c21211a744d3719f6b42d1e7b9.zip |
Identify ML functions that depend on native-coq
Diffstat (limited to 'src/versions/native/structures.ml')
-rw-r--r-- | src/versions/native/structures.ml | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/src/versions/native/structures.ml b/src/versions/native/structures.ml new file mode 100644 index 0000000..8f74c32 --- /dev/null +++ b/src/versions/native/structures.ml @@ -0,0 +1,26 @@ +(**************************************************************************) +(* *) +(* SMTCoq *) +(* Copyright (C) 2011 - 2015 *) +(* *) +(* Michaël Armand *) +(* Benjamin Grégoire *) +(* Chantal Keller *) +(* *) +(* Inria - École Polytechnique - MSR-Inria Joint Lab *) +(* *) +(* This file is distributed under the terms of the CeCILL-C licence *) +(* *) +(**************************************************************************) + +(* Int63 *) +let int63_modules = [["Coq";"Numbers";"Cyclic";"Int63";"Int63Native"]] + +let mkInt i = Term.mkInt (Uint63.of_int i) + + +(* PArray *) +let parray_modules = [["Coq";"Array";"PArray"]] + +let max_array_size = Parray.trunc_size (Uint63.of_int 4194303) +let mkArray = Term.mkArray |