diff options
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 819f269..e3a6f70 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 -> () |