From d6ca9b2f71bced8711b184400fa7e80061497fd7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Mon, 12 Feb 2018 14:46:05 +0100
Subject: Adding a sanity check on inductive variance subtyping.

---
 kernel/univ.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'kernel/univ.mli')

diff --git a/kernel/univ.mli b/kernel/univ.mli
index c45ebe21c..74d1bfd3a 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -253,6 +253,9 @@ sig
      A'] as opposed to [A' <= A]. *)
   type t = Irrelevant | Covariant | Invariant
 
+  (** [check_subtype x y] holds if variance [y] is also an instance of [x] *)
+  val check_subtype : t -> t -> bool
+
   val sup : t -> t -> t
 
   val pr : t -> Pp.t
-- 
cgit v1.2.3