aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/constrextern.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/constrextern.ml')
-rw-r--r--interp/constrextern.ml3
1 files changed, 3 insertions, 0 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 1330b3741..4f7d537d3 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -908,6 +908,9 @@ let rec extern inctx scopes vars r =
| GCast (c, c') ->
CCast (sub_extern true scopes vars c,
Miscops.map_cast_type (extern_typ scopes vars) c')
+ | GProj (p, c) ->
+ let pr = extern_reference ?loc Id.Set.empty (ConstRef (Projection.constant p)) in
+ CProj (pr, sub_extern inctx scopes vars c)
) r'
and extern_typ (_,scopes) =