let printf_constraint 
    ?forall ?exists ?andsym ?before ?after ?user_name_from_int mode c = 
  let exists = default "exists " exists
  and forall = default "forall " forall 
  and andsym = default "and" andsym 
  and print_variable = print_variable ?user_name_from_int
  and print_crterm = print_crterm ?user_name_from_int 
  in

  let rec pconstraint c = 
    ignore (opt_apply before c); 
    (match c with
       | CTrue _ 
       | CConjunction []
       | CDisjunction [] -> 
           print_string "true"

       | CDump _ -> 
           print_string "dump"

       | CEquation (_, t1, t2) -> 
           printf "%s = %s"
             (print_crterm t1)
             (print_crterm t2)

       | CConjunction (c :: []) -> 
           pconstraint c

       | CConjunction (c :: cs) -> 
           printf "(";
           pconstraint c;
           List.iter (fun c -> 
                        printf "@ %s@ "
                          andsym;
                        if is_let c then paren 
                          (fun () -> pconstraint c) else pconstraint c) cs;
           printf ")"

       | CDisjunction (c :: []) -> 
           pconstraint c

       | CDisjunction (c :: cs) -> 
           assert false

       | CLet ([ Scheme (_, [], fqs, c, h) ], CTrue _) 
           when StringMap.empty = h -> 
           let rec chop_exists acu = function
             | CLet ([ Scheme (_, [], fqs', c', _) ], CTrue _) -> 
                 chop_exists (acu @ fqs') c'
             | lc -> (acu, lc)
           in
             let (fqs, c) = chop_exists fqs c in 
               if (List.length fqs <> 0) then
                 print_string exists;
               print_string (print_separated_list " " print_variable fqs);
               if (List.length fqs <> 0) then
                 printf ".@,";
               printf "@[<b 2>";
               pconstraint c; 
               printf "@]"

       | CLet (schemes, c) -> 
           printf "let @[<b>";
           printf_schemes schemes;
           printf "@]@ in@ @[<b>";
           pconstraint c;
           printf "@]"

       | CInstance (_, SName name, t) -> 
           printf "%s < %s" name (print_crterm t)
    );
    ignore (opt_apply after c) 


  and printf_schemes  = function
    | [] -> ()
    | [ x ] -> printf_scheme x
    | x :: q -> (printf_scheme x; print_cut (); print_string " ; "; 
                 print_cut (); printf_schemes q)

  and is_true = function CTrue _ -> true | _ -> false 

  and printf_scheme (Scheme (_, rqs, fqs, c, header)) = 
    let len = StringMap.fold (fun x k acu -> acu + 1) header 0 in
      printf "";
      if (List.length rqs + List.length fqs <> 0) then
        print_string forall;
      print_string (print_separated_list " " print_variable fqs);
      if rqs <> [] then 
        printf "{%s}" (print_separated_list " " print_variable rqs);
      if not (is_true c) then (
        printf "@,[@[<b>";
        pconstraint c;
        printf "@]]");
      if (len <> 0) then print_string "(";
      let f = ref true in
      let sep () = if !f then (f := false; "") else "; " in
        StringMap.iter (fun name (t, pos) -> printf "%s%s : %s"
                          (sep ())  name (print_crterm t))
          header;
        if (len <> 0) then print_string ")";


  in (
      active_mode mode;
      open_box 0;
      pconstraint c;
      close_box ();
      print_newline ();
    )