From e3ff85dccf62b497cd017d2b55e08e7f49ebd80f Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Wed, 2 Mar 2016 13:16:12 +0100 Subject: Removed old port to Coq 8.4 --- src/trace/structures.ml | 55 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 55 insertions(+) create mode 100644 src/trace/structures.ml (limited to 'src/trace/structures.ml') diff --git a/src/trace/structures.ml b/src/trace/structures.ml new file mode 100644 index 0000000..2c3a8d2 --- /dev/null +++ b/src/trace/structures.ml @@ -0,0 +1,55 @@ +(**************************************************************************) +(* *) +(* 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 *) +(* *) +(**************************************************************************) + + +open Entries +open Coqlib + + + +let gen_constant modules constant = lazy (gen_constant_in_modules "SMT" modules constant) + + + +(* Int63 *) +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 int63_modules "int" + +(* PArray *) +let parray_modules = [["Coq";"Array";"PArray"]] + +let max_array_size : int = + Parray.trunc_size (Uint63.of_int 4194303) +let mkArray : Term.types * Term.constr array -> Term.constr = + Term.mkArray + + +(* Differences between the two versions of Coq *) +let dummy_loc = Pp.dummy_loc + +let mkConst c = + { const_entry_body = c; + const_entry_type = None; + const_entry_secctx = None; + const_entry_opaque = false; + const_entry_inline_code = false} + +let glob_term_CbvVm = Glob_term.CbvVm None + +let error = Errors.error -- cgit