anchor.diff:              let rec resugar_body t = match (t.tm) with
                 | A.Match(e, None, [(_,_,b)]) -> b
                 | A.Let(_, _, b) -> b  // One branch Match that is resugared as Let
  -              | A.Ascribed(t1, t2, t3) ->
  +              | A.Ascribed(t1, t2, t3, use_eq) ->
                   (* this case happens when the match is wrapped in Meta_Monadic which is resugared to Ascribe*)
  -                mk (A.Ascribed(resugar_body t1, t2, t3))
  +                mk (A.Ascribed(resugar_body t1, t2, t3, use_eq))
                 | _ -> failwith("unexpected body format to try_with") in
               let e = resugar_body body in
               let rec resugar_branches t = match (t.tm) with
                 | A.Match(e, None, branches) -> branches
  -              | A.Ascribed(t1, t2, t3) ->
  +              | A.Ascribed(t1, t2, t3, _) ->
                   (* this case happens when the match is wrapped in Meta_Monadic which is resugared to Ascribe*)
                   (* TODO: where should we keep the information stored in Ascribed? *)
                   resugar_branches t1
  
positive.code: 
      | Tm_unknown -> mk A.Wild
  
  and resugar_ascription env (asc, tac_opt) =
    (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)
  
  (* This entire function is of course very tied to the the desugaring
  of calc expressions in ToSyntax. This only really works for fully
  
negative.code:     let bopt = BU.map_option (fun b ->
        BU.must (resugar_binder' env b r)
        |> A.ident_of_binder r) bopt in
      let asc, use_eq =
        match resugar_ascription env asc with
        | asc, None, use_eq -> asc, use_eq
        | _ -> failwith "resugaring does not support match return annotation with a tactic" in
      Some (bopt, asc, use_eq)
  
  
  and resugar_comp' (env: DsEnv.env) (c:S.comp) : A.term =
  