diff --git a/.travis.yml b/.travis.yml
index aed969474..8431d63ea 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -38,9 +38,11 @@ install:
   # Install dependencies
   - ${HOME}/opam pin add --no-action dolmen .
   - ${HOME}/opam install --deps-only dolmen.dev
+  - ${HOME}/opam pin add --no-action dolmen-export .
+  - ${HOME}/opam install --deps-only dolmen-export.dev
 script:
   # Build and launch the tests
   - if [ "$TO_TEST" = "tests" ]; then make bin && make test; fi
   # Try and install the package with opam
-  - if [ "$TO_TEST" = "install" ]; then ${HOME}/opam install dolmen.dev; fi
+  - if [ "$TO_TEST" = "install" ]; then ${HOME}/opam install dolmen.dev; ${HOME}/opam install dolmen-export.dev; fi
 
diff --git a/Makefile b/Makefile
index 0302455ae..c099d4b0b 100644
--- a/Makefile
+++ b/Makefile
@@ -7,7 +7,7 @@ BINDIR=_build/install/default/bin
 all: dune
 
 dune:
-	dune build --profile release
+	dune build -p dolmen
 
 bin: dune
 	cp $(BINDIR)/dolmen ./
diff --git a/dolmen-export.opam b/dolmen-export.opam
new file mode 100644
index 000000000..c8835d115
--- /dev/null
+++ b/dolmen-export.opam
@@ -0,0 +1,22 @@
+opam-version: "1.2"
+name: "dolmen-export"
+version: "dev"
+author: "Guillaume Bury"
+maintainer: "guillaume.bury@gmail.com"
+license: "BSD-2-clauses"
+build: [
+  ["dune" "subst"] {pinned}
+  ["dune" "build" "-p" name "-j" jobs]
+]
+depends: [
+  "dune" {build}
+  "dolmen"
+  "uutf"
+  "uucp"
+]
+available: [ ocaml-version >= "4.02.3" ]
+tags: [ "parser" "tptp" "logic" "smtlib" "dimacs" ]
+homepage: "https://github.com/Gbury/dolmen"
+doc: "http://gbury.github.io/dolmen"
+bug-reports: "https://github.com/Gbury/dolmen/issues"
+dev-repo: "https://github.com/Gbury/dolmen.git"
\ No newline at end of file
diff --git a/src/dune b/src/dune
index b38af9c0c..c691e7f0f 100644
--- a/src/dune
+++ b/src/dune
@@ -1,5 +1,5 @@
 
-(documentation)
+(documentation (package dolmen))
 
 (library
   (name           dolmen)
@@ -12,6 +12,7 @@
 )
 
 (executable
+  (package         dolmen)
   (name            main)
   (public_name     dolmen)
   (libraries       dolmen)
diff --git a/src/export/dune b/src/export/dune
new file mode 100644
index 000000000..44e9fbcba
--- /dev/null
+++ b/src/export/dune
@@ -0,0 +1,6 @@
+(library
+  (name           dolmen_export)
+  (public_name    dolmen-export)
+  (libraries      uutf uucp dolmen.std)
+  (modules        Escape Pretty Tptp Smtlib)
+)
\ No newline at end of file
diff --git a/src/export/escape.ml b/src/export/escape.ml
new file mode 100644
index 000000000..9aa7ae3fe
--- /dev/null
+++ b/src/export/escape.ml
@@ -0,0 +1,189 @@
+
+(* This file is free software, part of dolmen. See file "LICENSE" for more information. *)
+
+(** Escaping identifiers
+
+    This module provides facilities for escaping identifiers, i.e. make them conform
+    to some output syntax, which typically have restrictions on what are correct
+    identifiers.
+*)
+
+open Dolmen_std
+
+module H = Hashtbl.Make(Id)
+
+(* Printing wrappers for escapped sequences *)
+
+type status =
+  | Same    (* No changes to the identifiers name *)
+  | Escaped (* Identifiers has been escaped *)
+  | Renamed (* Identifier has been renamed due to a conflict
+               with another escaped or renamed identifier *)
+
+type name =
+  | Exact of string   (** The given name is to be printed exactly as is *)
+  | Normal of string  (** The given name should be escaped/renamed if necessary *)
+
+type t = {
+  lang   : string;
+  name   : Id.t -> name;     (* function for identifier name *)
+  escape : string -> string;  (* escape function, ideally idempotent *)
+  rename : string -> string;  (* renaming function, should have no fixpoint *)
+  (* Each escaping mechanism may need to distinguish different formatters when escaping symbols. *)
+  mutable tables  : (Format.formatter * (status * string) H.t) list;
+  mutable names  : (Format.formatter * (string, Id.t) Hashtbl.t) list;
+}
+
+let mk ~lang ~name ~escape ~rename = {
+  lang; name;
+  escape; rename;
+  tables = [];
+  names = [];
+}
+
+
+let pp_assign fmt (id, status, name) =
+  Format.fprintf fmt "@[<hov>%a@ %s@ %s@]"
+    Id.print id
+    (match status with
+     | Same -> "->"
+     | Escaped -> "~>"
+     | Renamed -> "~~>")
+    name
+
+let get_table t fmt =
+  try List.assq fmt t.tables
+  with Not_found ->
+    let h = H.create 4013 in
+    t.tables <- (fmt, h) :: t.tables;
+    h
+
+let get_names t fmt =
+  try List.assq fmt t.names
+  with Not_found ->
+    let h = Hashtbl.create 4013 in
+    t.names <- (fmt, h) :: t.names;
+    h
+
+(* Adding escapped sequences *)
+
+let rec add ?(fragile=false) fmt t any status name =
+  match Hashtbl.find (get_names t fmt) name with
+  | exception Not_found ->
+    add_success fmt t any status name
+  | r ->
+    assert (not (Id.equal any r));
+    if status = Same then begin
+      match H.find (get_table t fmt) r with
+      (** Two ids have the same name, we trust the developpers
+          that this is intended *)
+      | (Same, s) ->
+        assert (s = name);
+        add_success fmt t any status name
+      (** The escaped id collided with another escaped/renamed id,
+          this is a potentially dangerous situation. *)
+      | _ ->
+        add_failure ~fragile fmt t any status name r
+    end else
+      add_failure ~fragile fmt t any status name r
+
+and add_success fmt t any status name =
+  (* Util.debug ~section "Adding %a" pp_assign (any, status, name); *)
+  let () = H.add (get_table t fmt) any (status, name) in
+  let () = Hashtbl.add (get_names t fmt) name any in
+  name
+
+and add_failure ~fragile fmt t id status name r =
+  let conflict_st, conflict_name = H.find (get_table t fmt) r in
+  if fragile then
+    failwith (Format.asprintf "Escaping %a,@ conficted with@ %a"
+                pp_assign (id, status, name) pp_assign (r, conflict_st, conflict_name));
+  let new_name = t.rename name in
+  assert (new_name <> name);
+  add fmt t id Renamed new_name
+
+let escape fmt t any =
+  match H.find (get_table t fmt) any with
+  | (_, s) -> s
+  | exception Not_found ->
+    let fragile, status, new_name =
+      match t.name any with
+      | Exact name ->
+        true, Same, name
+      | Normal name ->
+        let s = t.escape name in
+        let status = if (s = name) then Same else Escaped in
+        false, status, s
+    in
+    add ~fragile fmt t any status new_name
+
+(* Convenience functions *)
+
+let id t fmt x =
+  Format.fprintf fmt "%s" (escape fmt t x)
+
+(* Unicode wrappers *)
+
+let encode e c =
+  match Uutf.encode e c with
+  | `Ok -> ()
+  | `Partial ->
+    (* should only happen with manual sources according to the doc,
+       so it is safe to assume it doesn't happen *)
+    assert false
+
+let encode_char e c = encode e (`Uchar c)
+
+let umap f s =
+  let encoding = `UTF_8 in
+  let b = Buffer.create (String.length s) in
+  let d = Uutf.decoder ~encoding (`String s) in
+  let e = Uutf.encoder encoding (`Buffer b) in
+  let rec aux () =
+    match Uutf.decode d with
+    | `End ->
+      let () = encode e `End in
+      Buffer.contents b
+    | `Await ->
+      let () = encode e `Await in
+      aux ()
+    | `Uchar c ->
+      let pos = Uutf.decoder_count d in
+      let () = List.iter (encode_char e) (f pos (Some c)) in
+      aux ()
+    | `Malformed _ ->
+      let pos = Uutf.decoder_count d in
+      let () = List.iter (encode_char e) (f pos None) in
+      aux ()
+  in
+  aux ()
+
+(* Print an Uchar *)
+
+let pp_uchar fmt c =
+  let b = Buffer.create 5 in
+  let () = Uutf.Buffer.add_utf_8 b c in
+  let s = Buffer.contents b in
+  Format.fprintf fmt "%s" s
+
+(* Renaming function *)
+
+let get_num ~sep s =
+  let rec aux acc mult i =
+    if i < 0 then s, 0
+    else match s.[i] with
+      | ('0' .. '9') as c ->
+        let j = int_of_char c - 48 in
+        aux (acc + j * mult) (mult * 10) (i - 1)
+      | c when c = sep ->
+        if i = 0 then s, 0 (* no base name found *)
+        else String.sub s 0 i, acc
+      | _ -> s, 0
+  in
+  aux 0 1 (String.length s - 1)
+
+let rename ~sep s =
+  let base, n = get_num ~sep s in
+  Format.sprintf "%s%c%d" base sep (n + 1)
+
+
diff --git a/src/export/escape.mli b/src/export/escape.mli
new file mode 100644
index 000000000..5f7403132
--- /dev/null
+++ b/src/export/escape.mli
@@ -0,0 +1,59 @@
+
+(* This file is free software, part of Dolmen. See file "LICENSE" for more details. *)
+
+(** Escpaing identifiers
+
+    This module provides helpers to print identifers
+    in languages that restricts the range of acceptable characters
+    (for instance HTML, Coq, ...) *)
+
+
+(** {2 Environment for escaping} *)
+
+type t
+(** The type of environnment/escaper for a given language.
+    Identifiers printed using a given environment, are escaped, and
+    its actual printed string recorded, in order to avoid future conflicts
+    with other escaped identifiers. *)
+
+val id : t -> Format.formatter -> Dolmen_std.Id.t -> unit
+(** Printer for archsat identifiers. *)
+
+(** {3 Identifier names} *)
+
+type name =
+  | Exact of string   (** The given name is to be printed exactly as is *)
+  | Normal of string  (** The given name should be escaped/renamed if necessary *)
+(** Variant type to specify the name (and status) of how an identifier should be
+    printed. Typically, id name that come from the input problem should be escaped,
+    while names declared inside the source code can ask to be exact (for instance,
+    qualified names using module paths should *not* be escaped, etc...) *)
+
+(** Custom environments *)
+
+val mk :
+  lang:string ->
+  name:(Dolmen_std.Id.t -> name) ->
+  escape:(string -> string) ->
+  rename:(string -> string) -> t
+(** Create an escaper from scratch. The name function is called to determine
+    the name of an identifier. The escape function is assumed
+    to be idempotent and have a lot of fixpoints (i.e. all valid identifiers
+    name should map to themselves) whereas the renaming function should
+    have absolutely no fixpoint (i.e. for all strings [rename s <> s]) *)
+
+val rename : sep:char -> string -> string
+(** A renaming function, which adds an increasing number after
+    the last occurrence of the given separator. *)
+
+val umap :
+  (int -> Uchar.t option -> Uchar.t list) ->
+  string -> string
+(** [umap f] provides an equivalent of flat_map on unicode strings.
+    [f] is given the position of the character in the string (starting from [1]),
+    and a unicode character (or [None] if decoding failed for that byte). *)
+
+val pp_uchar : Format.formatter -> Uchar.t -> unit
+(** Prints an uchar *)
+
+
diff --git a/src/export/pretty.ml b/src/export/pretty.ml
new file mode 100644
index 000000000..7479352ee
--- /dev/null
+++ b/src/export/pretty.ml
@@ -0,0 +1,22 @@
+
+(* This file is free software, part of dolmen. See file "LICENSE" for more information. *)
+
+type pos =
+  | Infix
+  | Prefix (**)
+(** The type for printing positions of identifiers. *)
+
+type assoc =
+  | Left
+  | Right (**)
+(** Associativity of operators. *)
+
+type t = {
+  name  : string;
+  pos   : pos;
+  assoc : assoc option;
+}
+
+let mk ?assoc name pos =
+  { name; pos; assoc; }
+
diff --git a/src/export/smtlib.ml b/src/export/smtlib.ml
new file mode 100644
index 000000000..db55293ff
--- /dev/null
+++ b/src/export/smtlib.ml
@@ -0,0 +1,167 @@
+(* This module contains the pretty-printer functions for smtlib *)
+
+open Dolmen_std
+open Pretty
+open Term
+
+(* auxiliar functions *)
+let pretty_builtin = function
+  | Wildcard -> assert false
+  | Ttype -> assert false
+  | Prop -> assert false
+  | True -> Pretty.mk "true" Pretty.Prefix
+  | False -> Pretty.mk "false" Pretty.Prefix
+  | Eq -> Pretty.mk "=" Pretty.Prefix
+  | Distinct -> assert false
+  | Ite -> Pretty.mk "ite" Pretty.Prefix
+  | Sequent -> assert false
+  | Int -> assert false
+  | Minus -> Pretty.mk "-" Pretty.Prefix
+  | Add -> Pretty.mk "+" Pretty.Prefix
+  | Sub -> Pretty.mk "-" Pretty.Prefix
+  | Mult -> Pretty.mk "*" Pretty.Prefix
+  | Lt -> Pretty.mk "<" Pretty.Prefix
+  | Leq -> Pretty.mk "<=" Pretty.Prefix
+  | Gt -> Pretty.mk ">" Pretty.Prefix
+  | Geq -> Pretty.mk ">=" Pretty.Prefix
+  | Subtype -> assert false
+  | Product -> assert false
+  | Union -> assert false
+  | Not -> Pretty.mk "not" Pretty.Prefix
+  | And -> Pretty.mk "and" Pretty.Prefix
+  | Or -> Pretty.mk "or" Pretty.Prefix
+  | Nand -> assert false
+  | Xor -> assert false
+  | Nor -> assert false
+  | Imply -> Pretty.mk "=>" Pretty.Prefix
+  | Implied -> assert false
+  | Equiv -> assert false
+
+let print_builtin fmt builtin =
+  Format.fprintf fmt "%s" (pretty_builtin builtin).name
+
+let print_binder = function
+  | All -> "forall"
+  | Ex -> "exists"
+  | Pi -> assert false
+  | Arrow -> ""
+  | Let -> assert false
+  | Fun -> ""
+  | Choice -> assert false
+  | Description -> assert false
+
+let rec print_descr fmt = function
+  | Symbol id -> Id.print fmt id
+  | Builtin builtin -> print_builtin fmt builtin
+  | Colon (term1, term2) ->
+      Format.fprintf fmt "%a %a" print_term term1 print_term term2
+  | App (term, term_list) ->
+      Format.fprintf fmt "(%a %a)" print term
+        (Misc.print_list ~print_sep:Format.fprintf ~sep:" " ~print:print_term)
+        term_list
+  | Binder (Fun, [], {term= Colon (u, v) as d; _}) ->
+      Format.fprintf fmt "() @ %a @ %a" print_term v print_term u
+  | Binder (Fun, term_list, {term= Colon (u, v) as d; _}) ->
+      Format.fprintf fmt "((%a)) @ %a @ %a"
+        (Misc.print_list ~print_sep:Format.fprintf ~sep:") (" ~print:print_term)
+        term_list print_term v print_term u
+  | Binder (binder, [], term) ->
+      Format.fprintf fmt "%s () @ %a" (print_binder binder) print_term term
+  | Binder (binder, ( {term= Symbol _; _} :: lst as term_list ), term) ->
+      Format.fprintf fmt "%s (%a) @ %a" (print_binder binder)
+        (Misc.print_list ~print_sep:Format.fprintf ~sep:" " ~print:print_term)
+        term_list print_term term
+  | Binder (binder, term_list, term) ->
+      Format.fprintf fmt "%s ((%a)) @ %a" (print_binder binder)
+        (Misc.print_list ~print_sep:Format.fprintf ~sep:") (" ~print:print_term)
+        term_list print_term term
+  | Match (term, term_pair_list) -> assert false
+
+and print_variables v = assert false
+
+(* terms *)
+and print_term fmt = function
+  | {term= Symbol _ as d; _} | {term= Builtin _ as d; _} -> print_descr fmt d
+  | e -> Format.fprintf fmt "%a" print_descr e.term
+
+open Statement
+
+(* statements *)
+let rec print_statement fmt = function
+  | Pack statement_list -> List.iter (fun a -> print fmt a) statement_list
+  | Pop n -> assert false
+  | Push n -> assert false
+  | Reset_assertions -> assert false
+  | Plain term -> assert false
+  | Prove term_list ->
+      Format.fprintf fmt "(check-sat %a) @."
+        (Misc.print_list ~print_sep:Format.fprintf ~sep:" @ " ~print:print_term)
+        term_list
+  | Clause term_list -> assert false
+  | Antecedent ({term= App (_,_); _} as term) ->
+      Format.fprintf fmt "@[<hov 2>(assert@ %a )@] @." print_term term
+  | Antecedent term ->
+      Format.fprintf fmt "@[<hov 2>(assert@ (%a) )@] @." print_term term
+  | Consequent term -> assert false
+  | Include str -> assert false
+  | Set_logic str -> Format.fprintf fmt "(set-logic %s) @." str
+  | Get_info str -> Format.fprintf fmt "@[<hov 2>(get-info@ %s)@]" str
+  | Set_info term -> Format.fprintf fmt "(set-info %a) @." print_term term
+  | Get_option str -> assert false
+  | Set_option term -> Format.fprintf fmt "(set-option %a) @." print_term term
+  | Def (id, ({term= Binder (binder, _, _); _} as term)) ->
+      Format.fprintf fmt "@[<hov 2>(define-%s @ %s @ %a)@] @."
+        ( match id.ns with
+        | Sort -> "sort"
+        | Term -> if binder = Fun then "fun" else assert false
+        | _ -> assert false )
+        (* way to detect a sort or a binded term *)
+        id.name print_term term
+  | Def (id, _) -> assert false
+  | Decl (id, ({term= Binder (binder, _, _); _} as term)) -> (
+    match binder with
+    | Arrow ->
+        Format.fprintf fmt "@[<hov 2>(declare-fun @ %a @ %a)@] @." Id.print id
+          print_term term
+    | _ -> assert false )
+  | Decl (id, term) ->
+      Format.fprintf fmt "@[<hov 2>(declare-const @ %a @ %a)@] @." Id.print id
+        print_term term
+  | Inductive i ->
+      let induct fmt =
+        let f =
+          Misc.print_list ~print_sep:Format.fprintf ~sep:" "
+            ~print:(fun fmt (cstr, l) ->
+              match l with
+              | [] -> Format.fprintf fmt "(%a)" Id.print cstr
+              | l ->
+                  Format.fprintf fmt "(%a (%a) )" Id.print cstr
+                    (Misc.print_list ~print_sep:Format.fprintf ~sep:") ("
+                       ~print:print_term)
+                    l )
+        in
+        function
+        | 0 -> Format.fprintf fmt "(%a)" f i.cstrs
+        | _ ->
+            Format.fprintf fmt "(par (%a) (%a) )"
+              (Misc.print_list ~print_sep:Format.fprintf ~sep:" "
+                 ~print:print_term)
+              i.vars f i.cstrs
+      in
+      Format.fprintf fmt
+        "@[<hov 2>(declare-datatypes @ ((%a %s)) @ (%a) ) @] @." Id.print i.id
+        (string_of_int (List.length i.vars))
+        induct (List.length i.vars)
+  | Get_proof -> assert false
+  | Get_unsat_core -> assert false
+  | Get_unsat_assumptions -> assert false
+  | Get_model -> Format.fprintf fmt "(get-model) @."
+  | Get_value term_list -> assert false
+  | Get_assignment -> assert false
+  | Get_assertions -> assert false
+  | Echo str -> assert false
+  | Reset -> assert false
+  | Exit -> assert false
+
+and print fmt = function
+  | {descr; _} -> Format.fprintf fmt "%a" print_statement descr
diff --git a/src/export/tptp.ml b/src/export/tptp.ml
new file mode 100644
index 000000000..e0a1f1145
--- /dev/null
+++ b/src/export/tptp.ml
@@ -0,0 +1,126 @@
+
+(* This file is free software, part of dolmen. See file "LICENSE" for more information. *)
+
+(** Pretty-printing terms in tptp syntax
+
+    This modules defines a pretty-printer for terms in the tptp syntax. *)
+
+open Dolmen_std
+
+(* Pretty printing information for builtins *)
+(* ************************************************************************ *)
+
+let pretty_builtin = function
+  | Term.Wildcard         -> Pretty.mk "$_" Pretty.Prefix
+  | Term.Ttype            -> Pretty.mk "Type" Pretty.Prefix
+  | Term.Prop             -> Pretty.mk "$o" Pretty.Prefix
+  | Term.True             -> Pretty.mk "$true" Pretty.Prefix
+  | Term.False            -> Pretty.mk "$false" Pretty.Prefix
+  | Term.Eq               -> Pretty.mk "=" Pretty.Infix
+  | Term.Distinct         -> Pretty.mk "$distinct" Pretty.Prefix
+
+  | Term.Ite              -> Pretty.mk "$ite" Pretty.Prefix
+  | Term.Sequent          -> Pretty.mk "-->" Pretty.Infix
+
+  | Term.Int              -> Pretty.mk "$int" Pretty.Prefix
+  | Term.Minus            -> Pretty.mk "$uminus" Pretty.Prefix
+  | Term.Add              -> Pretty.mk "$sum" Pretty.Prefix
+  | Term.Sub              -> Pretty.mk "$difference" Pretty.Prefix
+  | Term.Mult             -> Pretty.mk "$product" Pretty.Prefix
+  | Term.Lt               -> Pretty.mk "$less" Pretty.Prefix
+  | Term.Leq              -> Pretty.mk "$lesseq" Pretty.Prefix
+  | Term.Gt               -> Pretty.mk "$greater" Pretty.Prefix
+  | Term.Geq              -> Pretty.mk "$greatereq" Pretty.Prefix
+
+  | Term.Subtype          -> Pretty.mk "<<" Pretty.Infix
+  | Term.Product          -> Pretty.mk "*" Pretty.Infix
+  | Term.Union            -> Pretty.mk "+" Pretty.Infix
+
+  | Term.Not              -> Pretty.mk "~" Pretty.Prefix
+  | Term.And              -> Pretty.mk "&" Pretty.Infix ~assoc:Pretty.Left
+  | Term.Or               -> Pretty.mk "|" Pretty.Infix ~assoc:Pretty.Left
+  | Term.Nand             -> Pretty.mk "~&" Pretty.Infix
+  | Term.Xor              -> Pretty.mk "<~>" Pretty.Infix
+  | Term.Nor              -> Pretty.mk "~|" Pretty.Infix
+  | Term.Imply            -> Pretty.mk "=>" Pretty.Infix ~assoc:Pretty.Right
+  | Term.Implied          -> Pretty.mk "<=" Pretty.Infix
+  | Term.Equiv            -> Pretty.mk "<=>" Pretty.Infix
+
+(* Variables and constants escaping *)
+(* ************************************************************************ *)
+
+let is_dollar c = Uchar.equal c (Uchar.of_char '$')
+let is_underscore c = Uchar.equal c (Uchar.of_char '_')
+
+let is_alpha c = Uucp.Alpha.is_alphabetic c
+let is_num c = Uucp.Num.numeric_type c <> `None
+
+(** Alphanumeric characters as defined by tptp (yes, it includes underscores, :p ) *)
+let is_alphanum c = is_alpha c || is_num c || is_underscore c
+
+let var_escape =
+  let name id = Escape.Normal (Dolmen_std.Id.full_name id) in
+  let rename = Escape.rename ~sep:'_' in
+  let escape = Escape.umap (fun i -> function
+      | None -> [ Uchar.of_char '_' ]
+      | Some c ->
+        begin match Uucp.Block.block c with
+          | `ASCII when i = 1 && is_underscore c ->
+            [Uchar.of_char 'V'; c]
+          | `ASCII when i = 1 && Uucp.Case.is_lower c ->
+            begin match Uucp.Case.Map.to_upper c with
+              | `Self -> [ c ]
+              | `Uchars l -> l
+            end
+          | `ASCII when (i = 1 && is_dollar c) || is_alphanum c ->
+            [ c ]
+          | _ -> [ Uchar.of_char 'V'; Uchar.of_char '_' ]
+        end) in
+  Escape.mk ~lang:"tptp" ~name ~escape ~rename
+
+let cst_escape =
+  let name id = Escape.Normal (Dolmen_std.Id.full_name id) in
+  let rename = Escape.rename ~sep:'_' in
+  let escape = Escape.umap (fun i -> function
+      | None -> [ Uchar.of_char '_' ]
+      | Some c ->
+        begin match Uucp.Block.block c with
+          | `ASCII when i = 1 && is_underscore c ->
+            [Uchar.of_char 'V'; c]
+          | `ASCII when i = 1 && Uucp.Case.is_upper c ->
+            begin match Uucp.Case.Map.to_lower c with
+              | `Self -> [ c ]
+              | `Uchars l -> l @ [Uchar.of_char '_']
+            end
+          | `ASCII when (i = 1 && is_dollar c) || is_alphanum c ->
+            [ c ]
+          | _ -> [ Uchar.of_char '_' ]
+        end) in
+  Escape.mk ~lang:"tptp" ~name ~escape ~rename
+
+(* Printing functions for terms *)
+(* ************************************************************************ *)
+
+let var fmt v = Escape.id var_escape fmt v
+let cst fmt c = Escape.id cst_escape fmt c
+
+let id fmt id = assert false (* match on the id namespace *)
+
+let builtins fmt b = assert false
+
+and binder fmt b = assert false
+
+and colon fmt (u, v) = assert false
+
+and app fmt (f, args) = assert false
+
+and _match fmt (e, branches) = assert false
+
+and term_descr fmt d = assert false
+
+and term fmt t = assert false
+
+(* Printing functions for formulas *)
+(* ************************************************************************ *)
+
+
diff --git a/src/standard/statement.mli b/src/standard/statement.mli
index 506846f3f..73ab718d1 100644
--- a/src/standard/statement.mli
+++ b/src/standard/statement.mli
@@ -23,7 +23,7 @@ type inductive = {
   cstrs : (Id.t * term list) list;
   loc : location option;
 }
-(** The type for inductive type declarations. The "vars" field if used
+(** The type for inductive type declarations. The "vars" field is used
     to store polymorphic variables of the inductive type. For instance,
     a polymorphic type for lists would have a single variable "a".
     The constructors each have a name and a list of concrete arguments types