anchor.diff:  
   let filter_imp a = a |> List.filter (function (_, Some (S.Implicit _)) -> false | _ -> true)
   
  -let resugar_arg_qual (q:option<S.arg_qualifier>) : option<A.arg_qualifier> =
  +(* If resugar_arg_qual returns None, the corresponding binder should *not* be resugared *)
  +let resugar_arg_qual (q:option<S.arg_qualifier>) : option<(option<A.arg_qualifier>)> =
     match q with
  -    | None -> None
  -    | Some (S.Implicit b) -> Some A.Implicit  //TODO: how should we map this flag back to the surface?
  -    | Some S.Equality -> Some A.Equality
  +  | None -> Some None
  +  | Some (S.Implicit b) ->
  +    (* TODO : set an option to print these inaccessible patterns *)
  +    if b then None
  +    else Some (Some A.Implicit)
  +  | Some S.Equality -> Some (Some A.Equality)
   
   let rec universe_to_int n u =
     match u with
  -    | U_succ u -> universe_to_int (n+1) u
  -    | _ -> (n, u)
  +  | U_succ u -> universe_to_int (n+1) u
  +  | _ -> (n, u)
   
   let rec resugar_universe (u:S.universe) r: A.term =
     let mk (a:A.term') r: A.term =
  -      //augment `a` an Unknown level (the level is unimportant ... we should maybe remove it altogether)
  -      A.mk_term a r A.Un
  +    //augment `a` an Unknown level (the level is unimportant ... we should maybe remove it altogether)
  +    A.mk_term a r A.Un
     in
     begin match u with
       | U_zero ->
  
positive.code: module D = FStar.Parser.ToDocument
  
  let bv_as_unique_ident (x:S.bv) : I.ident =
    let unique_name =  
      if starts_with reserved_prefix x.ppname.idText then
        x.ppname.idText ^ (string_of_int x.index)
      else
  
negative.code:         else
            A.mk_binder (A.Annotated(bv_as_unique_ident x, e)) r A.Type_level None
  
  and resugar_bv_as_pat (x:S.bv) qual: option<A.pattern> =
    let mk a = A.mk_pattern a (S.range_of_bv x) in
    match (SS.compress x.sort).n with
    //| Tm_type U_unknown
    | Tm_unknown ->
      let i = String.compare x.ppname.idText I.reserved_prefix in
      if i = 0 then
        Some (mk (A.PatWild))
      else
        BU.bind_opt (resugar_arg_qual qual) (fun aq -> mk (A.PatVar(bv_as_unique_ident x, )))
    | _ ->
      BU.bind_opt (resugar_arg_qual qual)
        begin fun aq ->
          let pat = mk (A.PatVar(bv_as_unique_ident x, aq)) in
          if Options.print_bound_var_types() then
            mk (A.PatAscribed(pat, resugar_term x.sort))
          else
            pat
        end
  
  and resugar_match_pat (p:S.pat) : A.pattern =
    (* We lose information when desugar PatAscribed to able to resugar it back *)
  