aboutsummaryrefslogtreecommitdiff
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, 0 insertions, 3 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 3996a1756c..98e1f6dd36 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -958,9 +958,6 @@ let rec extern inctx scopes vars r =
| GCast (c, c') ->
CCast (sub_extern true scopes vars c,
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)
in insert_coercion coercion (CAst.make ?loc c)