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/CMtypecheck.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/CMtypecheck.ml')
-rw-r--r-- | caml/CMtypecheck.ml | 14 |
1 files changed, 6 insertions, 8 deletions
diff --git a/caml/CMtypecheck.ml b/caml/CMtypecheck.ml index 1ac00654..d761f759 100644 --- a/caml/CMtypecheck.ml +++ b/caml/CMtypecheck.ml @@ -35,9 +35,7 @@ let tfloat = Base Tfloat let ty_of_typ = function Tint -> tint | Tfloat -> tfloat -let rec ty_of_sig_args = function - | Coq_nil -> [] - | Coq_cons(t, l) -> ty_of_typ t :: ty_of_sig_args l +let ty_of_sig_args tyl = List.map ty_of_typ tyl let rec repr t = match t with @@ -244,8 +242,8 @@ let rec type_expr env lenv e = and type_exprlist env lenv el = match el with - | Coq_nil -> [] - | Coq_cons (e1, et) -> + | [] -> [] + | e1 :: et -> let te1 = type_expr env lenv e1 in let tet = type_exprlist env lenv et in (te1 :: tet) @@ -352,8 +350,8 @@ let rec type_stmt env blk ret s = let rec env_of_vars idl = match idl with - | Coq_nil -> [] - | Coq_cons(id1, idt) -> (id1, newvar()) :: env_of_vars idt + | [] -> [] + | id1 :: idt -> (id1, newvar()) :: env_of_vars idt let type_function id f = try @@ -369,4 +367,4 @@ let type_fundef (Coq_pair (id, fd)) = | External ef -> () let type_program p = - coqlist_iter type_fundef p.prog_funct; p + List.iter type_fundef p.prog_funct; p |