Add "options" import category

coq · Jan 23, 2024 · 32e1fdb · 32e1fdb
1 parent e012009
commit 32e1fdb
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 2 deletions.
diff --git 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
@@ -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;