anchor.diff:          Err.raise_error (e, msg) r
       end
   
  -let run_tactic_on_typ (tactic:term) (env:env) (typ:typ) : list<goal> // remaining goals
  -                                                        * term // witness
  -                                                        =
  -    let rng = tactic.pos in
  +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.
  
positive.code: 
  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
      // 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
  
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);
  