diff options
Diffstat (limited to 'kernel/typeops.ml')
| -rw-r--r-- | kernel/typeops.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 1bb2d3c79c..c8fd83c8a9 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -91,7 +91,8 @@ let type_of_variable env id = (* Checks if a context of variables can be instantiated by the variables of the current env. Order does not have to be checked assuming that all names are distinct *) -let check_hyps_inclusion env f c sign = +let check_hyps_inclusion env ?evars f c sign = + let conv env a b = conv env ?evars a b in Context.Named.fold_outside (fun d1 () -> let open Context.Named.Declaration in |