4 files changed, 9 insertions, 23 deletions
diff --git a/src/trace/coqInterface.ml b/src/trace/coqInterface.ml
index 4b0acc9..96fe6c1 100644
--- a/src/trace/coqInterface.ml
+++ b/src/trace/coqInterface.ml
@@ -101,26 +101,12 @@ let init_modules = Coqlib.init_modules
 
 
 (* Int63 *)
-let int63_modules = [["SMTCoq";"Int63";"Int63Native"]]
-
-(* 31-bits integers are "called" 63 bits (this is sound) *)
-let int31_module = [["Coq";"Numbers";"Cyclic";"Int31";"Int31"]]
-let cD0 = gen_constant int31_module "D0"
-let cD1 = gen_constant int31_module "D1"
-let cI31 = gen_constant int31_module "I31"
-
-let mkInt : int -> constr = fun i ->
-  let a = Array.make 31 (Lazy.force cD0) in
-  let j = ref i in
-  let k = ref 30 in
-  while !j <> 0 do
-    if !j land 1 = 1 then a.(!k) <- Lazy.force cD1;
-    j := !j lsr 1;
-    decr k
-  done;
-  mkApp (Lazy.force cI31, a)
-
-let cint = gen_constant int31_module "int31"
+let int63_module = [["Coq";"Numbers";"Cyclic";"Int63";"Int63"]]
+
+let mkInt : int -> Constr.constr =
+  fun i -> Constr.mkInt (Uint63.of_int i)
+
+let cint = gen_constant int63_module "int"
 
 
 (* PArray *)
diff --git a/src/trace/coqInterface.mli b/src/trace/coqInterface.mli
index d355053..f450f6d 100644
--- a/src/trace/coqInterface.mli
+++ b/src/trace/coqInterface.mli
@@ -65,7 +65,7 @@ val init_modules : string list list
 
 
 (* Int63 *)
-val int63_modules : string list list
+val int63_module : string list list
 val mkInt : int -> constr
 val cint : constr lazy_t
 
diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml
index 1c4ee81..67392bb 100644
--- a/src/trace/coqTerms.ml
+++ b/src/trace/coqTerms.ml
@@ -18,7 +18,7 @@ let gen_constant = CoqInterface.gen_constant
 
 (* Int63 *)
 let cint = CoqInterface.cint
-let ceq63 = gen_constant CoqInterface.int63_modules "eqb"
+let ceq63 = gen_constant CoqInterface.int63_module "eqb"
 
 (* PArray *)
 let carray = gen_constant CoqInterface.parray_modules "array"
diff --git a/src/trace/smtBtype.ml b/src/trace/smtBtype.ml
index c9aad70..d091758 100644
--- a/src/trace/smtBtype.ml
+++ b/src/trace/smtBtype.ml
@@ -51,7 +51,7 @@ let index_tbl = Hashtbl.create 17
 let index_to_coq i =
   try Hashtbl.find index_tbl i
   with Not_found ->
-    let interp = mklApp cTindex [|mkInt i|] in
+    let interp = mklApp cTindex [|mkN i|] in
     Hashtbl.add index_tbl i interp;
     interp