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.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'printing/printer.ml')

diff --git a/printing/printer.ml b/printing/printer.ml
index af81e192d1..0fea782974 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -122,6 +122,9 @@ let pr_glob_constr c =
   let (sigma, env) = get_current_context () in
   pr_glob_constr_env env c
 
+let pr_closed_glob_env env sigma c =
+  pr_constr_expr (extern_closed_glob false env sigma c)
+
 let pr_lconstr_pattern_env env sigma c =
   pr_lconstr_pattern_expr (extern_constr_pattern (Termops.names_of_rel_context env) sigma c)
 let pr_constr_pattern_env env sigma c =
-- 
cgit v1.2.3