anchor.diff:      in
       let t1_star =  U.arrow [S.mk_binder <| S.new_bv None p_type] (S.mk_Total U.ktype0) in
       M t1,
  -    mk (Tm_ascribed (s_e, (Inl t1_star, None), None)) ,
  +    mk (Tm_ascribed (s_e, (Inl t1_star, None, false), None)) ,
       mk (Tm_match (u_e0, None, u_branches, None))
     end else begin
       let s_branches = List.map close_branch s_branches in
       let u_branches = List.map close_branch u_branches in
       let t1_star = t1 in
       N t1,
  -    mk (Tm_ascribed (mk (Tm_match (s_e0, None, s_branches, None)), (Inl t1_star, None), None)),
  +    mk (Tm_ascribed (mk (Tm_match (s_e0, None, s_branches, None)), (Inl t1_star, None, false), None)),
       mk (Tm_match (u_e0, None, u_branches, None))
     end
   
  
positive.code:       let u_body, u_rc_opt =
            let comp = trans_G env (U.comp_result comp) (is_monadic rc_opt) (SS.subst env.subst s_body) in
            (* TODO : consider removing this ascription *)
            U.ascribe u_body (Inr comp, None),
            Some (U.residual_comp_of_comp comp)
        in
  
  
negative.code:   | Tm_meta (t, m) ->
        mk (Tm_meta (star_type' env t, m))
  
    | Tm_ascribed (e, (Inl t, None, use_eq), something) ->
        mk (Tm_ascribed (star_type' env e, (Inl (star_type' env t), None, use_eq), something))
  
    | Tm_ascribed (e, (Inr c, None, use_eq), something) ->
        mk (Tm_ascribed (star_type' env e, (Inl (star_type' env (U.comp_result c)), None, use_eq), something))  //AR: this should effectively be the same, the effect checking for c should have done someplace else?
        (*raise_err (Errors.Fatal_TermOutsideOfDefLanguage, (BU.format1 "Tm_ascribed is outside of the definition language: %s"
                (Print.term_to_string t)))*)
  
   | Tm_ascribed (_, (_, Some _, _), _) ->
        raise_err (Errors.Fatal_TermOutsideOfDefLanguage, (BU.format1 "Ascriptions with tactics are outside of the definition language: %s"
          (Print.term_to_string t)))
  
  