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: 
  let tacdbg = BU.mk_ref false
  
  let rec e_tactic_0' (er : embedding<'r>) : embedding<tac<'r>> =
      mk_emb (fun _ _ -> failwith "Impossible: embedding tactic (0)?")
             (fun w t -> Some <| unembed_tactic_0 er t)
             S.t_unit // never used
  
  and e_tactic_1 (ea : embedding<'a>) (er : embedding<'r>) : embedding<('a -> tac<'r>)> =
      mk_emb (fun _ _ -> failwith "Impossible: embedding tactic (1)?")
             (fun w t -> unembed_tactic_1 ea er t)
             S.t_unit // never used
  
  and primitive_steps () : list<Cfg.primitive_step> =
      (* NB: We need a PRECISE number for the universe arguments or NBE will
  
negative.code:       mktac1 0 "dump1"         print_proof_state1 e_string e_unit
                                 print_proof_state1 NBET.e_string NBET.e_unit;
  
        mktac2 0 "__pointwise"   pointwise E.e_direction (e_tactic_0 e_unit) e_unit
                                 pointwise E.e_direction_nbe (e_tactic_nbe_0 NBET.e_unit) NBET.e_unit;
  
        mktac2 0 "__topdown_rewrite" topdown_rewrite (e_tactic_1 RE.e_term (e_tuple2 e_bool e_int)) (e_tactic_0 e_unit) e_unit
                                     topdown_rewrite (e_tactic_nbe_1 NRE.e_term (NBET.e_tuple2 NBET.e_bool NBET.e_int)) (e_tactic_nbe_0 NBET.e_unit) NBET.e_unit;
  
        mktac1 0 "trefl"         trefl   e_unit e_unit
                                 trefl   NBET.e_unit NBET.e_unit;
  