Merge PR #6496: Generate typed generic code from ltac macros

2 files changed, 10 insertions, 6 deletions

diff --git a/lib/genarg.ml b/lib/genarg.ml
index cf3a2bee7..209d1b271 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -174,19 +174,22 @@ sig
   val default : ('raw, 'glb, 'top) genarg_type -> ('raw, 'glb, 'top) obj option
 end
 
+let get_arg_tag = function
+| ExtraArg s -> s
+| _ -> assert false
+
 module Register (M : GenObj) =
 struct
   module GenMap = ArgMap(struct type ('r, 'g, 't) t = ('r, 'g, 't) M.obj end)
   let arg0_map = ref GenMap.empty
 
-  let register0 arg f = match arg with
-  | ExtraArg s ->
+  let register0 arg f =
+    let s = get_arg_tag arg in
     if GenMap.mem s !arg0_map then
       let msg = str M.name ++ str " function already registered: " ++ str (ArgT.repr s) ++ str "." in
       CErrors.anomaly msg
     else
       arg0_map := GenMap.add s (GenMap.Pack f) !arg0_map
-  | _ -> assert false
 
   let get_obj0 name =
     try
@@ -199,8 +202,6 @@ struct
 
   (** For now, the following function is quite dummy and should only be applied
       to an extra argument type, otherwise, it will badly fail. *)
-  let obj t = match t with
-  | ExtraArg s -> get_obj0 s
-  | _ -> assert false
+  let obj t = get_obj0 @@ get_arg_tag t
 
 end
diff --git a/lib/genarg.mli b/lib/genarg.mli
index d49cb334a..bb85f99e3 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -159,6 +159,9 @@ val unquote : ('a, 'co) abstract_argument_type -> argument_type
 
   This is boilerplate code used here and there in the code of Coq. *)
 
+val get_arg_tag : ('a, 'b, 'c) genarg_type -> ('a, 'b, 'c) ArgT.tag
+(** Works only on base objects (ExtraArg), otherwise fails badly. *)
+
 module type GenObj =
 sig
   type ('raw, 'glb, 'top) obj