Term synthesis with local let binding gets stuck (warning 266: "Not an embedded ...")

[W95Psp]

Hi,

Tactics that pack embedded values depending on a local let binding declared outside the tactic seem to get stuck. For instance, below I pack some term_view, but as soon as the term view depends on a local binding that lives outside of the tactic, the tactic gets stuck. Top levels a to e work as expected, but the n let binding in f seems not rewritten as 1 at the time of execution of the tactic.

This bug seems independent from the embedding in stake (see bug_fv, bug_fv_too, bug_comp)

module NotAnEmbedded
open FStar.Tactics

let a: int = _ by (exact (pack (Tv_Const (C_Int 1))))
let b: int = _ by (let n = 1 in exact (pack (Tv_Const (C_Int n))))
let c: int = match 1 with | n -> _ by (exact (pack (Tv_Const (C_Int n))))
let d: int = (fun n -> _ by (exact (pack (Tv_Const (C_Int n))))) 1
let n=1  let e: int = _ by (exact (pack (Tv_Const (C_Int n))))

[@@expect_failure [228]]
let f: int = let n = 1 in _ by (exact (pack (Tv_Const (C_Int n))))

// More examples with different embeddings
let foo = 0
let works_fv: int = _ by (let name = pack_fv (explode_qn (`%foo)) in
                  exact (pack (Tv_FVar name)))
let name = pack_fv (explode_qn (`%foo))
let works_fv_too: int = _ by (exact (pack (Tv_FVar name)))
let works_comp: Type0 = _ by (let binder = fresh_binder (`unit) in
                              let comp   = pack_comp (C_Total (`unit) []) in
                              exact (pack (Tv_Arrow binder comp)))
[@@expect_failure [228]]
let bug_fv: int = let name = pack_fv (explode_qn (`%foo)) in
                _ by (exact (pack (Tv_FVar name)))
  
[@@expect_failure [228]]
let bug_fv_too: int = let name = explode_qn (`%foo) in
                    _ by (exact (pack (Tv_FVar (pack_fv name))))

[@@expect_failure [228]]
let bug_comp: Type0 = let comp = pack_comp (C_Total (`unit) []) in
                      _ by (let binder = fresh_binder (`unit) in
                            exact (pack (Tv_Arrow binder comp)))