Remove Global.env from goptions by passing from vernacentries

Currently this env is only used to error for Printing If/Let on
non-2-constructor/non-1-constructor types so we could alternatively
remove it and not error / error later when trying to print.
Keeping the env and the error as-is should be fine though.

3 files changed, 33 insertions, 37 deletions

diff --git a/library/goptions.ml b/library/goptions.ml
index b9c1802a72..f4b8ce9465 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -42,13 +42,12 @@ let error_undeclared_key key =
 (****************************************************************************)
 (* 1- Tables                                                                *)
 
-class type ['a] table_of_A =
-object
-  method add : 'a -> unit
-  method remove : 'a -> unit
-  method mem : 'a -> unit
-  method print : unit
-end
+type 'a table_of_A =  {
+  add : Environ.env -> 'a -> unit;
+  remove : Environ.env -> 'a -> unit;
+  mem : Environ.env -> 'a -> unit;
+  print : unit -> unit;
+}
 
 module MakeTable =
   functor
@@ -109,18 +108,17 @@ module MakeTable =
 		 (fun a b -> spc () ++ printer a ++ b)
 		 table (mt ()) ++ str "." ++ fnl ())))
 
-    class table_of_A () =
-    object
-      method add x = add_option (A.encode (Global.env()) x)
-      method remove x = remove_option (A.encode (Global.env()) x)
-      method mem x =
-        let y = A.encode (Global.env()) x in
+    let table_of_A = {
+       add = (fun env x -> add_option (A.encode env x));
+       remove = (fun env x -> remove_option (A.encode env x));
+       mem = (fun env x ->
+        let y = A.encode env x in
         let answer = MySet.mem y !t in
-        Feedback.msg_info (A.member_message y answer)
-      method print = print_table A.title A.printer !t
-    end
+        Feedback.msg_info (A.member_message y answer));
+       print = (fun () -> print_table A.title A.printer !t);
+     }
 
-    let _ = A.table := (nick,new table_of_A ())::!A.table
+    let _ = A.table := (nick, table_of_A)::!A.table
     let active c = MySet.mem c !t
     let elements () = MySet.elements !t
   end
diff --git a/library/goptions.mli b/library/goptions.mli
index 2e593e9d9e..381ba4d34a 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -76,7 +76,7 @@ end
 
 (** The functor [MakeRefTable] declares a new table of objects of type
    [A.t] practically denoted by [reference]; the encoding function
-   [encode : reference -> A.t] is typically a globalization function,
+   [encode : env -> reference -> A.t] is typically a globalization function,
    possibly with some restriction checks; the function
    [member_message] say what to print when invoking the "Test Toto
    Titi foo." command; at the end [title] is the table name printed
@@ -139,19 +139,17 @@ val declare_bool_option_and_ref : depr:bool -> name:string -> key:option_name ->
 
 module OptionMap : CSig.MapS with type key = option_name
 
-val get_string_table :
-  option_name ->
-    < add : string -> unit;
-      remove : string -> unit;
-      mem : string -> unit;
-      print : unit >
+type 'a table_of_A =  {
+  add : Environ.env -> 'a -> unit;
+  remove : Environ.env -> 'a -> unit;
+  mem : Environ.env -> 'a -> unit;
+  print : unit -> unit;
+}
 
+val get_string_table :
+  option_name -> string table_of_A
 val get_ref_table :
-  option_name ->
-    < add : qualid -> unit;
-      remove : qualid -> unit;
-      mem : qualid -> unit;
-      print : unit >
+  option_name -> qualid table_of_A
 
 (** The first argument is a locality flag. *)
 val set_int_option_value_gen    : ?locality:option_locality -> option_name -> int option -> unit
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index e44d68b87d..fa170e4104 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1732,29 +1732,29 @@ let vernac_set_option ~local export table v = match v with
 
 let vernac_add_option key lv =
   let f = function
-    | StringRefValue s -> (get_string_table key)#add s
-    | QualidRefValue locqid -> (get_ref_table key)#add locqid
+    | StringRefValue s -> (get_string_table key).add (Global.env()) s
+    | QualidRefValue locqid -> (get_ref_table key).add (Global.env()) locqid
   in
   try List.iter f lv with Not_found -> error_undeclared_key key
 
 let vernac_remove_option key lv =
   let f = function
-  | StringRefValue s -> (get_string_table key)#remove s
-  | QualidRefValue locqid -> (get_ref_table key)#remove locqid
+  | StringRefValue s -> (get_string_table key).remove (Global.env()) s
+  | QualidRefValue locqid -> (get_ref_table key).remove (Global.env()) locqid
   in
   try List.iter f lv with Not_found -> error_undeclared_key key
 
 let vernac_mem_option key lv =
   let f = function
-  | StringRefValue s -> (get_string_table key)#mem s
-  | QualidRefValue locqid -> (get_ref_table key)#mem locqid
+  | StringRefValue s -> (get_string_table key).mem (Global.env()) s
+  | QualidRefValue locqid -> (get_ref_table key).mem (Global.env()) locqid
   in
   try List.iter f lv with Not_found -> error_undeclared_key key
 
 let vernac_print_option key =
-  try (get_ref_table key)#print
+  try (get_ref_table key).print ()
   with Not_found ->
-  try (get_string_table key)#print
+  try (get_string_table key).print ()
   with Not_found ->
   try print_option_value key
   with Not_found -> error_undeclared_key key