anchor.diff:      failwith ("Operation " ^ Ident.text_of_id op ^ " with " ^ string_of_int (List.length args) ^
                 " arguments couldn't be handled by the pretty printer")
     | Uvar id ->
  -    str "u#" ^^ str id.idText
  -//    failwith "Unexpected universe variable out of universe context"
  +    failwith "Unexpected universe variable out of universe context"
  +  | Labeled _ ->
  +    failwith "Unexpected labeled term"
   
     (* All the cases are explicitly listed below so that a modification of the ast doesn't lead to a loop *)
     (* We must also make sure that all the constructors listed below are handled somewhere *)
  
positive.code:     let es = extract_from_ref_set e in
      surround 2 0 (bang ^^ lbrace) (separate_map_or_flow (comma ^^ break1) p_appTerm es) rbrace
  
    (* KM : I still think that it is wrong to print a term that's not parseable... *)
    | Labeled (e, s, b) ->
        (* JP: what is this? can we remove it? *)
        str ("(*" ^ s ^ "*)") ^/^ p_term false false e
  
    (* Failure cases : these cases are not handled in the printing grammar since *)
    (* they are considered as invalid AST. We try to fail as soon as possible in order *)
    (* to prevent the pretty printer from looping *)
  
negative.code:   | [] -> true
    | x :: xs -> if f x then all f xs else false
  
  let all_explicit (args:list<(term*imp)>) : bool =
      BU.for_all (function
                  | (_, Nothing) -> true
                  | _ -> false) args
  
  (* [should_print_fs_typ_app] is set when encountering a [LightOff] pragma and *)
  (* reset at the end of each module. If you are using individual print function you *)
  (* should wrap them in [with_fs_typ_app] *)
  let should_print_fs_typ_app = BU.mk_ref false
  
  (* Tuples which come from a resugared AST, via term_to_document are already flattened *)
  (* This reference is set to false in term_to_document and checked in p_tmNoEqWith'    *)
  