aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--src/versions/native/structures.ml3
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"]]