anchor.diff:      | None ->
           Err.raise_error (Err.Fatal_TacticGotStuck, (BU.format1 "Tactic got stuck! Please file a bug report with a minimal reproduction of this issue.\n%s" (Print.term_to_string result))) proof_state.main_context.range
       )
  -//IN F*: and unembed_tactic_0' (#b:Type) (eb:embedding b) (embedded_tac_b:term) : option (tac b) =
  -and unembed_tactic_0'<'b> (eb:embedding<'b>) (embedded_tac_b:term) : option<(tac<'b>)> = //JUST FSHARP
  -    Some <| unembed_tactic_0 eb embedded_tac_b
  +
  +//IN F*: and unembed_tactic_nbe_1 (#a:Type) (#r:Type) (ea:NBET.embedding a) (er:NBET.embedding r) (f:NBET.t) : option (a -> tac r) =
  +and unembed_tactic_nbe_1<'a,'r> (ea:NBET.embedding<'a>) (er:NBET.embedding<'r>) (f:NBET.t) : option<('a -> tac<'r>)> = //JUST FSHARP
  +    Some (fun x ->
  +      let x_tm = NBET.embed ea x in
  +      let app = NBE.iapp f [NBET.as_arg x_tm] in
  +      unembed_tactic_nbe_0 er app)
  +
  +//IN F*: and unembed_tactic_nbe_0 (#b:Type) (eb:NBET.embedding b) (embedded_tac_b:NBET.t) : tac b =
  +and unembed_tactic_nbe_0<'b> (eb:NBET.embedding<'b>) (embedded_tac_b:NBET.t) : tac<'b> = //JUST FSHARP
  +    bind get (fun proof_state ->
  +
  +    (* Applying is normalizing!!! *)
  +    let result = NBE.iapp embedded_tac_b [NBET.as_arg (NBET.embed E.e_proofstate_nbe proof_state)] in
  +
  +    // F* requires more annotations.
  +    // IN F*: let res : option<__result<b>> = NBET.unembed (E.e_result_nbe eb) result in
  +    let res = NBET.unembed (E.e_result_nbe eb) result in //JUST FSHARP
  +
  +    match res with
  +    | Some (Success (b, ps)) ->
  +        bind (set ps) (fun _ -> ret b)
  +
  +    | Some (Failed (msg, ps)) ->
  +        bind (set ps) (fun _ -> fail msg)
  +
  +    | None ->
  +        Err.raise_error (Err.Fatal_TacticGotStuck, (BU.format1 "Tactic got stuck (in NBE)! Please file a bug report with a minimal reproduction of this issue.\n%s" (NBET.t_to_string result))) proof_state.main_context.range
  +    )
   
   let report_implicits ps (is : Env.implicits) : unit =
       let errs = List.map (fun imp ->
  
positive.code:       mktac1 0 "apply_lemma"   apply_lemma RE.e_term e_unit
                                 apply_lemma NRE.e_term NBET.e_unit;
  
        (* mktac5 2 "__divide"      (fun _ _ -> divide) e_any e_any e_int (e_tactic_0' e_any) (e_tactic_0' e_any) (e_tuple2 e_any e_any) *)
        (*                          (fun _ _ -> divide) NBET.e_any NBET.e_any NBET.e_int (e_tactic_0' e_any) (e_tactic_0' e_any) (e_tuple2 e_any e_any); *)
  
        (* mktac2 0 "__seq"         seq (e_tactic_0' e_unit) (e_tactic_0' e_unit) e_unit *)
        (*                          seq (e_tactic_0' e_unit) (e_tactic_0' e_unit) e_unit; *)
  
        mktac1 0 "set_options"   set_options e_string e_unit
                                 set_options NBET.e_string NBET.e_unit;
  
negative.code:       mktac1 0 "unshelve"      unshelve RE.e_term e_unit
                                 unshelve NRE.e_term NBET.e_unit;
  
        mktac2 1 "unquote"       unquote e_any RE.e_term e_any
                                 (fun _ _ -> failwith "NBE unquote") NBET.e_any NRE.e_term NBET.e_any;
  
        mktac1 0 "prune"         prune e_string e_unit
                                 prune NBET.e_string NBET.e_unit;
  