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:         Err.raise_error (e, msg) r
      end
  
  let run_tactic_on_typ
          (rng_tac : Range.range) (rng_goal : Range.range)
          (tactic:term) (env:env) (typ:typ)
                      : list<goal> // remaining goals
                      * term // witness
                      =
      // This bit is really important: a typechecked tactic can contain many uvar redexes
      // that make normalization SUPER slow (probably exponential). Doing this first pass
      // gets rid of those redexes and leaves a much smaller term, which performs a lot better.
  