From 2815d5841e98cd288921c364ca5b7bf36ca7bcfe Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Fri, 7 Nov 2014 18:53:22 +0100
Subject: Proper printer for [uconstr] in [Pptactic].

This particular instance is probably never called though.
---
 printing/pptactic.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 023335e6ae..46aad3bc2b 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -1347,7 +1347,7 @@ module Make
       let pr = {
         pr_tactic = pr_glob_tactic_level env;
         pr_constr = pr_constr_env env Evd.empty;
-        pr_uconstr = (fun _ -> mt ()); (* arnaud: todo *)
+        pr_uconstr = pr_closed_glob_env env Evd.empty;
         pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env);
         pr_lconstr = pr_lconstr_env env Evd.empty;
         pr_pattern = pr_pat_and_constr_expr (pr_glob_constr_env env);
-- 
cgit v1.2.3