Merge pull request #863 from SkySkimmer/del-unused-grammar

Adapt to coq/coq#19726 (removed some unused genargs)
ejgallego · Oct 19, 2024 · fae278e · fae278e
2 parents 090410c + 7a7ee41
commit fae278e
Showing 1 changed file with 0 additions and 13 deletions.
diff --git a/serlib/plugins/funind/ser_g_indfun.ml b/serlib/plugins/funind/ser_g_indfun.ml
@@ -81,20 +81,7 @@ end
 let ser_wit_function_fix_definition =
   let module M = Ser_genarg.GSV(WFFD) in M.genser
 
-module WAU = struct
-  type raw = Constrexpr.constr_expr list
-  [@@deriving sexp,hash,compare]
-  type glb = Genintern.glob_constr_and_expr list
-  [@@deriving sexp,hash,compare]
-  type top = EConstr.constr list
-  [@@deriving sexp,hash,compare]
-end
-
-let ser_wit_auto_using' = let module M = Ser_genarg.GS(WAU) in M.genser
-
 let register () =
-  Ser_genarg.register_genser Funind_plugin.G_indfun.wit_auto_using' ser_wit_auto_using';
-  Ser_genarg.register_genser Funind_plugin.G_indfun.wit_constr_comma_sequence' ser_wit_auto_using';
   Ser_genarg.register_genser Funind_plugin.G_indfun.wit_with_names ser_wit_with_names;
   Ser_genarg.register_genser Funind_plugin.G_indfun.wit_fun_ind_using ser_wit_fun_ind_using;
   Ser_genarg.register_genser Funind_plugin.G_indfun.wit_fun_scheme_arg ser_wit_fun_scheme_arg;