From fc2476e4a29592dcf2860a16d3a7c0aeeb4bffac Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Fri, 7 Nov 2014 18:38:12 +0100
Subject: Printing function for [uconstr].

The core is a "detyping" function for [closed_glob_constr]. Which interpretes the variable names according to the Ltac context, and apply the standard detyping procedure to typed terms in the closure.
---
 printing/printer.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'printing/printer.mli')

diff --git a/printing/printer.mli b/printing/printer.mli
index 315bf6810d..baa81c9fe4 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -59,6 +59,8 @@ val pr_ltype               : types -> std_ppcmds
 val pr_type_env            : env -> evar_map -> types -> std_ppcmds
 val pr_type                : types -> std_ppcmds
 
+val pr_closed_glob_env     : env -> evar_map -> closed_glob_constr -> std_ppcmds
+
 val pr_ljudge_env          : env -> evar_map -> unsafe_judgment -> std_ppcmds * std_ppcmds
 val pr_ljudge              : unsafe_judgment -> std_ppcmds * std_ppcmds
 
-- 
cgit v1.2.3