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.mli5
1 files changed, 5 insertions, 0 deletions
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 8c009c662..158e33ec9 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -19,6 +19,7 @@ val safe_basename_of_global : global_reference -> identifier
(*s Warning and Error messages. *)
val warning_axioms : unit -> unit
+val warning_opaques : unit -> unit
val warning_both_mod_and_cst :
qualid -> module_path -> global_reference -> unit
val warning_id : string -> unit
@@ -83,6 +84,10 @@ val add_info_axiom : global_reference -> unit
val remove_info_axiom : global_reference -> unit
val add_log_axiom : global_reference -> unit
+val add_opaque_ok : global_reference -> unit
+val add_opaque_ko : global_reference -> unit
+val remove_opaque : global_reference -> unit
+
val reset_tables : unit -> unit
(*s AutoInline parameter *)