aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/extraction/extraction.mli
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/extraction/extraction.mli')
-rw-r--r--contrib/extraction/extraction.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli
index 0f08f3128..e75e39fe6 100644
--- a/contrib/extraction/extraction.mli
+++ b/contrib/extraction/extraction.mli
@@ -23,7 +23,7 @@ type arity = Arity | NotArity
type type_var = info * arity
-type signature = (type_var * identifier) list
+type signature = type_var list
type extraction_context = bool list