anchor.diff:      Err.log_issue (goal_type g).pos
           (Errors.Warning_TacAdmit, BU.format1 "Tactics admitted goal <%s>\n\n"
                       (goal_to_string g));
  -    solve g U.exp_unit)
  +    solve' g U.exp_unit)
   
   let fresh () : tac<Z.t> =
       bind get (fun ps ->
  
positive.code:        //NS: 01/24 ... looks redundant
          bind (add_implicits implicits.implicits) (fun _ ->
          // We solve with (), we don't care about the witness if applying a lemma
          bind (solve goal U.exp_unit) (fun _ ->
          let is_free_uvar uv t =
              let free_uvars = List.map (fun x -> x.ctx_uvar_head) (BU.set_elements (SF.uvars t)) in
              List.existsML (fun u -> UF.equiv u uv) free_uvars
  
negative.code:         Options.pop ();
      ret r))
  
  let remove_solved_goals : tac<unit> =
      bind get (fun ps ->
      let ps' = { ps with goals = List.filter (fun g -> Option.isNone (check_goal_solved g)) ps.goals } in
      set ps'
      )
  
  (*
     set_solution:
  
  