diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-12-29 13:12:08 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-12-29 13:12:08 +0000 |
| commit | 1bce6b0f9f8cd614038a6e7fc21fb984724204a4 (patch) | |
| tree | 48683822666bc49b0101ed78f4d5059e834eb492 /caml/Camlcoq.ml | |
| parent | 12421d717405aa7964e437fc1167a23699b61ecc (diff) | |
| download | compcert-1bce6b0f9f8cd614038a6e7fc21fb984724204a4.tar.gz compcert-1bce6b0f9f8cd614038a6e7fc21fb984724204a4.zip | |
Extract Coq lists to Caml lists.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@929 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'caml/Camlcoq.ml')
| -rw-r--r-- | caml/Camlcoq.ml | 19 |
1 files changed, 0 insertions, 19 deletions
diff --git a/caml/Camlcoq.ml b/caml/Camlcoq.ml index e9089cf3..98fd79c8 100644 --- a/caml/Camlcoq.ml +++ b/caml/Camlcoq.ml @@ -77,25 +77,6 @@ let extern_atom a = with Not_found -> Printf.sprintf "<unknown atom %ld>" (camlint_of_positive a) -(* Lists *) - -let rec coqlist_iter f = function - Coq_nil -> () - | Coq_cons(a,l) -> f a; coqlist_iter f l - -let rec length_coqlist = function - | Coq_nil -> 0 - | Coq_cons (x, l) -> 1 + length_coqlist l - -let array_of_coqlist = function - | Coq_nil -> [||] - | Coq_cons(hd, tl) as l -> - let a = Array.create (length_coqlist l) hd in - let rec fill i = function - | Coq_nil -> a - | Coq_cons(hd, tl) -> a.(i) <- hd; fill (i + 1) tl in - fill 1 tl - (* Strings *) let char_of_ascii (Ascii.Ascii(a0, a1, a2, a3, a4, a5, a6, a7)) = |