anchor.diff:    | Tm_let ((true, _), _) ->
       check_inner_let_rec env top
   
  -and tc_synth env args rng =
  +and tc_synth head env args rng =
       let tau, atyp, rest =
       match args with
       | (tau, None)::rest ->
  
positive.code:     let tau, _, g2 = tc_tactic env' tau in
      Rel.force_trivial_guard env' g2;
  
      // Don't run the tactic (and end with a magic) when nosynth is set, cf. issue #73 in fstar-mode.el
      let t =
          if env.nosynth
          then mk_Tm_app (TcUtil.fvar_const env Const.magic_lid) [S.as_arg exp_unit] None rng
          else begin
              let t = env.synth_hook env' typ ({ tau with pos = rng }) in
              if Env.debug env <| Options.Other "Tac" then
  
negative.code:     value_check_expected_typ env e tc implicits
  
    | Tm_uinst({n=Tm_fvar fv}, _)
    | Tm_fvar fv when S.fv_eq_lid fv Const.synth_lid && not env.phase1 ->
      raise_error (Errors.Fatal_BadlyInstantiatedSynthByTactic, "Badly instantiated synth_by_tactic") (Env.get_range env)
  
    | Tm_uinst({n=Tm_fvar fv}, us) ->
  