diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-10 23:33:42 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-11 14:50:47 +0200 |
| commit | e1d4ad82b1557a8cf808e0374ece9c39ed349ea2 (patch) | |
| tree | 6539da95794f0029d90e60460c1aaca9b8ddafeb /kernel/uGraph.mli | |
| parent | 012f5fb722a9d5dcef82c800aa54ed50c0a58957 (diff) | |
Cleaning up the implementation of module subtyping in the kernel.
We export a function in UGraph to check that a polymorphic instance is
a subtype of another, instead of rolling up our own in module code.
We also add a few tests for module subtyping in presence of polymorphic
constants.
Diffstat (limited to 'kernel/uGraph.mli')
| -rw-r--r-- | kernel/uGraph.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index 935a3cab4..4de373eb4 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -53,6 +53,10 @@ val check_constraints : constraints -> universes -> bool val check_eq_instances : Instance.t check_function (** Check equality of instances w.r.t. a universe graph *) +val check_subtype : AUContext.t check_function +(** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of + [ctx1]. *) + (** {6 Pretty-printing of universes. } *) val pr_universes : (Level.t -> Pp.std_ppcmds) -> universes -> Pp.std_ppcmds |