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 97d79fe54..32920b02f 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 -> template_arity -> unit
-val type_of_constant_type : env -> constr -> constr
+val type_of_constant_type : env -> constant_type -> constr