From 3adfa2c8dc0850501c37201df7952d264135d124 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 28 Dec 2020 16:49:35 +0100
Subject: Export a high-level representation of term substitutions.

---
 kernel/esubst.mli | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'kernel/esubst.mli')

diff --git a/kernel/esubst.mli b/kernel/esubst.mli
index 8ff29ab07a..b0fbe680c3 100644
--- a/kernel/esubst.mli
+++ b/kernel/esubst.mli
@@ -94,3 +94,15 @@ val is_lift_id : lift -> bool
     That is, if Γ ⊢ e : Δ and Δ ⊢ σ : Ξ, then Γ ⊢ lift_subst mk e σ : Ξ.
 *)
 val lift_subst : (lift -> 'a -> 'b) -> lift -> 'a subs -> 'b subs
+
+(** Debugging utilities *)
+module Internal :
+sig
+type 'a or_rel = REL of int | VAL of int * 'a
+
+(** High-level representation of a substitution. The first component is a list
+    that associates a value to an index, and the second component is the
+    relocation shift that must be applied to any variable pointing outside of
+    the substitution. *)
+val repr : 'a subs -> 'a or_rel list * int
+end
-- 
cgit v1.2.3