diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index 1fb59068a..ea609f69d 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -1479,7 +1479,9 @@ struct let impl_val = ctx.interface_mode && not has_type in let let_impl = F.AST.TopLevelLet (NoLetQualifier, [ (pat, body) ]) in if impl_val then - let v = F.AST.Val (name, typ) in + let generics_types = List.map ~f:FStarBinder.to_typ generics in + let val_type = F.mk_e_arrow generics_types typ in + let v = F.AST.Val (name, val_type) in (F.decls ~fsti:true ~attrs:[ tcinst ] @@ v) @ F.decls ~fsti:false ~attrs:[ tcinst ] let_impl else F.decls ~fsti:ctx.interface_mode ~attrs:[ tcinst ] let_impl