summaryrefslogtreecommitdiff
path: root/plugins/subtac/subtac_coercion.mli
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/subtac/subtac_coercion.mli')
-rw-r--r--plugins/subtac/subtac_coercion.mli4
1 files changed, 4 insertions, 0 deletions
diff --git a/plugins/subtac/subtac_coercion.mli b/plugins/subtac/subtac_coercion.mli
new file mode 100644
index 00000000..5678c10e
--- /dev/null
+++ b/plugins/subtac/subtac_coercion.mli
@@ -0,0 +1,4 @@
+open Term
+val disc_subset : types -> (types * types) option
+
+module Coercion : Coercion.S