aboutsummaryrefslogtreecommitdiff
path: root/library/goptions.mli
diff options
context:
space:
mode:
Diffstat (limited to 'library/goptions.mli')
-rw-r--r--library/goptions.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/library/goptions.mli b/library/goptions.mli
index 336cae420c..59b1667f5a 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -204,4 +204,5 @@ type option_state = {
val get_tables : unit -> option_state OptionMap.t
val print_tables : unit -> Pp.t
+val error_no_table_of_this_type : kind:string -> option_name -> 'a
val error_undeclared_key : option_name -> 'a