diff options
| author | Gaëtan Gilbert | 2018-10-30 18:07:49 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-10-30 21:47:36 +0100 |
| commit | 9a99bad924f3c82107a5ecfa7a906988f0f69309 (patch) | |
| tree | 53aa873fec4c075ffb8a1134ab466ba2d24764e9 /kernel | |
| parent | a492288930a3f804ad05def938dd572ccf680a66 (diff) | |
Check univ instances in Typing.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/typeops.ml | 3 | ||||
| -rw-r--r-- | kernel/typeops.mli | 3 |
2 files changed, 4 insertions, 2 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 diff --git a/kernel/typeops.mli b/kernel/typeops.mli index d24002065b..4193324136 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -116,4 +116,5 @@ val constr_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t (** {6 Miscellaneous. } *) (** Check that hyps are included in env and fails with error otherwise *) -val check_hyps_inclusion : env -> ('a -> constr) -> 'a -> Constr.named_context -> unit +val check_hyps_inclusion : env -> ?evars:((existential->constr option) * UGraph.t) -> + ('a -> constr) -> 'a -> Constr.named_context -> unit |