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/extraargs.ml4')

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