diff options
Diffstat (limited to 'vernac/metasyntax.ml')
| -rw-r--r-- | vernac/metasyntax.ml | 8 |
1 files changed, 3 insertions, 5 deletions
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) |