aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction/table.mli
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/extraction/table.mli')
-rw-r--r--plugins/extraction/table.mli4
1 files changed, 4 insertions, 0 deletions
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index b17f83715..16c2275f1 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -136,6 +136,10 @@ val optims : unit -> opt_flag
val conservative_types : unit -> bool
+(*s A comment to print at the beginning of the files *)
+
+val file_comment : unit -> string
+
(*s Target language. *)
type lang = Ocaml | Haskell | Scheme