From b4686c78b9abbea40209f3780b73494f254c4750 Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Thu, 12 Feb 2015 12:09:58 +0100 Subject: Corrected a bug introduced in native compilation --- src/versions/native/structures.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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"]] -- cgit