Adapt to coq/coq#19646 (wit_binders and wit_withtac are vernac argume…

…nts)
ejgallego · Oct 9, 2024 · e442528 · e442528
1 parent f98b653
commit e442528
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/serlib/plugins/funind/ser_g_indfun.ml b/serlib/plugins/funind/ser_g_indfun.ml
@@ -79,7 +79,7 @@ module WFFD = struct
 end
 
 let ser_wit_function_fix_definition =
-  let module M = Ser_genarg.GS0(WFFD) in M.genser
+  let module M = Ser_genarg.GSV(WFFD) in M.genser
 
 module WAU = struct
   type raw = Constrexpr.constr_expr list

diff --git a/serlib/plugins/ltac/ser_tacarg.ml b/serlib/plugins/ltac/ser_tacarg.ml
@@ -216,7 +216,7 @@ module GT0 = struct
   [@@deriving sexp,hash,compare]
 end
 
-let ser_wit_binders = let module M = Ser_genarg.GS0(GT0) in M.genser
+let ser_wit_binders = let module M = Ser_genarg.GSV(GT0) in M.genser
 
 let wit_glob_constr_with_bindings = Ltac_plugin.G_rewrite.wit_glob_constr_with_bindings
 
@@ -265,7 +265,7 @@ module SWWT = struct
   type t = Ser_tacexpr.raw_tactic_expr option
   [@@deriving sexp,hash,compare]
 end
-let ser_wit_withtac = let module M = Ser_genarg.GS0(SWWT) in M.genser
+let ser_wit_withtac = let module M = Ser_genarg.GSV(SWWT) in M.genser
 
 (* extraargs *)