anchor.diff:      if b then None
       else Some (Some A.Implicit)
     | Some S.Equality -> Some (Some A.Equality)
  +
  +let resugar_imp (q:option<S.arg_qualifier>) : A.imp =
  +  match q with
  +  | None -> A.Nothing
  +  | Some (S.Implicit false) -> A.Hash
  +  | Some Equality
  +  | Some (S.Implicit true) ->
  +    (* This should be a proper error rather than a failwith *)
  +    failwith "Not an imp"
  +
  +let resugar_arg_qual (q:option<S.arg_qualifier>) : option<(option<A.arg_qualifier>)> =
  +    match q with
  +    | 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
  
positive.code:     else
        None
  
  let rec resugar_term_as_op(t:S.term) : option<(string*int)> =
    let infix_prim_ops = [
      (C.op_Addition    , "+" );
      (C.op_Subtraction , "-" );
  
negative.code:                       | _ -> failwith "wrong Data_app head format"
                      in
                      let head, universes = aux head in
                      let universes =
                          List.map (fun u -> (resugar_universe u t.pos, A.UnivApp)) universes
                      in
                      let args = List.map (fun (t, q) -> (resugar_term t, resugar_imp q)) args in
                      let args =
                          // ToDocument doesn't expect uvar that is added by the
                          // typechecker in tuple constructor
                          // TODO: where should be store the universe information?
                          if C.is_tuple_data_lid' head || not (Options.print_universes ()) then
                              args
                          else universes @ args
                       in
                       mk (A.Construct(head, args))
                  | Tm_meta(_, m) ->
                    // the Tm_app for Data_app could be wrapped inside Tm_meta(_, Meta_monadic) after TypeChecker
                    // applies monadic_application
  