diff options
| author | Pierre-Marie Pédrot | 2018-11-05 13:19:54 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-05 13:19:54 +0100 |
| commit | 5202b20739d18137780b7729ee657b7eecef5c0c (patch) | |
| tree | dedf81cdb23cc530db04a6bfe1a42528397afdb3 /kernel/typeops.mli | |
| parent | 538a54e8855d477e9ca350a76f852a147809a06b (diff) | |
| parent | f18ea56a697fe27467e499d35495e18b866de371 (diff) | |
Merge PR #8866: Check universe instances in Typing
Diffstat (limited to 'kernel/typeops.mli')
| -rw-r--r-- | kernel/typeops.mli | 3 |
1 files changed, 2 insertions, 1 deletions
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 |