anchor.diff:          | Some t -> Some t
           | _ -> fallback fv
         end
  -    | Tm_uinst(e, us) -> resugar_term_as_op e
  +    | Tm_uinst(e, us) ->
  +      resugar_term_as_op e
       | _ -> None
   
   let is_true_pat (p:S.pat) : bool = match p.v with
  
positive.code:             | _::t -> last_three t
        in
        let resugar_as_app e args =
          let args = args |> List.map (fun (e, qual) ->
                resugar_term e) in
          let e = resugar_term e in
          List.fold_left(fun acc x -> mk (A.App(acc, x, A.Nothing))) e args
        in
        let args = if (Options.print_implicits()) then args else filter_imp args
        in
  
negative.code:     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
  