diff options
| author | Hugo Herbelin | 2020-08-22 18:58:51 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-08-25 15:36:47 +0200 |
| commit | 27c1b6504b04c7653eced708492626be28a4f868 (patch) | |
| tree | a21f2dcd425ea6903231b31b21d85acea583270c /interp | |
| parent | 7f82d1387860860f1f6b2fb6e01759e92274349f (diff) | |
The body of a let is considered to be "in context" if its type is present.
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 2 |
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) |