From 264c208a5eb824c880ef4c46e060185470064df5 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 19 Jul 2018 11:41:48 +0200
Subject: Higher-level libobject API for objects with fixed scopes

---
 vernac/metasyntax.ml | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

(limited to 'vernac')

diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index dccd776fa8..790b62c9d0 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -33,11 +33,9 @@ open Nameops
 let cache_token (_,s) = CLexer.add_keyword s
 
 let inToken : string -> obj =
-  declare_object {(default_object "TOKEN") with
-       open_function = (fun i o -> if Int.equal i 1 then cache_token o);
-       cache_function = cache_token;
-       subst_function = Libobject.ident_subst_function;
-       classify_function = (fun o -> Substitute o)}
+  declare_object @@ global_object_nodischarge "TOKEN"
+    ~cache:cache_token
+    ~subst:(Some Libobject.ident_subst_function)
 
 let add_token_obj s = Lib.add_anonymous_leaf (inToken s)
 
-- 
cgit v1.2.3