aboutsummaryrefslogtreecommitdiff
path: root/kernel/typeops.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/typeops.mli')
-rw-r--r--kernel/typeops.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index ae816fe26e..f88bc653de 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -111,7 +111,7 @@ val type_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t
(** Check that hyps are included in env and fails with error otherwise *)
val check_hyps_inclusion : env -> ?evars:((existential->constr option) * UGraph.t) ->
- ('a -> constr) -> 'a -> Constr.named_context -> unit
+ GlobRef.t -> Constr.named_context -> unit
val check_primitive_type : env -> CPrimitives.op_or_type -> types -> unit