From 5ee144846a221021b70dd1e8730bc7dbee56ca97 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Fri, 9 Jun 2023 12:05:18 +0200
Subject: [PATCH 1/2] Move genarg substitutions to new pretyping/gensubst

---
 interp/genintern.ml                | 20 --------------
 interp/genintern.mli               | 13 ---------
 interp/notation_ops.ml             |  2 +-
 plugins/ltac/tacentries.ml         |  8 +++---
 plugins/ltac/tacentries.mli        |  2 +-
 plugins/ltac/tacinterp.ml          |  2 +-
 plugins/ltac/tacsubst.ml           | 42 +++++++++++++++---------------
 plugins/ltac2/tac2core.ml          |  6 ++---
 plugins/ltac2/tac2intern.ml        |  8 +++---
 plugins/ssr/ssrparser.mlg          |  2 +-
 plugins/ssrmatching/ssrmatching.ml |  2 +-
 pretyping/detyping.ml              |  4 +--
 pretyping/detyping.mli             |  3 ---
 pretyping/gensubst.ml              | 29 +++++++++++++++++++++
 pretyping/gensubst.mli             | 23 ++++++++++++++++
 tactics/autorewrite.ml             |  2 +-
 tactics/hints.ml                   |  2 +-
 17 files changed, 92 insertions(+), 78 deletions(-)
 create mode 100644 pretyping/gensubst.ml
 create mode 100644 pretyping/gensubst.mli

diff --git a/interp/genintern.ml b/interp/genintern.ml
index 0850ad70c6f4..53ec646f8c86 100644
--- a/interp/genintern.ml
+++ b/interp/genintern.ml
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Names
-open Mod_subst
 open Genarg
 
 module Store = Store.Make ()
@@ -50,7 +49,6 @@ type glob_constr_and_expr = Glob_term.glob_constr * Constrexpr.constr_expr optio
 type glob_constr_pattern_and_expr = Id.Set.t * glob_constr_and_expr * Pattern.constr_pattern
 
 type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb
-type 'glb subst_fun = substitution -> 'glb -> 'glb
 type 'glb ntn_subst_fun = Id.Set.t -> Glob_term.glob_constr Id.Map.t -> 'glb -> 'glb
 
 module InternObj =
@@ -60,13 +58,6 @@ struct
   let default _ = None
 end
 
-module SubstObj =
-struct
-  type ('raw, 'glb, 'top) obj = 'glb subst_fun
-  let name = "subst"
-  let default _ = None
-end
-
 module NtnSubstObj =
 struct
   type ('raw, 'glb, 'top) obj = 'glb ntn_subst_fun
@@ -75,7 +66,6 @@ struct
 end
 
 module Intern = Register (InternObj)
-module Subst = Register (SubstObj)
 module NtnSubst = Register (NtnSubstObj)
 
 let intern = Intern.obj
@@ -85,16 +75,6 @@ let generic_intern ist (GenArg (Rawwit wit, v)) =
   let (ist, v) = intern wit ist v in
   (ist, in_gen (glbwit wit) v)
 
-(** Substitution functions *)
-
-let substitute = Subst.obj
-let register_subst0 = Subst.register0
-
-let generic_substitute subs (GenArg (Glbwit wit, v)) =
-  in_gen (glbwit wit) (substitute wit subs v)
-
-let () = Hook.set Detyping.subst_genarg_hook generic_substitute
-
 (** Notation substitution *)
 
 let substitute_notation = NtnSubst.obj
diff --git a/interp/genintern.mli b/interp/genintern.mli
index 4c831c8f9d37..27ff89c67193 100644
--- a/interp/genintern.mli
+++ b/interp/genintern.mli
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Names
-open Mod_subst
 open Genarg
 
 module Store : Store.S
@@ -47,15 +46,6 @@ val intern : ('raw, 'glb, 'top) genarg_type -> ('raw, 'glb) intern_fun
 
 val generic_intern : (raw_generic_argument, glob_generic_argument) intern_fun
 
-(** {5 Substitution functions} *)
-
-type 'glb subst_fun = substitution -> 'glb -> 'glb
-(** The type of functions used for substituting generic arguments. *)
-
-val substitute : ('raw, 'glb, 'top) genarg_type -> 'glb subst_fun
-
-val generic_substitute : glob_generic_argument subst_fun
-
 (** {5 Notation functions} *)
 
 type 'glb ntn_subst_fun = Id.Set.t -> Glob_term.glob_constr Id.Map.t -> 'glb -> 'glb
@@ -69,8 +59,5 @@ val generic_substitute_notation : glob_generic_argument ntn_subst_fun
 val register_intern0 : ('raw, 'glb, 'top) genarg_type ->
   ('raw, 'glb) intern_fun -> unit
 
-val register_subst0 : ('raw, 'glb, 'top) genarg_type ->
-  'glb subst_fun -> unit
-
 val register_ntn_subst0 : ('raw, 'glb, 'top) genarg_type ->
   'glb ntn_subst_fun -> unit
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 22316c33cb66..c2c2fb0a87e1 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -920,7 +920,7 @@ let rec subst_notation_constr subst bound raw =
     else NHole (nknd, naming)
 
   | NGenarg arg ->
-    let arg' = Genintern.generic_substitute subst arg in
+    let arg' = Gensubst.generic_substitute subst arg in
     if arg' == arg then raw
     else NGenarg arg'
 
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index bcf3aeeda177..abf028b5ebe4 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -830,7 +830,7 @@ let in_tacval =
   let intern_fun _ e = Empty.abort e in
   let subst_fun s v = v in
   let () = Genintern.register_intern0 wit intern_fun in
-  let () = Genintern.register_subst0 wit subst_fun in
+  let () = Gensubst.register_subst0 wit subst_fun in
   (* No need to register a value tag for it via register_val0 since we will
      never access this genarg directly. *)
   let interp_fun ist tac =
@@ -871,7 +871,7 @@ type ('a, 'b) argument_intern =
 | ArgInternWit : ('a, 'b, 'c) Genarg.genarg_type -> ('a, 'b) argument_intern
 
 type 'b argument_subst =
-| ArgSubstFun : 'b Genintern.subst_fun -> 'b argument_subst
+| ArgSubstFun : 'b Gensubst.subst_fun -> 'b argument_subst
 | ArgSubstWit : ('a, 'b, 'c) Genarg.genarg_type -> 'b argument_subst
 
 type ('b, 'c) argument_interp =
@@ -898,7 +898,7 @@ match arg.arg_intern with
     let ans = Genarg.out_gen (glbwit wit) (Tacintern.intern_genarg ist (Genarg.in_gen (rawwit wit) v)) in
     (ist, ans)
 
-let subst_fun (type a b c) (arg : (a, b, c) tactic_argument) : b Genintern.subst_fun =
+let subst_fun (type a b c) (arg : (a, b, c) tactic_argument) : b Gensubst.subst_fun =
 match arg.arg_subst with
 | ArgSubstFun f -> f
 | ArgSubstWit wit ->
@@ -923,7 +923,7 @@ match arg.arg_interp with
 let argument_extend (type a b c) ~plugin ~name (arg : (a, b, c) tactic_argument) =
   let wit = Genarg.create_arg name in
   let () = Genintern.register_intern0 wit (intern_fun name arg) in
-  let () = Genintern.register_subst0 wit (subst_fun arg) in
+  let () = Gensubst.register_subst0 wit (subst_fun arg) in
   let tag = match arg.arg_tag with
   | None ->
     let () = register_val0 wit None in
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index 74386296c491..b1220f19061f 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -156,7 +156,7 @@ type ('a, 'b) argument_intern =
 | ArgInternWit : ('a, 'b, 'c) Genarg.genarg_type -> ('a, 'b) argument_intern
 
 type 'b argument_subst =
-| ArgSubstFun : 'b Genintern.subst_fun -> 'b argument_subst
+| ArgSubstFun : 'b Gensubst.subst_fun -> 'b argument_subst
 | ArgSubstWit : ('a, 'b, 'c) Genarg.genarg_type -> 'b argument_subst
 
 type ('b, 'c) argument_interp =
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 56df9ec2256e..7a64d21d60cb 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -2061,7 +2061,7 @@ let def_interp ist x = Ftactic.return x
 
 let declare_uniform t =
   Genintern.register_intern0 t def_intern;
-  Genintern.register_subst0 t def_subst;
+  Gensubst.register_subst0 t def_subst;
   register_interp0 t def_interp
 
 let () =
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index a30975f175df..7e6043925b91 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -272,29 +272,29 @@ and subst_genarg subst (GenArg (Glbwit wit, x)) =
     let q = out_gen (glbwit wit2) (subst_genarg subst (in_gen (glbwit wit2) q)) in
     in_gen (glbwit (wit_pair wit1 wit2)) (p, q)
   | ExtraArg s ->
-      Genintern.generic_substitute subst (in_gen (glbwit wit) x)
+      Gensubst.generic_substitute subst (in_gen (glbwit wit) x)
 
 (** Registering *)
 
 let () =
-  Genintern.register_subst0 wit_int_or_var (fun _ v -> v);
-  Genintern.register_subst0 wit_nat_or_var (fun _ v -> v);
-  Genintern.register_subst0 wit_ref subst_global_reference;
-  Genintern.register_subst0 wit_smart_global subst_global_reference;
-  Genintern.register_subst0 wit_pre_ident (fun _ v -> v);
-  Genintern.register_subst0 wit_ident (fun _ v -> v);
-  Genintern.register_subst0 wit_hyp (fun _ v -> v);
-  Genintern.register_subst0 wit_intropattern subst_intro_pattern [@warning "-3"];
-  Genintern.register_subst0 wit_simple_intropattern subst_intro_pattern;
-  Genintern.register_subst0 wit_tactic subst_tactic;
-  Genintern.register_subst0 wit_ltac subst_tactic;
-  Genintern.register_subst0 wit_constr subst_glob_constr;
-  Genintern.register_subst0 wit_clause_dft_concl (fun _ v -> v);
-  Genintern.register_subst0 wit_uconstr (fun subst c -> subst_glob_constr subst c);
-  Genintern.register_subst0 wit_open_constr (fun subst c -> subst_glob_constr subst c);
-  Genintern.register_subst0 Redexpr.wit_red_expr subst_redexp;
-  Genintern.register_subst0 wit_quant_hyp subst_declared_or_quantified_hypothesis;
-  Genintern.register_subst0 wit_bindings subst_bindings;
-  Genintern.register_subst0 wit_constr_with_bindings subst_glob_with_bindings;
-  Genintern.register_subst0 wit_destruction_arg subst_destruction_arg;
+  Gensubst.register_subst0 wit_int_or_var (fun _ v -> v);
+  Gensubst.register_subst0 wit_nat_or_var (fun _ v -> v);
+  Gensubst.register_subst0 wit_ref subst_global_reference;
+  Gensubst.register_subst0 wit_smart_global subst_global_reference;
+  Gensubst.register_subst0 wit_pre_ident (fun _ v -> v);
+  Gensubst.register_subst0 wit_ident (fun _ v -> v);
+  Gensubst.register_subst0 wit_hyp (fun _ v -> v);
+  Gensubst.register_subst0 wit_intropattern subst_intro_pattern [@warning "-3"];
+  Gensubst.register_subst0 wit_simple_intropattern subst_intro_pattern;
+  Gensubst.register_subst0 wit_tactic subst_tactic;
+  Gensubst.register_subst0 wit_ltac subst_tactic;
+  Gensubst.register_subst0 wit_constr subst_glob_constr;
+  Gensubst.register_subst0 wit_clause_dft_concl (fun _ v -> v);
+  Gensubst.register_subst0 wit_uconstr (fun subst c -> subst_glob_constr subst c);
+  Gensubst.register_subst0 wit_open_constr (fun subst c -> subst_glob_constr subst c);
+  Gensubst.register_subst0 Redexpr.wit_red_expr subst_redexp;
+  Gensubst.register_subst0 wit_quant_hyp subst_declared_or_quantified_hypothesis;
+  Gensubst.register_subst0 wit_bindings subst_bindings;
+  Gensubst.register_subst0 wit_constr_with_bindings subst_glob_with_bindings;
+  Gensubst.register_subst0 wit_destruction_arg subst_destruction_arg;
   ()
diff --git a/plugins/ltac2/tac2core.ml b/plugins/ltac2/tac2core.ml
index f7792eeeeb0f..96f3b9e2e9fc 100644
--- a/plugins/ltac2/tac2core.ml
+++ b/plugins/ltac2/tac2core.ml
@@ -1773,7 +1773,7 @@ let () =
     else
       return (Tac2ffi.of_closure (Tac2ffi.abstract len clos))
   in
-  let subst s (ids, tac) = (ids, Genintern.substitute Ltac_plugin.Tacarg.wit_tactic s tac) in
+  let subst s (ids, tac) = (ids, Gensubst.substitute Ltac_plugin.Tacarg.wit_tactic s tac) in
   let print env sigma (ids, tac) =
     let ids =
       if List.is_empty ids then mt ()
@@ -1830,7 +1830,7 @@ let () =
     else
       return (Tac2ffi.of_closure (Tac2ffi.abstract len clos))
   in
-  let subst s (ids, tac) = (ids, Genintern.substitute Tacarg.wit_tactic s tac) in
+  let subst s (ids, tac) = (ids, Gensubst.substitute Tacarg.wit_tactic s tac) in
   let print env sigma (ids, tac) =
     let ids =
       if List.is_empty ids then mt ()
@@ -2007,7 +2007,7 @@ let () =
   let intern_fun _ e = Empty.abort e in
   let subst_fun s v = v in
   let () = Genintern.register_intern0 wit_ltac2_val intern_fun in
-  let () = Genintern.register_subst0 wit_ltac2_val subst_fun in
+  let () = Gensubst.register_subst0 wit_ltac2_val subst_fun in
   (* These are bound names and not relevant *)
   let tac_id = Id.of_string "F" in
   let arg_id = Id.of_string "X" in
diff --git a/plugins/ltac2/tac2intern.ml b/plugins/ltac2/tac2intern.ml
index ca1269935184..f799d2c0ec47 100644
--- a/plugins/ltac2/tac2intern.ml
+++ b/plugins/ltac2/tac2intern.ml
@@ -1992,9 +1992,9 @@ let () =
   in
   Genintern.register_intern0 wit_ltac2_constr intern
 
-let () = Genintern.register_subst0 wit_ltac2in1 (fun s (ids, e) -> ids, subst_expr s e)
-let () = Genintern.register_subst0 wit_ltac2in1_val subst_expr
-let () = Genintern.register_subst0 wit_ltac2_constr (fun s (ids, e) -> ids, subst_expr s e)
+let () = Gensubst.register_subst0 wit_ltac2in1 (fun s (ids, e) -> ids, subst_expr s e)
+let () = Gensubst.register_subst0 wit_ltac2in1_val subst_expr
+let () = Gensubst.register_subst0 wit_ltac2_constr (fun s (ids, e) -> ids, subst_expr s e)
 
 let intern_var_quotation ist (kind, { CAst.v = id; loc }) =
   let open Genintern in
@@ -2034,4 +2034,4 @@ let intern_var_quotation ist (kind, { CAst.v = id; loc }) =
 
 let () = Genintern.register_intern0 wit_ltac2_var_quotation intern_var_quotation
 
-let () = Genintern.register_subst0 wit_ltac2_var_quotation (fun _ v -> v)
+let () = Gensubst.register_subst0 wit_ltac2_var_quotation (fun _ v -> v)
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index c29be6173cad..7515f9a38846 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -166,7 +166,7 @@ let add_genarg tag pr =
   let interp ist x = Ftactic.return (Geninterp.Val.Dyn (tag, x)) in
   let gen_pr env sigma _ _ _ = pr env sigma in
   let () = Genintern.register_intern0 wit glob in
-  let () = Genintern.register_subst0 wit subst in
+  let () = Gensubst.register_subst0 wit subst in
   let () = Geninterp.register_interp0 wit interp in
   let () = Geninterp.register_val0 wit (Some (Geninterp.Val.Base tag)) in
   Pptactic.declare_extra_genarg_pprule wit gen_pr gen_pr gen_pr;
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 4226215d6d7f..b79ea500eb03 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -111,7 +111,7 @@ let add_genarg tag pr =
   let interp ist x = Ftactic.return (Geninterp.Val.Dyn (tag, x)) in
   let gen_pr env sigma _ _ _ = pr env sigma in
   let () = Genintern.register_intern0 wit glob in
-  let () = Genintern.register_subst0 wit subst in
+  let () = Gensubst.register_subst0 wit subst in
   let () = Geninterp.register_interp0 wit interp in
   let () = Geninterp.register_val0 wit (Some (Geninterp.Val.Base tag)) in
   Pptactic.declare_extra_genarg_pprule wit gen_pr gen_pr gen_pr;
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 072ee3d6a03a..094d2dbacbbb 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -1138,8 +1138,6 @@ let rec subst_cases_pattern subst = DAst.map (function
           PatCstr (((kn',i),j),cpl',n)
   )
 
-let (f_subst_genarg, subst_genarg_hook) = Hook.make ()
-
 let rec subst_glob_constr env subst = DAst.map (function
   | GRef (ref,u) as raw ->
     let ref',t = subst_global subst ref in
@@ -1250,7 +1248,7 @@ let rec subst_glob_constr env subst = DAst.map (function
     else GHole (nknd, naming)
 
   | GGenarg arg as raw ->
-    let arg' = Hook.get f_subst_genarg subst arg in
+    let arg' = Gensubst.generic_substitute subst arg in
     if arg' == arg then raw
     else GGenarg arg'
 
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 6db4318b9483..735b249f7d32 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -70,9 +70,6 @@ val lookup_index_as_renamed : env -> evar_map -> constr -> int -> int option
 val force_wildcard : unit -> bool
 val synthetize_type : unit -> bool
 
-val subst_genarg_hook :
-  (substitution -> Genarg.glob_generic_argument -> Genarg.glob_generic_argument) Hook.t
-
 module PrintingInductiveMake :
   functor (Test : sig
     val encode : Environ.env -> Libnames.qualid -> Names.inductive
diff --git a/pretyping/gensubst.ml b/pretyping/gensubst.ml
new file mode 100644
index 000000000000..89a67a063065
--- /dev/null
+++ b/pretyping/gensubst.ml
@@ -0,0 +1,29 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Genarg
+
+(** Substitution functions *)
+type 'glb subst_fun = Mod_subst.substitution -> 'glb -> 'glb
+
+module SubstObj =
+struct
+  type ('raw, 'glb, 'top) obj = 'glb subst_fun
+  let name = "subst"
+  let default _ = None
+end
+
+module Subst = Register (SubstObj)
+
+let substitute = Subst.obj
+let register_subst0 = Subst.register0
+
+let generic_substitute subs (GenArg (Glbwit wit, v)) =
+  in_gen (glbwit wit) (substitute wit subs v)
diff --git a/pretyping/gensubst.mli b/pretyping/gensubst.mli
new file mode 100644
index 000000000000..70bcf7d10b17
--- /dev/null
+++ b/pretyping/gensubst.mli
@@ -0,0 +1,23 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Genarg
+
+(** {5 Substitution functions} *)
+
+type 'glb subst_fun = Mod_subst.substitution -> 'glb -> 'glb
+(** The type of functions used for substituting generic arguments. *)
+
+val substitute : ('raw, 'glb, 'top) genarg_type -> 'glb subst_fun
+
+val generic_substitute : glob_generic_argument subst_fun
+
+val register_subst0 : ('raw, 'glb, 'top) genarg_type ->
+  'glb subst_fun -> unit
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 213992bf0661..7e45f95d72eb 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -479,7 +479,7 @@ let subst_hintrewrite (subst,(rbase,list as node)) =
     let cst' = subst_mps subst hint.rew_lemma in
     let typ' = subst_mps subst hint.rew_type in
     let pat' = subst_mps subst hint.rew_pat in
-    let t' = Option.Smart.map (Genintern.generic_substitute subst) hint.rew_tac in
+    let t' = Option.Smart.map (Gensubst.generic_substitute subst) hint.rew_tac in
       if hint.rew_id == id' && hint.rew_lemma == cst' && hint.rew_type == typ' &&
          hint.rew_tac == t' && hint.rew_pat == pat' then hint else
         { hint with
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 261d91376c52..d944acb72bdc 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1183,7 +1183,7 @@ let subst_autohint (subst, obj) =
           if ref==ref' then data.code.obj else Unfold_nth ref'
       | Extern (pat, tac) ->
           let pat' = Option.Smart.map (subst_pattern env sigma subst) pat in
-          let tac' = Genintern.generic_substitute subst tac in
+          let tac' = Gensubst.generic_substitute subst tac in
           if pat==pat' && tac==tac' then data.code.obj else Extern (pat', tac')
     in
     let name' = Option.Smart.map (subst_global_reference subst) data.name in

From 39115d0ed94fec6dc3b689879d063d3010c9ca95 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Wed, 31 May 2023 15:47:18 +0200
Subject: [PATCH 2/2] Support quotations (genargs) in patterns

For #11641

`constr_pattern` is split in 2 types, one is allowed to contain
genargs and the other not.
To share code this uses a GADT `'i uninstantiated_pattern` used in
`'i constr_pattern_r`,
with genargs allowed instantiated to `` [`uninstantiated] constr_pattern_r ``,
without genargs instantiated to `` constr_pattern = [`any] constr_pattern_r ``.

Ltac2 instantiates the genargs in the `ml_interp` for the TacExt ie
a pattern expression is interned to `` [`uninstantiated] constr_pattern_r ``
then interped to `constr_pattern`.

Most code (basically everything except ltac2) uses only the no-genarg
version (TODO change this? but currently we have no non-ltac2 genargs
handled).

For now I just have it handling `$pattern:` quotations.

For instance something like `ltac2pat:(tactic : pattern)` should be
easy to implement (main issue is how to handle the tactic monad
switch, but maybe `interp_pat` should live in the monad?).

Exposing a `preterm -> pattern` should also be possible.

Also maybe internalization should pass around `pattern_mode`? This
would let us intern `ltac2:(tac)` with different expected types
depending on if we're interning as constr or pattern.

PS the genarg mod_subst operators should probably be in their own
gensubst module, for now out of lazyness I put them in genarg.ml
---
 .../17667-SkySkimmer-pattern-quotations.sh    |  7 ++
 .../17667-pattern-quotations.rst              |  5 ++
 doc/sphinx/proof-engine/ltac2.rst             |  9 ++
 interp/constrextern.ml                        | 36 ++++----
 interp/constrextern.mli                       |  2 +-
 interp/constrintern.ml                        | 11 ++-
 interp/constrintern.mli                       |  4 +
 interp/genintern.ml                           | 21 +++++
 interp/genintern.mli                          | 12 +++
 plugins/ltac2/tac2core.ml                     | 36 ++++++--
 plugins/ltac2/tac2env.ml                      |  1 +
 plugins/ltac2/tac2env.mli                     |  1 +
 plugins/ltac2/tac2intern.ml                   | 26 +++++-
 plugins/ltac2/tac2quote.mli                   |  2 +-
 pretyping/constr_matching.ml                  |  4 +-
 pretyping/detyping.mli                        |  6 +-
 pretyping/genarg.ml                           | 22 +++++
 pretyping/genarg.mli                          | 15 ++++
 pretyping/pattern.mli                         | 38 ++++++---
 pretyping/patternops.ml                       | 85 ++++++++++++++++---
 pretyping/patternops.mli                      | 22 +++--
 printing/printer.mli                          |  4 +-
 tactics/btermdn.ml                            |  3 +-
 test-suite/bugs/bug_11641.v                   | 28 ++++++
 24 files changed, 332 insertions(+), 68 deletions(-)
 create mode 100644 dev/ci/user-overlays/17667-SkySkimmer-pattern-quotations.sh
 create mode 100644 doc/changelog/06-Ltac2-language/17667-pattern-quotations.rst
 create mode 100644 test-suite/bugs/bug_11641.v

diff --git a/dev/ci/user-overlays/17667-SkySkimmer-pattern-quotations.sh b/dev/ci/user-overlays/17667-SkySkimmer-pattern-quotations.sh
new file mode 100644
index 000000000000..eddb77ecd036
--- /dev/null
+++ b/dev/ci/user-overlays/17667-SkySkimmer-pattern-quotations.sh
@@ -0,0 +1,7 @@
+overlay elpi https://github.com/SkySkimmer/coq-elpi pattern-quotations 17667
+
+overlay equations https://github.com/SkySkimmer/Coq-Equations pattern-quotations 17667
+
+overlay serapi https://github.com/SkySkimmer/coq-serapi pattern-quotations 17667
+
+overlay tactician https://github.com/SkySkimmer/coq-tactician pattern-quotations 17667
diff --git a/doc/changelog/06-Ltac2-language/17667-pattern-quotations.rst b/doc/changelog/06-Ltac2-language/17667-pattern-quotations.rst
new file mode 100644
index 000000000000..f07b0e0126c2
--- /dev/null
+++ b/doc/changelog/06-Ltac2-language/17667-pattern-quotations.rst
@@ -0,0 +1,5 @@
+- **Added:**
+  Ltac2 supports pattern quotations when building `pattern` values.
+  This allows building dynamic patterns, eg `Ltac2 eq_pattern a b := pattern:($pattern:a = $pattern:b)`
+  (`#17667 <https://github.com/coq/coq/pull/17667>`_,
+  by Gaëtan Gilbert).
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index 21887ea6943f..2a3c2c617deb 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -777,6 +777,15 @@ Similarly variables of type `preterm` have an antiquotation
 
 It is equivalent to pretyping the preterm with the appropriate typing constraint.
 
+Variables of type `pattern` have an antiquotation
+
+.. prodn:: term += $pattern:@lident
+
+Its use is only allowed when producing a pattern, i.e.
+`pattern:($pattern:x -> True)` is allowed but
+`constr:($pattern:x -> True)` is not allowed. Conversely `constr` and `preterm`
+antiquotations are not allowed when producing a pattern.
+
 Match over terms
 ~~~~~~~~~~~~~~~~
 
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index fa8e1246256b..2e40ed0fc148 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1399,7 +1399,22 @@ let compute_displayed_name_in_pattern sigma avoid na c =
   let open Namegen in
   compute_displayed_name_in_gen (fun _ -> Patternops.noccurn_pattern) sigma avoid na c
 
-let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
+let glob_of_pat_under_context glob_of_pat avoid env sigma (nas, pat) =
+  let fold (avoid, env, nas, epat) na =
+    let na, avoid = compute_displayed_name_in_pattern (Global.env ()) sigma avoid na epat in
+    let env = Termops.add_name na env in
+    let epat = match epat with PLambda (_, _, p) -> p | _ -> assert false in
+    (avoid, env, na :: nas, epat)
+  in
+  let epat = Array.fold_right (fun na p -> PLambda (na, PMeta None, p)) nas pat in
+  let (avoid', env', nas, _) = Array.fold_left fold (avoid, env, [], epat) nas in
+  let pat = glob_of_pat avoid' env' sigma pat in
+  (Array.rev_of_list nas, pat)
+
+let rec glob_of_pat
+  : 'a. _ -> _ -> _ -> 'a constr_pattern_r -> _
+  = fun (type a) avoid env sigma (pat: a constr_pattern_r) ->
+    DAst.make @@ match pat with
   | PRef ref -> GRef (ref,None)
   | PVar id  -> GVar id
   | PEvar (evk,l) ->
@@ -1422,6 +1437,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
       GVar id
   | PMeta None -> GHole (Evar_kinds.InternalHole, IntroAnonymous)
   | PMeta (Some n) -> GPatVar (Evar_kinds.FirstOrderPatVar n)
+  | PUninstantiated (PGenarg g) -> GGenarg g
   | PProj (p,c) -> GApp (DAst.make @@ GRef (GlobRef.ConstRef (Projection.constant p),None),
                          [glob_of_pat avoid env sigma c])
   | PApp (f,args) ->
@@ -1446,7 +1462,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
       GIf (glob_of_pat avoid env sigma c, (Anonymous,None),
            glob_of_pat avoid env sigma b1, glob_of_pat avoid env sigma b2)
   | PCase ({cip_style=Constr.LetStyle},None,tm,[(0,n,b)]) ->
-      let n, b = glob_of_pat_under_context avoid env sigma (n, b) in
+      let n, b = glob_of_pat_under_context glob_of_pat avoid env sigma (n, b) in
       let nal = Array.to_list n in
       GLetTuple (nal,(Anonymous,None),glob_of_pat avoid env sigma tm,b)
   | PCase (info,p,tm,bl) ->
@@ -1454,7 +1470,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
         | [], _ -> []
         | _, Some ind ->
           let map (i, n, c) =
-            let n, c = glob_of_pat_under_context avoid env sigma (n, c) in
+            let n, c = glob_of_pat_under_context glob_of_pat avoid env sigma (n, c) in
             let nal = Array.to_list n in
             let mkPatVar na = DAst.make @@ PatVar na in
             let p = DAst.make @@ PatCstr ((ind,i+1),List.map mkPatVar nal,Anonymous) in
@@ -1469,7 +1485,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
       let indnames,rtn = match p, info.cip_ind with
         | None, _ -> (Anonymous,None),None
         | Some p, Some ind ->
-          let nas, p = glob_of_pat_under_context avoid env sigma p in
+          let nas, p = glob_of_pat_under_context glob_of_pat avoid env sigma p in
           let nas = Array.rev_to_list nas in
           ((List.hd nas, Some (CAst.make (ind, List.tl nas))), Some p)
         | _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive.")
@@ -1515,18 +1531,6 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
     let glob_of = glob_of_pat avoid env sigma in
     GArray (None, Array.map glob_of t, glob_of def, glob_of ty)
 
-and glob_of_pat_under_context avoid env sigma (nas, pat) =
-  let fold (avoid, env, nas, epat) na =
-    let na, avoid = compute_displayed_name_in_pattern (Global.env ()) sigma avoid na epat in
-    let env = Termops.add_name na env in
-    let epat = match epat with PLambda (_, _, p) -> p | _ -> assert false in
-    (avoid, env, na :: nas, epat)
-  in
-  let epat = Array.fold_right (fun na p -> PLambda (na, PMeta None, p)) nas pat in
-  let (avoid', env', nas, _) = Array.fold_left fold (avoid, env, [], epat) nas in
-  let pat = glob_of_pat avoid' env' sigma pat in
-  (Array.rev_of_list nas, pat)
-
 let extern_constr_pattern env sigma pat =
   extern true ((constr_some_level,None),([],[]))
     (* XXX no vars? *)
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 69bc2343ee84..f9b78192a506 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -29,7 +29,7 @@ val extern_cases_pattern : Id.Set.t -> 'a cases_pattern_g -> cases_pattern_expr
 val extern_glob_constr : extern_env -> 'a glob_constr_g -> constr_expr
 val extern_glob_type : ?impargs:Glob_term.binding_kind list -> extern_env -> 'a glob_constr_g -> constr_expr
 val extern_constr_pattern : names_context -> Evd.evar_map ->
-  constr_pattern -> constr_expr
+  _ constr_pattern_r -> constr_expr
 val extern_closed_glob : ?goal_concl_style:bool -> ?inctx:bool -> ?scope:scope_name ->
   env -> Evd.evar_map -> closed_glob_constr -> constr_expr
 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 2c590d59ea52..adad3695a329 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2400,7 +2400,11 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
           intern_sign;
           strict_check = match env.strict_check with None -> false | Some b -> b;
         } in
-        let (_, glb) = Genintern.generic_intern ist gen in
+        let intern = if pattern_mode
+          then Genintern.generic_intern_pat ?loc
+          else Genintern.generic_intern
+        in
+        let (_, glb) = intern ist gen in
         DAst.make ?loc @@
         GGenarg glb
     (* Parsing pattern variables *)
@@ -2740,6 +2744,11 @@ let intern_constr_pattern env sigma ?(as_type=false) ?strict_check ?(ltacvars=em
             ?strict_check ~pattern_mode:true ~ltacvars env sigma c in
   pattern_of_glob_constr c
 
+let intern_uninstantiated_constr_pattern env sigma ?(as_type=false) ?strict_check ?(ltacvars=empty_ltac_sign) c =
+  let c = intern_gen (if as_type then IsType else WithoutTypeConstraint)
+            ?strict_check ~pattern_mode:true ~ltacvars env sigma c in
+  uninstantiated_pattern_of_glob_constr c
+
 let intern_core kind env sigma ?strict_check ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign)
       { Genintern.intern_ids = ids; Genintern.notation_variable_status = vl } c =
   let tmp_scope = scope_of_type_kind env sigma kind in
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 6eea239a5dac..790e97b477be 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -144,6 +144,10 @@ val intern_constr_pattern :
   env -> evar_map -> ?as_type:bool -> ?strict_check:bool -> ?ltacvars:ltac_sign ->
     constr_pattern_expr -> Id.Set.t * constr_pattern
 
+val intern_uninstantiated_constr_pattern :
+  env -> evar_map -> ?as_type:bool -> ?strict_check:bool -> ?ltacvars:ltac_sign ->
+    constr_pattern_expr -> Id.Set.t * [`uninstantiated] constr_pattern_r
+
 (** Returns None if it's an abbreviation not bound to a name, raises an error
     if not existing *)
 val intern_reference : qualid -> GlobRef.t option
diff --git a/interp/genintern.ml b/interp/genintern.ml
index 53ec646f8c86..765f3af293a1 100644
--- a/interp/genintern.ml
+++ b/interp/genintern.ml
@@ -75,6 +75,27 @@ let generic_intern ist (GenArg (Rawwit wit, v)) =
   let (ist, v) = intern wit ist v in
   (ist, in_gen (glbwit wit) v)
 
+type ('raw,'glb) intern_pat_fun = ?loc:Loc.t -> ('raw,'glb) intern_fun
+
+module InternPatObj = struct
+  type ('raw, 'glb, 'top) obj = ('raw, 'glb) intern_pat_fun
+  let name = "intern_pat"
+  let default tag =
+    Some (fun ?loc ->
+        let name = Genarg.(ArgT.repr (get_arg_tag tag)) in
+        CErrors.user_err ?loc Pp.(str "This quotation is not supported in tactic patterns (" ++ str name ++ str ")"))
+end
+
+module InternPat = Register (InternPatObj)
+
+let intern_pat = InternPat.obj
+
+let register_intern_pat = InternPat.register0
+
+let generic_intern_pat ?loc ist (GenArg (Rawwit wit, v)) =
+  let (ist, v) = intern_pat wit ?loc ist v in
+  (ist, in_gen (glbwit wit) v)
+
 (** Notation substitution *)
 
 let substitute_notation = NtnSubst.obj
diff --git a/interp/genintern.mli b/interp/genintern.mli
index 27ff89c67193..b6483c69585f 100644
--- a/interp/genintern.mli
+++ b/interp/genintern.mli
@@ -46,6 +46,14 @@ val intern : ('raw, 'glb, 'top) genarg_type -> ('raw, 'glb) intern_fun
 
 val generic_intern : (raw_generic_argument, glob_generic_argument) intern_fun
 
+(** {5 Internalization in tactic patterns} *)
+
+type ('raw,'glb) intern_pat_fun = ?loc:Loc.t -> ('raw,'glb) intern_fun
+
+val intern_pat : ('raw, 'glb, 'top) genarg_type -> ('raw, 'glb) intern_pat_fun
+
+val generic_intern_pat : (raw_generic_argument, glob_generic_argument) intern_pat_fun
+
 (** {5 Notation functions} *)
 
 type 'glb ntn_subst_fun = Id.Set.t -> Glob_term.glob_constr Id.Map.t -> 'glb -> 'glb
@@ -59,5 +67,9 @@ val generic_substitute_notation : glob_generic_argument ntn_subst_fun
 val register_intern0 : ('raw, 'glb, 'top) genarg_type ->
   ('raw, 'glb) intern_fun -> unit
 
+val register_intern_pat : ('raw, 'glb, 'top) genarg_type ->
+  ('raw, 'glb) intern_pat_fun -> unit
+
+
 val register_ntn_subst0 : ('raw, 'glb, 'top) genarg_type ->
   'glb ntn_subst_fun -> unit
diff --git a/plugins/ltac2/tac2core.ml b/plugins/ltac2/tac2core.ml
index 96f3b9e2e9fc..b21e94bc89d9 100644
--- a/plugins/ltac2/tac2core.ml
+++ b/plugins/ltac2/tac2core.ml
@@ -1642,11 +1642,15 @@ let () =
   define_ml_object Tac2quote.wit_ident obj
 
 let () =
-  let intern self ist c =
-    let env = ist.Genintern.genv in
+  let intern self {Genintern.ltacvars=lfun; genv=env; extra; intern_sign=_; strict_check} c =
     let sigma = Evd.from_env env in
-    let strict_check = ist.Genintern.strict_check in
-    let _, pat = Constrintern.intern_constr_pattern env sigma ~strict_check ~as_type:false c in
+    let ltacvars = {
+      Constrintern.ltac_vars = lfun;
+      ltac_bound = Id.Set.empty;
+      ltac_extra = extra;
+    }
+    in
+    let _, pat = Constrintern.intern_uninstantiated_constr_pattern env sigma ~strict_check ~as_type:false ~ltacvars c in
     GlbVal pat, gtypref t_pattern
   in
   let subst subst c =
@@ -1656,7 +1660,13 @@ let () =
   in
   let print env sigma pat = str "pat:(" ++ Printer.pr_lconstr_pattern_env env sigma pat ++ str ")" in
   let raw_print env sigma pat = str "pat:(" ++ Ppconstr.pr_constr_pattern_expr env sigma pat ++ str ")" in
-  let interp _ c = return (Tac2ffi.of_pattern c) in
+  let interp env c =
+    let ist = to_lvar env in
+    pf_apply ~catch_exceptions:true begin fun env sigma ->
+      let c = Patternops.interp_pattern env sigma ist c in
+      return (Tac2ffi.of_pattern c)
+    end
+  in
   let obj = {
     ml_intern = intern;
     ml_interp = interp;
@@ -1917,11 +1927,26 @@ let () =
     let f = match kind with
       | ConstrVar -> interp_constr_var_as_constr
       | PretermVar -> interp_preterm_var_as_constr
+      | PatternVar -> assert false
     in
     f ?loc env sigma tycon id
   in
   GlobEnv.register_constr_interp0 wit_ltac2_var_quotation interp
 
+let () =
+  let interp env sigma ist (kind,id) =
+    let () = match kind with
+      | ConstrVar -> assert false (* checked at intern time *)
+      | PretermVar -> assert false
+      | PatternVar -> ()
+    in
+    let ist = Tac2interp.get_env ist.Ltac_pretype.ltac_genargs in
+    let c = Id.Map.find id ist.env_ist in
+    let c = Tac2ffi.to_pattern c in
+    c
+  in
+  Patternops.register_interp_pat wit_ltac2_var_quotation interp
+
 let () =
   let pr_raw (kind,id) = Genprint.PrinterBasic (fun _env _sigma ->
       let ppkind =
@@ -1935,6 +1960,7 @@ let () =
       let ppkind = match kind with
         | ConstrVar -> mt()
         | PretermVar -> str "preterm:"
+        | PatternVar -> str "pattern:"
       in
       str "$" ++ ppkind ++ Id.print id) in
   let pr_top x = Util.Empty.abort x in
diff --git a/plugins/ltac2/tac2env.ml b/plugins/ltac2/tac2env.ml
index 0e8f11d12454..775725ffb1bd 100644
--- a/plugins/ltac2/tac2env.ml
+++ b/plugins/ltac2/tac2env.ml
@@ -329,6 +329,7 @@ let ltac1_prefix =
 type var_quotation_kind =
   | ConstrVar
   | PretermVar
+  | PatternVar
 
 let wit_ltac2in1 = Genarg.make0 "ltac2in1"
 let wit_ltac2in1_val = Genarg.make0 "ltac2in1val"
diff --git a/plugins/ltac2/tac2env.mli b/plugins/ltac2/tac2env.mli
index 6f931081f608..555a014e12d6 100644
--- a/plugins/ltac2/tac2env.mli
+++ b/plugins/ltac2/tac2env.mli
@@ -180,6 +180,7 @@ val wit_ltac2_constr : (raw_tacexpr, Id.Set.t * glb_tacexpr, Util.Empty.t) genar
 type var_quotation_kind =
   | ConstrVar
   | PretermVar
+  | PatternVar
 
 val wit_ltac2_var_quotation : (lident option * lident, var_quotation_kind * Id.t, Util.Empty.t) genarg_type
 (** Ltac2 quotations for variables "$x" or "$kind:foo" in Gallina terms.
diff --git a/plugins/ltac2/tac2intern.ml b/plugins/ltac2/tac2intern.ml
index f799d2c0ec47..8b86a4c154a6 100644
--- a/plugins/ltac2/tac2intern.ml
+++ b/plugins/ltac2/tac2intern.ml
@@ -31,6 +31,7 @@ let t_constr = coq_type "constr"
 let t_ltac1 = ltac1_kn "t"
 let ltac1_lamdba = ltac1_kn "lambda"
 let t_preterm = coq_type "preterm"
+let t_pattern = coq_type "pattern"
 let t_bool = coq_type "bool"
 
 let ltac2_env : Tac2typing_env.t Genintern.Store.field =
@@ -1996,20 +1997,31 @@ let () = Gensubst.register_subst0 wit_ltac2in1 (fun s (ids, e) -> ids, subst_exp
 let () = Gensubst.register_subst0 wit_ltac2in1_val subst_expr
 let () = Gensubst.register_subst0 wit_ltac2_constr (fun s (ids, e) -> ids, subst_expr s e)
 
-let intern_var_quotation ist (kind, { CAst.v = id; loc }) =
+let intern_var_quotation_gen ~ispat ist (kind, { CAst.v = id; loc }) =
   let open Genintern in
   let kind = match kind with
     | None -> ConstrVar
     | Some kind -> match Id.to_string kind.CAst.v with
       | "constr" -> ConstrVar
       | "preterm" -> PretermVar
+      | "pattern" -> PatternVar
       | _ ->
         CErrors.user_err ?loc:kind.loc
           Pp.(str "Unknown Ltac2 variable quotation kind" ++ spc() ++ Id.print kind.v)
   in
   let typ = match kind with
-    | ConstrVar -> t_constr
-    | PretermVar -> t_preterm
+    | ConstrVar ->
+      if ispat
+      then CErrors.user_err ?loc Pp.(str "constr quotations not supported in tactic patterns.")
+      else t_constr
+    | PretermVar ->
+      if ispat
+      then CErrors.user_err ?loc Pp.(str "preterm quotations not supported in tactic patterns.")
+      else t_preterm
+    | PatternVar ->
+      if not ispat
+      then CErrors.user_err ?loc Pp.(str "pattern quotations not supported outside tactic patterns.")
+      else t_pattern
   in
   let env = match Genintern.Store.get ist.extra ltac2_env with
     | None ->
@@ -2032,6 +2044,14 @@ let intern_var_quotation ist (kind, { CAst.v = id; loc }) =
   let () = unify ?loc env t (GTypRef (Other typ, [])) in
   (ist, (kind, id))
 
+let intern_var_quotation = intern_var_quotation_gen ~ispat:false
+
 let () = Genintern.register_intern0 wit_ltac2_var_quotation intern_var_quotation
 
+let intern_var_quotation_pat ?loc ist v =
+  intern_var_quotation_gen ~ispat:true ist v
+
+let () = Genintern.register_intern_pat wit_ltac2_var_quotation
+    intern_var_quotation_pat
+
 let () = Gensubst.register_subst0 wit_ltac2_var_quotation (fun _ v -> v)
diff --git a/plugins/ltac2/tac2quote.mli b/plugins/ltac2/tac2quote.mli
index 49d69e04397e..a24bcb7eecf0 100644
--- a/plugins/ltac2/tac2quote.mli
+++ b/plugins/ltac2/tac2quote.mli
@@ -95,7 +95,7 @@ val of_format : lstring -> raw_tacexpr
 
 (** {5 Generic arguments} *)
 
-val wit_pattern : (Constrexpr.constr_expr, Pattern.constr_pattern) Arg.tag
+val wit_pattern : (Constrexpr.constr_expr, [`uninstantiated] Pattern.constr_pattern_r) Arg.tag
 
 val wit_ident : (Id.t, Id.t) Arg.tag
 
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 3590503a0d4a..302c3224fa4f 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -285,7 +285,7 @@ let matches_core env sigma allow_bound_rels
     | ConstructRef c, Construct (c',u) -> Environ.QConstruct.equal env c c'
     | _, _ -> false
   in
-  let rec sorec ctx env subst p t =
+  let rec sorec ctx env subst (p:constr_pattern) t =
     let cT = strip_outer_cast sigma t in
     match p, EConstr.kind sigma cT with
       | PSoApp (n,args),m ->
@@ -479,6 +479,8 @@ let matches_core env sigma allow_bound_rels
          | PProd _ | PLetIn _ | PSort _ | PIf _ | PCase _
          | PFix _ | PCoFix _| PEvar _ | PInt _ | PFloat _ | PArray _), _ -> raise PatternMatchingFailure
 
+      | PUninstantiated _, _ -> .
+
   in
   sorec [] env ((Id.Map.empty,Id.Set.empty), Id.Map.empty) pat c
 
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 735b249f7d32..b81de87535a2 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -55,10 +55,10 @@ val detype_rel_context : 'a delay -> constr option -> Id.Set.t -> (names_context
   evar_map -> rel_context -> 'a glob_decl_g list
 
 val share_pattern_names :
-  (Id.Set.t -> names_context -> 'c -> Pattern.constr_pattern -> 'a) -> int ->
+  (Id.Set.t -> names_context -> 'c -> 'd Pattern.constr_pattern_r -> 'a) -> int ->
   (Name.t * binding_kind * 'b option * 'a) list ->
-  Id.Set.t -> names_context -> 'c -> Pattern.constr_pattern ->
-  Pattern.constr_pattern ->
+  Id.Set.t -> names_context -> 'c -> 'd Pattern.constr_pattern_r ->
+  'd Pattern.constr_pattern_r ->
   (Name.t * binding_kind * 'b option * 'a) list * 'a * 'a
 
 val detype_closed_glob :  ?isgoal:bool -> Id.Set.t -> env -> evar_map -> closed_glob_constr -> glob_constr
diff --git a/pretyping/genarg.ml b/pretyping/genarg.ml
index eb4da3361aeb..3d5bf486cb54 100644
--- a/pretyping/genarg.ml
+++ b/pretyping/genarg.ml
@@ -206,8 +206,30 @@ struct
       to an extra argument type, otherwise, it will badly fail. *)
   let obj t = get_obj0 @@ get_arg_tag t
 
+  let mem t =
+    let t = get_arg_tag t in
+    GenMap.mem t !arg0_map
+
   (** NB: we need the [Pack] pattern to get [tag]
       from [_ ArgT.DYN.tag] to [(_ * _ * _) ArgT.DYN.tag] *)
   let fold_keys f acc = GenMap.fold (fun (Any (tag,Pack _)) acc -> f (ArgT.Any tag) acc) !arg0_map acc
 
 end
+
+(** Substitution functions *)
+type 'glb subst_fun = Mod_subst.substitution -> 'glb -> 'glb
+
+module SubstObj =
+struct
+  type ('raw, 'glb, 'top) obj = 'glb subst_fun
+  let name = "subst"
+  let default _ = None
+end
+
+module Subst = Register (SubstObj)
+
+let substitute = Subst.obj
+let register_subst0 = Subst.register0
+
+let generic_substitute subs (GenArg (Glbwit wit, v)) =
+  in_gen (glbwit wit) (substitute wit subs v)
diff --git a/pretyping/genarg.mli b/pretyping/genarg.mli
index 19a265c01e51..fc0374dbe959 100644
--- a/pretyping/genarg.mli
+++ b/pretyping/genarg.mli
@@ -187,11 +187,26 @@ sig
   val obj : ('raw, 'glb, 'top) genarg_type -> ('raw, 'glb, 'top) M.obj
   (** Recover a manipulation function at a given type. *)
 
+  val mem : _ genarg_type -> bool
+  (** Is this type registered? *)
+
   val fold_keys : (ArgT.any -> 'acc -> 'acc) -> 'acc -> 'acc
   (** Fold over the registered keys. *)
 
 end
 
+(** {5 Substitution functions} *)
+
+type 'glb subst_fun = Mod_subst.substitution -> 'glb -> 'glb
+(** The type of functions used for substituting generic arguments. *)
+
+val substitute : ('raw, 'glb, 'top) genarg_type -> 'glb subst_fun
+
+val generic_substitute : glob_generic_argument subst_fun
+
+val register_subst0 : ('raw, 'glb, 'top) genarg_type ->
+  'glb subst_fun -> unit
+
 (** {5 Compatibility layer}
 
 The functions below are aliases for generic_type constructors.
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index 576b37dd1b90..c0f454b04165 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -20,27 +20,37 @@ type case_info_pattern =
       cip_ind : inductive option;
       cip_extensible : bool (** does this match end with _ => _ ? *) }
 
-type constr_pattern =
+type 'i uninstantiated_pattern =
+  | PGenarg : Genarg.glob_generic_argument -> [ `uninstantiated ] uninstantiated_pattern
+
+type 'i constr_pattern_r =
   | PRef of GlobRef.t
   | PVar of Id.t
-  | PEvar of (Evar.t * constr_pattern list)
+  | PEvar of (Evar.t * 'i constr_pattern_r list)
   | PRel of int
-  | PApp of constr_pattern * constr_pattern array
-  | PSoApp of patvar * constr_pattern list
-  | PProj of Projection.t * constr_pattern
-  | PLambda of Name.t * constr_pattern * constr_pattern
-  | PProd of Name.t * constr_pattern * constr_pattern
-  | PLetIn of Name.t * constr_pattern * constr_pattern option * constr_pattern
+  | PApp of 'i constr_pattern_r * 'i constr_pattern_r array
+  | PSoApp of patvar * 'i constr_pattern_r list
+  | PProj of Projection.t * 'i constr_pattern_r
+  | PLambda of Name.t * 'i constr_pattern_r * 'i constr_pattern_r
+  | PProd of Name.t * 'i constr_pattern_r * 'i constr_pattern_r
+  | PLetIn of Name.t * 'i constr_pattern_r * 'i constr_pattern_r option * 'i constr_pattern_r
   | PSort of Sorts.family
   | PMeta of patvar option
-  | PIf of constr_pattern * constr_pattern * constr_pattern
-  | PCase of case_info_pattern * (Name.t array * constr_pattern) option * constr_pattern *
-      (int * Name.t array * constr_pattern) list (** index of constructor, nb of args *)
-  | PFix of (int array * int) * (Name.t array * constr_pattern array * constr_pattern array)
-  | PCoFix of int * (Name.t array * constr_pattern array * constr_pattern array)
+  | PIf of 'i constr_pattern_r * 'i constr_pattern_r * 'i constr_pattern_r
+  | PCase of case_info_pattern * (Name.t array * 'i constr_pattern_r) option * 'i constr_pattern_r *
+      (int * Name.t array * 'i constr_pattern_r) list (** index of constructor, nb of args *)
+  | PFix of (int array * int) * (Name.t array * 'i constr_pattern_r array * 'i constr_pattern_r array)
+  | PCoFix of int * (Name.t array * 'i constr_pattern_r array * 'i constr_pattern_r array)
   | PInt of Uint63.t
   | PFloat of Float64.t
-  | PArray of constr_pattern array * constr_pattern * constr_pattern
+  | PArray of 'i constr_pattern_r array * 'i constr_pattern_r * 'i constr_pattern_r
+  | PUninstantiated of 'i uninstantiated_pattern
+
+type constr_pattern = [ `any ] constr_pattern_r
 
 (** Nota : in a [PCase], the array of branches might be shorter than
     expected, denoting the use of a final "_ => _" branch *)
+
+type _ pattern_kind =
+  | Any
+  | Uninstantiated : [`uninstantiated] pattern_kind
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index ac2283d93db7..c31286aca679 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -26,7 +26,7 @@ let case_info_pattern_eq i1 i2 =
   Option.equal Ind.CanOrd.equal i1.cip_ind i2.cip_ind &&
   i1.cip_extensible == i2.cip_extensible
 
-let rec constr_pattern_eq p1 p2 = match p1, p2 with
+let rec constr_pattern_eq (p1:constr_pattern) p2 = match p1, p2 with
 | PRef r1, PRef r2 -> GlobRef.CanOrd.equal r1 r2
 | PVar v1, PVar v2 -> Id.equal v1 v2
 | PEvar (ev1, ctx1), PEvar (ev2, ctx2) ->
@@ -66,6 +66,7 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with
 | PArray (t1, def1, ty1), PArray (t2, def2, ty2) ->
   Array.equal constr_pattern_eq t1 t2 && constr_pattern_eq def1 def2
   && constr_pattern_eq ty1 ty2
+| PUninstantiated _, _ -> .
 | (PRef _ | PVar _ | PEvar _ | PRel _ | PApp _ | PSoApp _
    | PLambda _ | PProd _ | PLetIn _ | PSort _ | PMeta _
    | PIf _ | PCase _ | PFix _ | PCoFix _ | PProj _ | PInt _
@@ -80,7 +81,8 @@ and rec_declaration_eq (n1, c1, r1) (n2, c2, r2) =
   Array.equal constr_pattern_eq c1 c2 &&
   Array.equal constr_pattern_eq r1 r2
 
-let rec occurn_pattern n = function
+let rec occurn_pattern : 'a. _ -> 'a constr_pattern_r -> _
+  = fun (type a) n (p:a constr_pattern_r) -> match p with
   | PRel p -> Int.equal n p
   | PApp (f,args) ->
       (occurn_pattern n f) || (Array.exists (occurn_pattern n) args)
@@ -106,12 +108,13 @@ let rec occurn_pattern n = function
      Array.exists (occurn_pattern n) tl || Array.exists (occurn_pattern (n+Array.length tl)) bl
   | PArray (t,def,ty) ->
     Array.exists (occurn_pattern n) t || occurn_pattern n def || occurn_pattern n ty
+  | PUninstantiated (PGenarg _) -> false
 
 let noccurn_pattern n c = not (occurn_pattern n c)
 
 exception BoundPattern;;
 
-let rec head_pattern_bound t =
+let rec head_pattern_bound (t:constr_pattern) =
   match t with
     | PProd (_,_,b)  -> head_pattern_bound b
     | PLetIn (_,_,_,b) -> head_pattern_bound b
@@ -126,6 +129,7 @@ let rec head_pattern_bound t =
     | PLambda _ -> raise BoundPattern
     | PCoFix _ | PInt _ | PFloat _ | PArray _ ->
       anomaly ~label:"head_pattern_bound" (Pp.str "not a type.")
+    | PUninstantiated _ -> .
 
 let head_of_constr_reference sigma c = match EConstr.kind sigma c with
   | Const (sp,_) -> GlobRef.ConstRef sp
@@ -224,11 +228,11 @@ let pattern_of_constr ~broken env sigma t =
   pattern_of_constr env t
 
 let legacy_bad_pattern_of_constr env sigma c : constr_pattern = pattern_of_constr ~broken:true env sigma c
-let pattern_of_constr env sigma c : constr_pattern = pattern_of_constr ~broken:false env sigma c
+let pattern_of_constr env sigma c = pattern_of_constr ~broken:false env sigma c
 
 (* To process patterns, we need a translation without typing at all. *)
 
-let map_pattern_with_binders g f l = function
+let map_pattern_with_binders_gen (type a b) g f fgen l : a constr_pattern_r -> b constr_pattern_r = function
   | PApp (p,pl) -> PApp (f l p, Array.map (f l) pl)
   | PSoApp (n,pl) -> PSoApp (n, List.map (f l) pl)
   | PLambda (n,a,b) -> PLambda (n,f l a,f (g n l) b)
@@ -248,9 +252,17 @@ let map_pattern_with_binders g f l = function
      let l' = Array.fold_left (fun l na -> g na l) l lna in
      PCoFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl))
   | PArray (t,def,ty) -> PArray (Array.map (f l) t, f l def, f l ty)
+  | PEvar (ev,ps) -> PEvar (ev, List.map (f l) ps)
+  | PUninstantiated (PGenarg _ as x) -> fgen (x:a uninstantiated_pattern)
   (* Non recursive *)
-  | (PVar _ | PEvar _ | PRel _ | PRef _  | PSort _  | PMeta _ | PInt _
-     | PFloat _ as x) -> x
+  | (PVar _ | PRel _ | PRef _  | PSort _  | PMeta _ | PInt _
+    | PFloat _ as x) -> x
+
+let map_pattern_with_binders (type a) g f l (p:a constr_pattern_r) : a constr_pattern_r =
+  let fgen : a uninstantiated_pattern -> a constr_pattern_r = function
+    | PGenarg _ as x -> PUninstantiated x
+  in
+  map_pattern_with_binders_gen g f fgen l p
 
 let rec liftn_pattern k n = function
   | PRel i as x -> if i >= n then PRel (i+k) else x
@@ -258,7 +270,9 @@ let rec liftn_pattern k n = function
 
 let lift_pattern k = liftn_pattern k 1
 
-let rec subst_pattern env sigma subst pat =
+let rec subst_pattern
+  : 'a. _ -> _ -> _ -> 'a constr_pattern_r -> 'a constr_pattern_r
+  = fun (type a) env sigma subst (pat: a constr_pattern_r) ->
   match pat with
   | PRef ref ->
     let ref',t = subst_global subst ref in
@@ -271,6 +285,7 @@ let rec subst_pattern env sigma subst pat =
   | PRel _
   | PInt _
   | PFloat _ -> pat
+  | PUninstantiated (PGenarg g) -> PUninstantiated (PGenarg (Genarg.generic_substitute subst g))
   | PProj (p,c) ->
       let p' = Projection.map (subst_mind subst) p in
       let c' = subst_pattern env sigma subst c in
@@ -358,8 +373,33 @@ let mkPLambda_or_LetIn (na,_,bo,t) c =
   | None -> mkPLambda na t c
   | Some b -> mkPLetIn na b (Some t) c
 
-let it_mkPProd_or_LetIn = List.fold_left (fun c d -> mkPProd_or_LetIn d c)
-let it_mkPLambda_or_LetIn = List.fold_left (fun c d -> mkPLambda_or_LetIn d c)
+let it_mkPProd_or_LetIn x y = List.fold_left (fun c d -> mkPProd_or_LetIn d c) x y
+let it_mkPLambda_or_LetIn x y = List.fold_left (fun c d -> mkPLambda_or_LetIn d c) x y
+
+type 'a pat_interp_fun = Environ.env -> Evd.evar_map -> Ltac_pretype.ltac_var_map
+  -> 'a -> Pattern.constr_pattern
+
+module InterpPatObj =
+struct
+  type (_, 'g, _) obj = 'g pat_interp_fun
+  let name = "interp_pat"
+  let default _ = None
+end
+
+module InterpPat = Genarg.Register(InterpPatObj)
+
+let interp_pat = InterpPat.obj
+
+let register_interp_pat = InterpPat.register0
+
+let interp_pattern env sigma ist p =
+  let fgen = function
+    | PGenarg (GenArg (Glbwit tag,g)) -> interp_pat tag env sigma ist g
+  in
+  let rec aux p =
+    map_pattern_with_binders_gen (fun _ () -> ()) (fun () p -> aux p) fgen () p
+  in
+  aux p
 
 let err ?loc pp = user_err ?loc pp
 
@@ -385,7 +425,9 @@ let in_cast_type loc = function
        Alternatively we could use the loc of the meta, or the loc of the innermost cast. *)
     v
 
-let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function
+let pat_of_raw (type pkind) (kind:pkind pattern_kind) metas vars p =
+
+let rec pat_of_raw metas vars : _ -> pkind constr_pattern_r = DAst.with_loc_val (fun ?loc -> function
   | GVar id ->
       (try PRel (List.index Name.equal (Name id) vars)
        with Not_found -> PVar id)
@@ -426,11 +468,19 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function
      (try PSort (Glob_ops.glob_sort_family gs)
       with Glob_ops.ComplexSort -> user_err ?loc (str "Unexpected universe in pattern."))
   | GHole _ -> PMeta None
-  | GGenarg _ -> CErrors.user_err ?loc Pp.(str "Quotation not supported in pattern.")
+  | GGenarg (GenArg (Glbwit tag, _) as g) -> begin match kind with
+      | Uninstantiated ->
+        let () = if not (InterpPat.mem tag) then
+            let name = Genarg.(ArgT.repr (get_arg_tag tag)) in
+            user_err ?loc (str "This quotation is not supported in patterns (" ++ str name ++ str ").")
+        in
+        PUninstantiated (PGenarg g)
+      | Any -> user_err ?loc (str "Quotations not allowed in this pattern.")
+    end
   | GCast (c,_,t) ->
       let () =
         (* Checks that there are no pattern variables in the type *)
-        let _ : constr_pattern = pat_of_raw (in_cast_type t.loc metas) vars t in
+        let _ : pkind constr_pattern_r = pat_of_raw (in_cast_type t.loc metas) vars t in
         ()
       in
       warn_cast_in_pattern ?loc ();
@@ -556,7 +606,14 @@ and pats_of_glob_branches loc metas vars ind brs =
   in
   get_pat Int.Set.empty brs
 
+in pat_of_raw metas vars p
+
 let pattern_of_glob_constr c =
   let metas = ref Id.Set.empty in
-  let p = pat_of_raw (Metas metas) [] c in
+  let p = pat_of_raw Any (Metas metas) [] c in
+  (!metas, p)
+
+let uninstantiated_pattern_of_glob_constr c =
+  let metas = ref Id.Set.empty in
+  let p = pat_of_raw Uninstantiated (Metas metas) [] c in
   (!metas, p)
diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli
index 1a6289e35aff..db43ec26e52b 100644
--- a/pretyping/patternops.mli
+++ b/pretyping/patternops.mli
@@ -18,9 +18,9 @@ open EConstr
 
 val constr_pattern_eq : constr_pattern -> constr_pattern -> bool
 
-val subst_pattern : Environ.env -> Evd.evar_map -> substitution -> constr_pattern -> constr_pattern
+val subst_pattern : Environ.env -> Evd.evar_map -> substitution -> 'i constr_pattern_r -> 'i constr_pattern_r
 
-val noccurn_pattern : int -> constr_pattern -> bool
+val noccurn_pattern : int -> _ constr_pattern_r -> bool
 
 exception BoundPattern
 
@@ -49,10 +49,20 @@ val legacy_bad_pattern_of_constr : Environ.env -> Evd.evar_map -> EConstr.constr
    a pattern; variables bound in [l] are replaced by the pattern to which they
     are bound *)
 
-val pattern_of_glob_constr : glob_constr ->
-      Id.Set.t * constr_pattern
+val pattern_of_glob_constr : glob_constr -> Id.Set.t * constr_pattern
+
+val uninstantiated_pattern_of_glob_constr : glob_constr -> Id.Set.t * [`uninstantiated] constr_pattern_r
 
 val map_pattern_with_binders : (Name.t -> 'a -> 'a) ->
-  ('a -> constr_pattern -> constr_pattern) -> 'a -> constr_pattern -> constr_pattern
+  ('a -> 'i constr_pattern_r -> 'i constr_pattern_r) -> 'a -> 'i constr_pattern_r -> 'i constr_pattern_r
+
+val lift_pattern : int -> 'i constr_pattern_r -> 'i constr_pattern_r
+
+(** Interp genargs *)
+
+type 'a pat_interp_fun = Environ.env -> Evd.evar_map -> Ltac_pretype.ltac_var_map
+  -> 'a -> Pattern.constr_pattern
+
+val interp_pattern : [`uninstantiated] constr_pattern_r pat_interp_fun
 
-val lift_pattern : int -> constr_pattern -> constr_pattern
+val register_interp_pat : (_, 'g, _) Genarg.genarg_type -> 'g pat_interp_fun -> unit
diff --git a/printing/printer.mli b/printing/printer.mli
index 3e984ad29d69..9b62b36b9440 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -109,9 +109,9 @@ val pr_lglob_constr_env    : env -> evar_map -> 'a glob_constr_g -> Pp.t
 
 val pr_glob_constr_env     : env -> evar_map -> 'a glob_constr_g -> Pp.t
 
-val pr_lconstr_pattern_env : env -> evar_map -> constr_pattern -> Pp.t
+val pr_lconstr_pattern_env : env -> evar_map -> _ constr_pattern_r -> Pp.t
 
-val pr_constr_pattern_env  : env -> evar_map -> constr_pattern -> Pp.t
+val pr_constr_pattern_env  : env -> evar_map -> _ constr_pattern_r -> Pp.t
 
 val pr_cases_pattern       : cases_pattern -> Pp.t
 
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index 8c7b7bad54c9..878a1f538962 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -35,7 +35,7 @@ let eta_reduce = Reductionops.shrink_eta
 
 (* TODO: instead of doing that on patterns we should try to perform it on terms
    before translating them into patterns in Hints. *)
-let rec eta_reduce_pat p = match p with
+let rec eta_reduce_pat (p:constr_pattern) = match p with
 | PLambda (_, _, q) ->
   let f, cl = match eta_reduce_pat q with
   | PApp (f, cl) -> f, cl
@@ -54,6 +54,7 @@ let rec eta_reduce_pat p = match p with
 | PRef _ | PVar _ | PEvar _ | PRel _ | PApp _ | PSoApp _ | PProj _ | PProd _
 | PLetIn _ | PSort _ | PMeta _ | PIf _ | PCase _ | PFix _ | PCoFix _ | PInt _
 | PFloat _ | PArray _ -> p
+| PUninstantiated _ -> .
 
 let decomp_pat p =
   let rec decrec acc = function
diff --git a/test-suite/bugs/bug_11641.v b/test-suite/bugs/bug_11641.v
new file mode 100644
index 000000000000..ddf2d53c5b7c
--- /dev/null
+++ b/test-suite/bugs/bug_11641.v
@@ -0,0 +1,28 @@
+Require Import Ltac2.Ltac2.
+
+Fail Ltac2 my_change1 (a : constr) (b : constr) :=
+  change $a with $b.
+
+Fail Ltac2 my_change2 (a:preterm) (b:constr) :=
+  change $preterm:a with $b.
+
+(* This is pretty bad, maybe $x should mean $pattern:x in patterns?
+   Main question is if we allow preterm in pattern, is
+   "fun x => let y := preterm:($x) in pattern:($preterm:y)"
+   going to be confusing? (x must be constr, and we error at runtime??)
+
+   Instead don't allow preterms, instead expose "pattern_of_preterm : preterm -> pattern",
+   having runtime errors there seems more sensible than with the quotation.
+ *)
+Ltac2 my_change3 (a:pattern) (b:constr) :=
+  change $pattern:a with $b.
+
+Fail Ltac2 dummy x := preterm:($pattern:x).
+
+Goal id True -> False.
+  Fail match! goal with [ |- True -> False ] => () end.
+  my_change3 pat:(id True) constr:(True).
+  match! goal with [ |- True -> False ] => () end.
+
+  Fail let a := preterm:(id True) in change $preterm:a with True.
+Abort.