From ad8c2b7dab1b0759d1c304350523d6d2cc9c7b24 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 28 Dec 2020 22:02:22 +0100
Subject: Register a printer for fconstr substitutions in the kernel.

---
 dev/top_printers.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'dev/top_printers.mli')

diff --git a/dev/top_printers.mli b/dev/top_printers.mli
index 50495dc0a4..e8ed6c709e 100644
--- a/dev/top_printers.mli
+++ b/dev/top_printers.mli
@@ -52,6 +52,7 @@ val ppconstr_expr : Constrexpr.constr_expr -> unit
 val ppglob_constr : 'a Glob_term.glob_constr_g -> unit
 val pppattern : Pattern.constr_pattern -> unit
 val ppfconstr : CClosure.fconstr -> unit
+val ppfsubst : CClosure.fconstr Esubst.subs -> unit
 
 val ppnumtokunsigned : NumTok.Unsigned.t -> unit
 val ppnumtokunsignednat : NumTok.UnsignedNat.t -> unit
-- 
cgit v1.2.3