aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/typeops.mli
diff options
context:
space:
mode:
Diffstat (limited to 'checker/typeops.mli')
-rw-r--r--checker/typeops.mli6
1 files changed, 3 insertions, 3 deletions
diff --git a/checker/typeops.mli b/checker/typeops.mli
index 92535606f..97d79fe54 100644
--- a/checker/typeops.mli
+++ b/checker/typeops.mli
@@ -16,8 +16,8 @@ open Environ
val infer : env -> constr -> constr
val infer_type : env -> constr -> sorts
val check_ctxt : env -> rel_context -> env
-val check_polymorphic_arity :
- env -> rel_context -> polymorphic_arity -> unit
+(* val check_polymorphic_arity : *)
+(* env -> rel_context -> polymorphic_arity -> unit *)
-val type_of_constant_type : env -> constant_type -> constr
+val type_of_constant_type : env -> constr -> constr