aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrextern.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 8a29fc3581..43fef8685d 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1000,7 +1000,7 @@ let rec extern inctx ?impargs scopes vars r =
mkFlattenedCApp (head,args))
| GLetIn (na,b,t,c) ->
- CLetIn (make ?loc na,sub_extern false scopes vars b,
+ CLetIn (make ?loc na,sub_extern (Option.has_some t) scopes vars b,
Option.map (extern_typ scopes vars) t,
extern inctx ?impargs scopes (add_vname vars na) c)