aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/typeops.mli
diff options
context:
space:
mode:
Diffstat (limited to 'checker/typeops.mli')
-rw-r--r--checker/typeops.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/typeops.mli b/checker/typeops.mli
index 5e71ec77f..3c56c15ef 100644
--- a/checker/typeops.mli
+++ b/checker/typeops.mli
@@ -9,6 +9,7 @@
(*i*)
open Names
open Cic
+open Term
open Environ
(*i*)
@@ -17,7 +18,6 @@ open Environ
val infer : env -> constr -> constr
val infer_type : env -> constr -> sorts
val check_ctxt : env -> rel_context -> env
-val check_named_ctxt : env -> named_context -> env
val check_polymorphic_arity :
env -> rel_context -> polymorphic_arity -> unit