diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 780a62422a02..9dd4614d19b7 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2585,6 +2585,35 @@ let appexpl self genv env lvar ?loc ((ref,us), args) =
   if args = [] then DAst.make ?loc @@ GApp (f,[])
   else apply_args self genv env lvar loc f (List.map fst args)
 
+let genarg_gen self genv env lvar ?loc gen =
+  let (ltacvars, ntnvars) = lvar in
+  (* Preventively declare notation variables in ltac as non-bindings *)
+  Id.Map.iter (fun x status -> status.Genintern.ntnvar_used_as_binder <- false) ntnvars;
+  let extra = ltacvars.ltac_extra in
+  (* We inform ltac that the interning vars and the notation vars are bound *)
+  (* but we could instead rely on the "intern_sign" *)
+  let lvars = Id.Set.union ltacvars.ltac_bound ltacvars.ltac_vars in
+  let lvars = Id.Set.union lvars (Id.Map.domain ntnvars) in
+  let ltacvars = Id.Set.union lvars env.ids in
+  (* Propagating enough information for mutual interning with tac-in-term *)
+  let intern_sign = {
+    Genintern.intern_ids = env.ids;
+    Genintern.intern_univs = env.local_univs.bound;
+    Genintern.notation_variable_status = ntnvars
+  } in
+  let ist = {
+    Genintern.genv;
+    ltacvars;
+    extra;
+    intern_sign;
+    strict_check = match env.strict_check with None -> false | Some b -> b;
+  } in
+  let intern = if env.pattern_mode
+    then Genintern.generic_intern_pat
+    else Genintern.generic_intern_constr
+  in
+  intern ?loc ist gen
+
 let app self genv env lvar ?loc (f, args) =
   let intern env = intern self genv env lvar in
   let apply_impargs env = apply_impargs self genv env lvar in
@@ -2600,6 +2629,13 @@ let app self genv env lvar ?loc (f, args) =
   | CNotation (_,ntn,ntnargs) ->
     let c = intern_notation intern env (snd lvar) loc ntn ntnargs in
     apply_impargs env loc c args
+  | CGenarg gen ->
+    let f, info = genarg_gen self genv env lvar ?loc:f.loc gen in
+    if info.passthrough_impls then
+      apply_impargs env loc f args
+    else
+      let args = extract_regular_arguments args in
+      apply_args env loc f args
   | _ ->
     let f = intern_no_implicit self genv env lvar f in
     let args = extract_regular_arguments args in
@@ -2746,35 +2782,10 @@ let hole self genv env lvar ?loc k =
   GHole k
 
 let genarg self genv env lvar ?loc gen =
-  let (ltacvars, ntnvars) = lvar in
-  (* Preventively declare notation variables in ltac as non-bindings *)
-  Id.Map.iter (fun x status -> status.Genintern.ntnvar_used_as_binder <- false) ntnvars;
-  let extra = ltacvars.ltac_extra in
-  (* We inform ltac that the interning vars and the notation vars are bound *)
-  (* but we could instead rely on the "intern_sign" *)
-  let lvars = Id.Set.union ltacvars.ltac_bound ltacvars.ltac_vars in
-  let lvars = Id.Set.union lvars (Id.Map.domain ntnvars) in
-  let ltacvars = Id.Set.union lvars env.ids in
-  (* Propagating enough information for mutual interning with tac-in-term *)
-  let intern_sign = {
-    Genintern.intern_ids = env.ids;
-    Genintern.intern_univs = env.local_univs.bound;
-    Genintern.notation_variable_status = ntnvars
-  } in
-  let ist = {
-    Genintern.genv;
-    ltacvars;
-    extra;
-    intern_sign;
-    strict_check = match env.strict_check with None -> false | Some b -> b;
-  } in
-  let intern = if env.pattern_mode
-    then Genintern.generic_intern_pat
-    else Genintern.generic_intern_constr
-  in
-  let glb = intern ?loc ist gen in
-  DAst.make ?loc @@
-  GGenarg glb
+  let c, info = genarg_gen self genv env lvar ?loc gen in
+  if info.passthrough_impls then
+    apply_impargs self genv env lvar loc c []
+  else c
 
 let genargglob self genv env lvar ?loc gen =
   DAst.make ?loc @@ GGenarg gen
diff --git a/interp/genintern.ml b/interp/genintern.ml
index 3fbd948b0f3f..42b98460b901 100644
--- a/interp/genintern.ml
+++ b/interp/genintern.ml
@@ -67,8 +67,18 @@ end
 
 type ('raw, 'glb) constr_intern_fun = ?loc:Loc.t -> glob_sign -> 'raw -> 'glb
 
+type constr_intern_info = { passthrough_impls : bool }
+
+let default_info = { passthrough_impls = false }
+
+let wrap_constr_intern (type raw glb) (tag:(raw,glb) GenConstr.tag) (f:(raw, glb) constr_intern_fun)
+  : (raw, Glob_term.glob_constr * constr_intern_info) constr_intern_fun =
+  fun ?loc ist v ->
+  let v = f ?loc ist v in
+  DAst.make ?loc @@ Glob_term.GGenarg (Glb (tag, v)), default_info
+
 module CInternObj = struct
-  type ('r, 'g) t = ('r, 'g) constr_intern_fun
+  type ('r, _) t = ('r, Glob_term.glob_constr * constr_intern_info) constr_intern_fun
 end
 
 module NtnSubstObj =
@@ -82,7 +92,9 @@ module NtnSubst = GenConstr.Register (NtnSubstObj)
 
 let intern = Intern.obj
 let register_intern0 = Intern.register0
-let register_intern_constr = CIntern.register
+let register_intern_constr_gen = CIntern.register
+let register_intern_constr tag f =
+  register_intern_constr_gen tag (wrap_constr_intern tag f)
 
 let generic_intern ist (GenArg (Rawwit wit, v)) =
   let (ist, v) = intern wit ist v in
@@ -90,15 +102,16 @@ let generic_intern ist (GenArg (Rawwit wit, v)) =
 
 let generic_intern_constr ?loc ist (GenConstr.Raw (tag, v)) =
   let internf = CIntern.get tag in
-  GenConstr.Glb (tag, internf ?loc ist v)
+  internf ?loc ist v
 
 module InternPatObj = struct
-  type ('raw, 'glb) t = ('raw, 'glb) constr_intern_fun
+  type ('raw, _) t = ('raw, Glob_term.glob_constr * constr_intern_info) constr_intern_fun
 end
 
 module InternPat = GenConstr.Register (InternPatObj)
 
-let register_intern_pat = InternPat.register
+let register_intern_pat_gen = InternPat.register
+let register_intern_pat tag f = register_intern_pat_gen tag (wrap_constr_intern tag f)
 
 let generic_intern_pat ?loc ist (GenConstr.Raw (tag, v)) =
   match InternPat.find_opt tag with
@@ -107,7 +120,7 @@ let generic_intern_pat ?loc ist (GenConstr.Raw (tag, v)) =
     CErrors.user_err ?loc Pp.(str "This quotation is not supported in tactic patterns (" ++ str name ++ str ").")
   | Some internf ->
     let v = internf ?loc ist v in
-    GenConstr.Glb (tag, v)
+    v
 
 (** Notation substitution *)
 
diff --git a/interp/genintern.mli b/interp/genintern.mli
index 8f0f4d0f4a5a..1d72ba421e6a 100644
--- a/interp/genintern.mli
+++ b/interp/genintern.mli
@@ -51,15 +51,17 @@ type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb
 
 type ('raw, 'glb) constr_intern_fun = ?loc:Loc.t -> glob_sign -> 'raw -> 'glb
 
+type constr_intern_info = { passthrough_impls : bool }
+
 val intern : ('raw, 'glb, 'top) genarg_type -> ('raw, 'glb) intern_fun
 
 val generic_intern : (raw_generic_argument, glob_generic_argument) intern_fun
 
-val generic_intern_constr : (GenConstr.raw, GenConstr.glb) constr_intern_fun
+val generic_intern_constr : (GenConstr.raw, Glob_term.glob_constr * constr_intern_info) constr_intern_fun
 
 (** {5 Internalization in tactic patterns} *)
 
-val generic_intern_pat : (GenConstr.raw, GenConstr.glb) constr_intern_fun
+val generic_intern_pat : (GenConstr.raw, Glob_term.glob_constr * constr_intern_info) constr_intern_fun
 
 (** {5 Notation functions} *)
 
@@ -83,6 +85,12 @@ val register_intern_constr : ('raw, 'glb) GenConstr.tag ->
 val register_intern_pat : ('raw, 'glb) GenConstr.tag ->
   ('raw, 'glb) constr_intern_fun -> unit
 
+val register_intern_constr_gen : ('raw, Util.Empty.t) GenConstr.tag ->
+  ('raw, Glob_term.glob_constr * constr_intern_info) constr_intern_fun -> unit
+
+val register_intern_pat_gen : ('raw, Util.Empty.t) GenConstr.tag ->
+  ('raw, Glob_term.glob_constr * constr_intern_info) constr_intern_fun -> unit
+
 val register_ntn_subst0 : (_, 'glb) GenConstr.tag -> 'glb ntn_subst_fun -> unit
 
 (** Used to compute the set of used notation variables during internalization.*)