aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/typeops.mli
diff options
context:
space:
mode:
Diffstat (limited to 'checker/typeops.mli')
-rw-r--r--checker/typeops.mli3
1 files changed, 0 insertions, 3 deletions
diff --git a/checker/typeops.mli b/checker/typeops.mli
index 2be461b05..d9f2915a3 100644
--- a/checker/typeops.mli
+++ b/checker/typeops.mli
@@ -18,6 +18,3 @@ val infer_type : env -> constr -> sorts
val check_ctxt : env -> rel_context -> env
val check_polymorphic_arity :
env -> rel_context -> template_arity -> unit
-
-val type_of_constant_type : env -> constant_type -> constr
-