From 51cc164e858433961acc166e83e69880700a89f1 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 20 Apr 2020 13:33:20 +0200
Subject: Use polymorphic record for Vernacentries.iter_table

---
 vernac/vernacentries.ml | 22 ++++++++--------------
 1 file changed, 8 insertions(+), 14 deletions(-)

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index a6a38e5253..07a9272336 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1554,34 +1554,28 @@ let vernac_set_option ~locality table v = match v with
       vernac_set_option0 ~locality table v
 | _ -> vernac_set_option0 ~locality table v
 
-(* We have to request twice the same polymorphic function as argument
-   because OCaml won't compute the same type for it in both cases. *)
-let iter_table ~f ~g key lv =
+type iter_table_aux = { aux : 'a. 'a Goptions.table_of_A -> Environ.env -> 'a -> unit }
+
+let iter_table f key lv =
   let aux = function
     | StringRefValue s ->
        begin
-         try f (get_string_table key) (Global.env()) s
+         try f.aux (get_string_table key) (Global.env()) s
          with Not_found -> error_no_table_of_this_type ~kind:"string" key
        end
     | QualidRefValue locqid ->
        begin
-         try g (get_ref_table key) (Global.env()) locqid
+         try f.aux (get_ref_table key) (Global.env()) locqid
          with Not_found -> error_no_table_of_this_type ~kind:"qualid" key
        end
   in
   List.iter aux lv
 
-let vernac_add_option =
-  let aux table = table.add in
-  iter_table ~f:aux ~g:aux
+let vernac_add_option = iter_table { aux = fun table -> table.add }
 
-let vernac_remove_option =
-  let aux table = table.remove in
-  iter_table ~f:aux ~g:aux
+let vernac_remove_option = iter_table { aux = fun table -> table.remove }
 
-let vernac_mem_option =
-  let aux table = table.mem in
-  iter_table ~f:aux ~g:aux
+let vernac_mem_option = iter_table { aux = fun table -> table.mem }
 
 let vernac_print_option key =
   try (get_ref_table key).print ()
-- 
cgit v1.2.3