From e1d4ad82b1557a8cf808e0374ece9c39ed349ea2 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
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/univ.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'kernel/univ.ml')

diff --git a/kernel/univ.ml b/kernel/univ.ml
index cb19761b3..6614d6027 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1060,6 +1060,9 @@ module AUContext =
 struct
   include UContext
 
+  let repr (inst, cst) =
+    (Array.mapi (fun i l -> Level.var i) inst, cst)
+
   let instantiate inst (u, cst) =
     assert (Array.length u = Array.length inst);
     subst_instance_constraints inst cst
-- 
cgit v1.2.3