anchor.diff:        decls |> List.map doc_of_decl |> separate hardline
   
   
  -(* Automatic level assignment *)
  -(* would be perfect with a little of staging... *)
  -
  -type associativity =
  -    | Left
  -    | Right
  -    | NonAssoc
  -
  -type token = either<FStar.Char.char, string>
  -type associativity_level = associativity * list<token>
  -
  -let assign_levels (token_associativity_spec : list<associativity_level>) : string -> int * int * int =
  -    let levels_from_associativity (l:int) = function
  -        | Left -> l, l, l-1
  -        | Right -> l-1, l, l
  -        | NonAssoc -> l, l, l
  -    in
  -    let level_table =
  -        List.mapi (fun i (assoc, tokens) -> (levels_from_associativity i assoc, tokens)) token_associativity_spec
  -    in
  -    let matches_token s = function
  -        | Inl c -> s.[0] = c
  -        | Inl s' -> s = s'
  -    in
  -    let matches_level s (assoc_levels, tokens) =
  -        List.existsb (matches_token s) tokens
  -    in
  -    function s ->
  -        match List.find (matches_level s) with
  -            | Some assoc_levels -> assoc_levels
  -            | _ -> failwith ("Unrecognized operator " ^ s)
  -
  -let level_of_operator =
  -    let spec = [
  -        Left,  [Inl '*' ; Inl '/' ; Inl '%'];
  -        Left,  [Inl '+' ; Inl '-' ];
  -        Right, [Inl '@' Inl '^'] ;
  -        Left,  [Inr "|>"] ;
  -        Left,  [Inl '$'] ;
  -        Left,  [Inl '=' ; Inl '<' ; Inl '>'] ;
  -        Left,  [Inl '&'] ;
  -        Left,  [Inl '|']
  -        ]
  -    in assign_levels spec
  
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:     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
  