anchor.diff:  
   let synthesize (env:Env.env) (typ:typ) (tau:term) : term =
       tacdbg := Env.debug env (Options.Other "Tac");
  -    let tau = reify_tactic tau in
  -    let gs, w = run_tactic_on_typ tau env typ in
  +    let gs, w = run_tactic_on_typ tau.pos typ.pos (reify_tactic tau) env typ in
       // Check that all goals left are irrelevant. We don't need to check their
       // validity, as we will typecheck the witness independently.
       if List.existsML (fun g -> not (Option.isSome (getprop (goal_env g) (goal_type g)))) gs
  
positive.code:             when S.fv_eq_lid fv PC.by_tactic_lid ->
          begin match pol with
          | Pos ->
              let gs, _ = run_tactic_on_typ tactic e assertion in
              Simplified (FStar.Syntax.Util.t_true, gs)
  
          | Both ->
              let gs, _ = run_tactic_on_typ tactic e assertion in
              Dual (assertion, FStar.Syntax.Util.t_true, gs)
  
          | Neg ->
  
negative.code:     let env = { env with Env.instantiate_imp = false } in
      (* TODO: We do not faithfully expose universes to metaprograms *)
      let env = { env with Env.lax_universes = true } in
      let rng = range_of_rng (use_range rng_goal) (use_range rng_tac) in
      let ps, w = proofstate_of_goal_ty rng env typ in
      if !tacdbg then
          BU.print1 "Running tactic with goal = %s\n" (Print.term_to_string typ);
  