anchor.diff:          else term_to_string t
   
         | Tm_unknown -> "_"
  +    )
     end
   
   and branch_to_string (p, wopt, e) : string =
  
positive.code:           else U.format2 "%s (%s)" (sli c.effect_name) (term_to_string c.result_typ) in
        let dec = c.flags |> List.collect (function DECREASES e -> [U.format1 " (decreases %s)" (term_to_string e)] | _ -> []) |> String.concat " " in
        U.format2 "%s%s" basic dec
  
  and cflag_to_string c =
      match c with
  
negative.code: open FStar.Ident
  open FStar.Const
  
  module Errors     = FStar.Errors
  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
  