anchor.diff:      match t.tm with
           | Var y -> Ident.lid_equals x y
           | _ -> false
  +
  +(* This does not have anything to do here *)
  +(* It must be moved asa the situation wrt F#/ocaml implementation file is cleaned up *)
  +exception Different
  +let is_prefix s s' =
  +    let n = FStar.String.strlen s in
  +    let n' = FStar.String.strlen s' in
  +    if n > n' then false
  +    else
  +        try for i = 0 to n-1 do
  +            if s.[i] <> s'.[i] then raise Different
  +            done ;
  +            true
  +        with Different -> false
  +
  +let is_tuple_constructor lid =
  +    let tuple_prefix = "Mktuple" in
  +    is_prefix tuple_prefix (text_of_lid lid)
  +
  +(* Automatic level assignment *)
  +(* would be perfect with a little of staging... *)
  +
  +type associativity =
  +    | Left
  +    | Right
  +    | NonAssoc
  +
  +(* A token is either a character c representing any string beginning with c or a complete string *)
  +type token = either<FStar.Char.char, string>
  +
  +type associativity_level = associativity * list<token>
  +
  +let matches_token (s:string) = function
  +    | Inl c -> s.[0] = c
  +    | Inr s' -> s = s'
  +
  +let matches_level s (assoc_levels, tokens) =
  +    List.existsb (matches_token s) tokens
  +
  +let assign_levels (token_associativity_spec : list<associativity_level>) : string -> int * int * int =
  +    in
  +    function s ->
  +        match List.find (matches_level s) level_table with
  +            | Some (assoc_levels, _) -> assoc_levels
  +            | _ -> failwith ("Unrecognized operator " ^ s)
  +
  +(* Precedence and associativity levels, taken from ../src/parse.mly *)
  +let opinfix4 = Right, [Inr "**"]
  +// level backtick won't be used here
  +let opinfix3 = Left,  [Inl '*' ; Inl '/' ; Inl '%']
  +let opinfix2 = Left,  [Inl '+' ; Inl '-' ]
  +let minus = Left, [Inr "-"] // Sublevel of opinfix2, not a level on its own !!!
  +let opinfix1 = Right, [Inl '@' ; Inl '^']
  +let pipe_right = Left,  [Inr "|>"]
  +let opinfix0d = Left,  [Inl '$']
  +let opinfix0c = Left,  [Inl '=' ; Inl '<' ; Inl '>']
  +let equal = Left, [Inr "="] // Sublevel of opinfix0c, not a level on its own !!!
  +let opinfix0b = Left,  [Inl '&']
  +let opinfix0a = Left,  [Inl '|']
  +let colon_equals = NonAssoc, [Inr ":="]
  +let amp = Right, [Inr "&"]
  +let colon_colon = Right, [Inr "::"]
  +
  +(* The latter the element, the tighter it binds *)
  +let level_associativity_spec =
  +  [
  +    colon_colon ;
  +    amp ;
  +    colon_equals ;
  +    opinfix0a ;
  +    opinfix0b ;
  +    opinfix0c ;
  +    opinfix0d ;
  +    pipe_right ;
  +    opinfix1 ;
  +    opinfix2 ;
  +    opinfix3 ;
  +    opinfix4
  +  ]
  +
  +let level_table =
  +  let levels_from_associativity (l:int) = function
  +    | Left -> l, l, l-1
  +    | Right -> l-1, l, l
  +    | NonAssoc -> l, l, l
  +  in
  +  List.mapi (fun i (assoc, tokens) -> (levels_from_associativity i assoc, tokens)) level_associativity_spec
  +
  +let max_level l =
  +  let find_level_and_max n level =
  +    match List.find (fun (_, tokens) -> tokens = snd level) level_table with
  +      | Some ((_,l,_), _) -> max n l
  +      | None -> failwith "Undefined associativity level"
  +  in List.fold_left find_level_and_max 0 l
  +
  +let level_of_operator = assign_levels spec
  +
  +let is_operatorInfix0ad12 =
  +    let opinfix0ad12 = [opinfix0a ; opinfix0b ; opinfix0c ; opinfix0d ; opinfix1 ; opinfix2 ] in
  +    fun op -> List.existsb (matches_level op) opinfix0ad12
   
   
   // printer really begins here
  
positive.code:       0, 0, -1
    | '|' ->
        -1, -1, -2
    | _ when op = "&" ->
        -2, -2, -1
    | _ when op = "::" ->
        -3, -3, -2
    | _ ->
        failwith ("invalid first character for infix operator " ^ op)
  
  
negative.code:   | e -> p_tmTuple e
  
  and p_tmTuple e = match e with
    | Construct (lid, args) when is_tuple_constructor lid ->
        separate_map comma p_tmEq args
    | e -> p_tmEq e
  
  and paren_if curr mine doc =
  