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/ltac')

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


From 3c2331a4a9d8c5d5f27c90185c616fe3400d4f1f Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Fri, 6 Apr 2018 16:36:09 +0200
Subject: Extraargs: avoid two token declarations to appear in all .vo

 Without this, the library segment of all .vo except Notations.vo starts
 with two TOKEN objects (declaration of tokens "->" and "<-").
 This is due to side effects creating these objects during the dynlink
 of ltac_plugin.cmxs, more precisely the two Metasyntax.add_token_obj in
 Extraargs. It's quite cleaner to register these two side effects via
 Mltop.declare_cache_obj, so that the two objects only live in
 Notations.vo, and are loaded from there.
---
 plugins/ltac/extraargs.ml4 | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index dbbdbfa396..d779951180 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -52,8 +52,11 @@ let () =
 
 (* Rewriting orientation *)
 
-let _ = Metasyntax.add_token_obj "<-"
-let _ = Metasyntax.add_token_obj "->"
+let _ =
+  Mltop.declare_cache_obj
+    (fun () -> Metasyntax.add_token_obj "<-";
+               Metasyntax.add_token_obj "->")
+    "ltac_plugin"
 
 let pr_orient _prc _prlc _prt = function
   | true -> Pp.mt ()
-- 
cgit v1.2.3