From 0ae66237261b9810976eb2614dfda8e293e4b9ea Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Thu, 25 Jun 2015 14:55:07 +0200
Subject: Remove useless `and_short_name` in interpreted level in `Tacexpr`.

---
 printing/pptactic.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'printing')

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index b8ad996aa3..1502884be7 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -1382,7 +1382,7 @@ module Make
         pr_lconstr = pr_lconstr_env env Evd.empty;
         pr_pattern = pr_pat_and_constr_expr (pr_glob_constr_env env);
         pr_lpattern = pr_pat_and_constr_expr (pr_lglob_constr_env env);
-        pr_constant = pr_and_short_name (pr_evaluable_reference_env env);
+        pr_constant = pr_evaluable_reference_env env;
         pr_reference = pr_located pr_ltac_constant;
         pr_name = pr_id;
         pr_generic = Genprint.generic_top_print;
-- 
cgit v1.2.3