anchor.diff:    | Trivial -> "trivial"
     | NonTrivial f ->
         if debug env Medium then
  -        Normalize.formula_norm_to_string env f
  +        Normalize.formula_norm_to_string env f
         else
           "non-trivial"
   
  
positive.code:     | None 
      | Some (NonTrivial _) ->  
        let r = Tc.Env.get_range env in
        raise (Error(Tc.Errors.basic_type_error env eopt t2 t1, r))
  
  let sub_comp env c1 c2 = 
    if debug env <| Other "Rel" then Util.fprint2 "sub_comp of %s and %s\n" (Print.comp_typ_to_string c1) (Print.comp_typ_to_string c2);
  
negative.code:  if debug env <| Other "Rel" then Util.fprint2 "try_subkind of %s and %s\n" (Print.kind_to_string k1) (Print.kind_to_string k2);
   let prob  = KProb(SUB, whnf_k env k1, whnf_k env k2) in
   Util.must <| solve_and_commit env None prob (fun _ -> 
      raise (Error(Tc.Errors.incompatible_kinds env k1 k2, Tc.Env.get_range env)))
  
  let try_subtype env t1 t2 = 
   if debug env <| Other "Rel" then Util.fprint2 "try_subtype of %s and %s\n" (Print.typ_to_string t1) (Print.typ_to_string t2);
  