anchor.diff:      | _ -> n, Some u
   
   let rec univ_to_string u =
  +Errors.with_ctx "While printing universe" (fun () ->
     // VD: commented out for testing NBE
     // if not (Options.ugly()) then
     //   let e = Resugar.resugar_universe u Range.dummyRange in
  
positive.code: open FStar.Ident
  open FStar.Const
  
  module U = FStar.Util
  module A = FStar.Parser.AST
  module Resugar = FStar.Syntax.Resugar
  module ToDocument = FStar.Parser.ToDocument
  module Pp = FStar.Pprint
  module Unionfind = FStar.Syntax.Unionfind
  module C = FStar.Parser.Const
  module SU = FStar.Syntax.Util
  
  let rec delta_depth_to_string = function
      | Delta_constant_at_level i   -> "Delta_constant_at_level " ^ string_of_int i
  
negative.code: 
  and comp_to_string c =
    if not (Options.ugly()) then
      let e = Errors.with_ctx "While resugaring a computation" (fun () -> Resugar.resugar_comp c) in
      let d = ToDocument.term_to_document e in
      Pp.pretty_string (float_of_string "1.0") 100 d
    else
      Errors.with_ctx "While ugly-printing a computation" (fun () ->
      match c.n with
      | Total (t, uopt) ->
        begin match (compress t).n with
  