Proper printer for [uconstr] in [Pptactic].

This particular instance is probably never called though.

1 files changed, 1 insertions, 1 deletions

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);