From 0f3c1f242ec824a5772c47de61a6cddebe2ee8c8 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 20 Nov 2018 14:42:05 +0100
Subject: checker: check inductive types by roundtrip through the kernel.

---
 kernel/univ.ml  | 2 ++
 kernel/univ.mli | 1 +
 2 files changed, 3 insertions(+)

(limited to 'kernel')

diff --git a/kernel/univ.ml b/kernel/univ.ml
index 93a91af1d7..d7c0cf13ec 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1034,6 +1034,8 @@ module ACumulativityInfo =
 struct
   type t = AUContext.t * Variance.t array
 
+  let repr (auctx,var) = AUContext.repr auctx, var
+
   let pr prl (univs, variance) =
     AUContext.pr prl ~variance univs
 
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 8327ff1644..d7097be570 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -400,6 +400,7 @@ module ACumulativityInfo :
 sig
   type t
 
+  val repr : t -> CumulativityInfo.t
   val univ_context : t -> AUContext.t
   val variance : t -> Variance.t array
   val leq_constraints : t -> Instance.t constraint_function
-- 
cgit v1.2.3