From e1d4ad82b1557a8cf808e0374ece9c39ed349ea2 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 10 Jul 2017 23:33:42 +0200
Subject: 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.
---
 kernel/uGraph.mli | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'kernel/uGraph.mli')

diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index 935a3cab4a..4de373eb4c 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
-- 
cgit v1.2.3