From 5df8f2ed3d9cf8d7903568308d8ce2e8e6dd4720 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Fri, 6 Apr 2018 14:38:02 +0200
Subject: Tacenv: minor code cleanup

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

(limited to 'plugins')

diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml
index 0bb9ccb1d8..1f2c722b34 100644
--- a/plugins/ltac/tacenv.ml
+++ b/plugins/ltac/tacenv.ml
@@ -144,7 +144,7 @@ let add ~deprecation kn b t =
   mactab := KNmap.add kn entry !mactab
 
 let replace kn path t =
-  let (path, _, _) = KerName.repr path in
+  let path = KerName.modpath path in
   let entry _ e = { e with tac_body = t; tac_redef = path :: e.tac_redef } in
   mactab := KNmap.modify kn entry !mactab
 
-- 
cgit v1.2.3