diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-10-18 09:40:59 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-10-18 09:40:59 +0000 |
commit | cdcb658c29409c8aef94ca3e22c14a90b396aea0 (patch) | |
tree | 8981d0a2312604c6b8ab8a8acb108f39f1cd1377 /backend/CMtypecheck.ml | |
parent | f535ac931c2b7dc65fefa83e47bb8c79ca90e92d (diff) | |
download | compcert-cdcb658c29409c8aef94ca3e22c14a90b396aea0.tar.gz compcert-cdcb658c29409c8aef94ca3e22c14a90b396aea0.zip |
Extraction: map Coq pairs to Caml pairs and Coq chars (type ascii) to Caml chars
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1732 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/CMtypecheck.ml')
-rw-r--r-- | backend/CMtypecheck.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/CMtypecheck.ml b/backend/CMtypecheck.ml index 819f269e..e3a6f704 100644 --- a/backend/CMtypecheck.ml +++ b/backend/CMtypecheck.ml @@ -351,7 +351,7 @@ let type_function id f = with Error s -> raise (Error (sprintf "In function %s:\n%s" (extern_atom id) s)) -let type_fundef (Coq_pair (id, fd)) = +let type_fundef (id, fd) = match fd with | Internal f -> type_function id f | External ef -> () |