From 1bce6b0f9f8cd614038a6e7fc21fb984724204a4 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Mon, 29 Dec 2008 13:12:08 +0000
Subject: Extract Coq lists to Caml lists.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@929 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 caml/CMtypecheck.ml | 14 ++++++--------
 1 file changed, 6 insertions(+), 8 deletions(-)

(limited to 'caml/CMtypecheck.ml')

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
-- 
cgit