diff options
| author | Chantal Keller <Chantal.Keller@inria.fr> | 2015-02-12 12:09:58 +0100 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@inria.fr> | 2015-02-12 12:09:58 +0100 |
| commit | b4686c78b9abbea40209f3780b73494f254c4750 (patch) | |
| tree | e65dcfc205df161aaf39892c66854fa6f161b46e | |
| parent | 6f4e3de82246a4fe8b431e704e0e362b81c9f065 (diff) | |
| download | smtcoq-b4686c78b9abbea40209f3780b73494f254c4750.tar.gz smtcoq-b4686c78b9abbea40209f3780b73494f254c4750.zip | |
Corrected a bug introduced in native compilation
| -rw-r--r-- | src/versions/native/structures.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/versions/native/structures.ml b/src/versions/native/structures.ml index 26edef3..2c3a8d2 100644 --- a/src/versions/native/structures.ml +++ b/src/versions/native/structures.ml @@ -15,6 +15,7 @@ open Entries +open Coqlib @@ -28,7 +29,7 @@ let int63_modules = [["Coq";"Numbers";"Cyclic";"Int63";"Int63Native"]] let mkInt : int -> Term.constr = fun i -> Term.mkInt (Uint63.of_int i) -let cint = gen_constant Structures.int63_modules "int" +let cint = gen_constant int63_modules "int" (* PArray *) let parray_modules = [["Coq";"Array";"PArray"]] |