From 32e1fdbf4fc2c612d461ee494012e3328b874766 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Tue, 23 Jan 2024 14:36:42 +0100 Subject: [PATCH] Add "options" import category --- doc/sphinx/language/core/modules.rst | 2 ++ library/goptions.ml | 6 ++++-- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/doc/sphinx/language/core/modules.rst b/doc/sphinx/language/core/modules.rst index f5245b76b513b..341219dd3ca3b 100644 --- a/doc/sphinx/language/core/modules.rst +++ b/doc/sphinx/language/core/modules.rst @@ -301,6 +301,8 @@ are now available through the dot notation. :cmd:`Reserved Notation`), scope controls (:cmd:`Delimit Scope`, :cmd:`Bind Scope`, :cmd:`Open Scope`) but not :ref:`Abbreviations`. + - ``options`` for :ref:`flags-options-tables` + - ``ltac.notations`` corresponding to :cmd:`Tactic Notation`. - ``ltac2.notations`` corresponding to :cmd:`Ltac2 Notation` diff --git a/library/goptions.ml b/library/goptions.ml index 1907de48a288c..452f7c71679ab 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -55,6 +55,8 @@ type 'a table_of_A = { print : unit -> unit; } +let opts_cat = Libobject.create_category "options" + module MakeTable = functor (A : sig @@ -100,7 +102,7 @@ module MakeTable = Libobject.declare_object {(Libobject.default_object nick) with Libobject.object_stage = Summary.Stage.Synterp; Libobject.load_function = load_options; - Libobject.open_function = Libobject.simple_open load_options; + Libobject.open_function = Libobject.simple_open ~cat:opts_cat load_options; Libobject.cache_function = cache_options; Libobject.subst_function = subst_options; Libobject.classify_function = (fun x -> Substitute)} @@ -295,7 +297,7 @@ let declare_option cast uncast append ?(preprocess = fun x -> x) { (default_object (nickname key)) with object_stage = stage; load_function = load_options; - open_function = simple_open open_options; + open_function = simple_open ~cat:opts_cat open_options; cache_function = cache_options; subst_function = subst_options; discharge_function = discharge_options;