Merge pull request #500 from SkySkimmer/pattern-quotations

Adapt to coq/coq#17667 (Genintern.register_subst0 moved to Gensubst)
LPCIC · Nov 15, 2023 · 4587e02 · 4587e02
2 parents f6bed81 + b8e9df2
commit 4587e02
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/coq_elpi_arg_HOAS.ml b/src/coq_elpi_arg_HOAS.ml
@@ -482,7 +482,7 @@ let add_genarg tag pr_raw pr_glob pr_top glob subst interp =
   let wit = Genarg.make0 tag in
   let tag = Geninterp.Val.create tag 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 (fun x -> Ftactic.return @@ Geninterp.Val.Dyn (tag, x))) in
   let () = Geninterp.register_val0 wit (Some (Geninterp.Val.Base tag)) in
   Ltac_plugin.Pptactic.declare_extra_genarg_pprule wit pr_raw pr_glob pr_top;