anchor.diff:      let bopt = BU.map_option (fun b ->
         BU.must (resugar_binder' env b r)
         |> A.ident_of_binder r) bopt in
  -    let asc =
  +    let asc, use_eq =
         match resugar_ascription env asc with
  -      | asc, None -> asc
  +      | asc, None, use_eq -> asc, use_eq
         | _ -> failwith "resugaring does not support match return annotation with a tactic" in
  -    Some (bopt, asc)
  +    Some (bopt, asc, use_eq)
   
   
   and resugar_comp' (env: DsEnv.env) (c:S.comp) : A.term =
  
positive.code:                   List.map resugar_branch branches))
  
      | Tm_ascribed(e, asc, _) ->
        let (asc, tac_opt) = resugar_ascription env asc in
        mk (A.Ascribed(resugar_term' env e, asc, tac_opt))
  
      | Tm_let((is_rec, source_lbs), body) ->
        let mk_pat a = A.mk_pattern a t.pos in
  
negative.code: 
      | Tm_unknown -> mk A.Wild
  
  and resugar_ascription env (asc, tac_opt, b) =
    (match asc with
     | Inl n -> (* term *)
       resugar_term' env n
     | Inr n -> (* comp *)
       resugar_comp' env n),
    BU.map_opt tac_opt (resugar_term' env),
    b
  
  (* This entire function is of course very tied to the the desugaring
  of calc expressions in ToSyntax. This only really works for fully
  