anchor.diff:                  | None -> ()
                   | Some _ -> raise_error (Errors.Fatal_TypeWithinPatternsAllowedOnVariablesOnly, "Type ascriptions within patterns are cannot be associated with a tactic") orig.prange
           in
  -        let loc, env', binder, p, imp = aux loc env p in
  +        let loc, env', binder, p, annots, imp = aux loc env p in
           let annot_pat_var p t =
               match p.v with
               | Pat_var x -> {p with v=Pat_var({x with sort=t})}
  
positive.code:             let pat =
                  match pat with
                  | [] -> None
                  | [p] -> Some p
                  | _ ->
                    raise_error (Errors.Fatal_UnsupportedDisjuctivePatterns, "Disjunctive patterns are not supported in abstractions") p.prange
              in
  
negative.code: 
  (* TODO : Patterns should be checked that there are no incompatible type ascriptions *)
  (* and these type ascriptions should not be dropped !!!                              *)
  let rec desugar_data_pat env p is_mut : (env_t * bnd * list<annotated_pat>) =
    let check_linear_pattern_variables pats r =
      // returns the set of pattern variables
      let rec pat_vars p = match p.v with
  