From 0c50d5d193535f277454d2fcd70e0dc502fb2c23 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Mon, 23 Oct 2017 22:30:00 +0100
Subject: Type check external casts

---
 src/type_check.ml | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

(limited to 'src')

diff --git a/src/type_check.ml b/src/type_check.ml
index 58de77e1..d90e8d35 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -3232,12 +3232,13 @@ let check_fundef env (FD_aux (FD_function (recopt, tannotopt, effectopt, funcls)
    the difference is irrelevant for the typechecker. *)
 let check_val_spec env (VS_aux (vs, (l, _))) =
   let (id, quants, typ, env) = match vs with
-    | VS_val_spec (TypSchm_aux (TypSchm_ts (quants, typ), _), id, None, false) -> (id, quants, typ, env)
-    | VS_val_spec (TypSchm_aux (TypSchm_ts (quants, typ), _), id, None, true) -> (id, quants, typ, Env.add_cast id env)
-    | VS_val_spec (TypSchm_aux (TypSchm_ts (quants, typ), _), id, Some ext, false) ->
-       let env = Env.add_extern id ext env in
+    | VS_val_spec (TypSchm_aux (TypSchm_ts (quants, typ), _), id, ext_opt, is_cast) ->
+       let env = match ext_opt with
+         | None -> env
+         | Some ext -> Env.add_extern id ext env
+       in
+       let env = if is_cast then Env.add_cast id env else env in
        (id, quants, typ, env)
-    | _ -> typ_error l "Invalid valspec"
   in
   [DEF_spec (VS_aux (vs, (l, None)))], Env.add_val_spec id (quants, Env.expand_synonyms env typ) env
 
-- 
cgit v1.2.3