From b6feaafc7602917a8ef86fb8adc9651ff765e710 Mon Sep 17 00:00:00 2001
From: Matej Košík <matej.kosik@inria.fr>
Date: Mon, 29 May 2017 11:02:06 +0200
Subject: Remove (useless) aliases from the API.

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

(limited to 'plugins/ltac/profile_ltac.ml')

diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index 0fbb9df2d..020b3048f 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -247,7 +247,7 @@ let string_of_call ck =
     (match ck with
        | 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.LtacVarCall (id, t) -> Names.Id.print id
        | Tacexpr.LtacAtomCall te ->
          (Pptactic.pr_glob_tactic (Global.env ())
             (Tacexpr.TacAtom (Loc.tag te)))
-- 
cgit v1.2.3