From e3ff85dccf62b497cd017d2b55e08e7f49ebd80f Mon Sep 17 00:00:00 2001
From: Chantal Keller <Chantal.Keller@lri.fr>
Date: Wed, 2 Mar 2016 13:16:12 +0100
Subject: Removed old port to Coq 8.4

---
 src/versions/standard/structures.ml | 77 -------------------------------------
 1 file changed, 77 deletions(-)
 delete mode 100644 src/versions/standard/structures.ml

(limited to 'src/versions/standard/structures.ml')

diff --git a/src/versions/standard/structures.ml b/src/versions/standard/structures.ml
deleted file mode 100644
index a5fd69b..0000000
--- a/src/versions/standard/structures.ml
+++ /dev/null
@@ -1,77 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*     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 mklApp f args = Term.mkApp (Lazy.force f, args)
-let gen_constant modules constant = lazy (gen_constant_in_modules "SMT" modules constant)
-
-
-(* Int63 *)
-let int63_modules = [["SMTCoq";"versions";"standard";"Int63";"Int63Native"]]
-
-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 -> Term.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;
-  mklApp cI31 a
-
-let cint = gen_constant int31_module "int31"
-
-(* PArray *)
-let parray_modules = [["SMTCoq";"versions";"standard";"Array";"PArray"]]
-
-let cmake = gen_constant parray_modules "make"
-let cset = gen_constant parray_modules "set"
-
-let max_array_size : int = 4194302
-let mkArray : Term.types * Term.constr array -> Term.constr =
-  fun (ty, a) ->
-  let l = (Array.length a) - 1 in
-  snd (Array.fold_left (fun (i,acc) c ->
-                        let acc' =
-                          if i = l then
-                            acc
-                          else
-                            mklApp cset [|ty; acc; mkInt i; c|] in
-                        (i+1,acc')
-                       ) (0,mklApp cmake [|ty; mkInt l; a.(l)|]) a)
-
-
-(* Differences between the two versions of Coq *)
-let dummy_loc = Util.dummy_loc
-
-let mkConst c =
-  { const_entry_body = c;
-    const_entry_type = None;
-    const_entry_secctx = None;
-    const_entry_opaque = false}
-
-let glob_term_CbvVm = Glob_term.CbvVm
-
-let error = Util.error
-- 
cgit