From ce9058b597fc53310619d537aadacc091755ed39 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 18 Aug 2016 13:15:42 +0200
Subject: Fix bug #4939: LtacProf prints tactic notations weirdly.

---
 ltac/profile_ltac.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml
index f332e1a0d5..bea02e3dcb 100644
--- a/ltac/profile_ltac.ml
+++ b/ltac/profile_ltac.ml
@@ -139,7 +139,7 @@ let string_of_call ck =
   let s =
   string_of_ppcmds
     (match ck with
-       | Tacexpr.LtacNotationCall s -> Names.KerName.print s
+       | Tacexpr.LtacNotationCall s -> Pptactic.pr_alias_key s
        | Tacexpr.LtacNameCall cst -> Pptactic.pr_ltac_constant cst
        | Tacexpr.LtacVarCall (id, t) -> Nameops.pr_id id
        | Tacexpr.LtacAtomCall te ->
-- 
cgit v1.2.3