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.

1 files changed, 8 insertions, 8 deletions

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