From ae34d334f0694cd08b70fd088228156a23b31ef9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Wed, 14 Feb 2024 12:44:53 +0100 Subject: [PATCH] Adapt w.r.t. coq/coq#18664. --- serlib/plugins/ltac/ser_tacarg.ml | 16 ++-------------- 1 file changed, 2 insertions(+), 14 deletions(-) diff --git a/serlib/plugins/ltac/ser_tacarg.ml b/serlib/plugins/ltac/ser_tacarg.ml index dee6a84a..ed4ce6d4 100644 --- a/serlib/plugins/ltac/ser_tacarg.ml +++ b/serlib/plugins/ltac/ser_tacarg.ml @@ -215,24 +215,13 @@ let ser_wit_hintbases = let module M = Ser_genarg.GS(A16) in M.genser module A17 = struct type raw = Ser_libnames.qualid Ser_hints.hints_path_gen [@@deriving sexp,hash,compare] - type glb = Ser_hints.hints_path + type glb = unit [@@deriving sexp,hash,compare] - type top = Ser_hints.hints_path + type top = unit [@@deriving sexp,hash,compare] end let ser_wit_hintbases_path = let module M = Ser_genarg.GS(A17) in M.genser -module A18 = struct - type raw = Libnames.qualid Hints.hints_path_atom_gen - [@@deriving sexp,hash,compare] - type glb = Names.GlobRef.t Hints.hints_path_atom_gen - [@@deriving sexp,hash,compare] - type top = Names.GlobRef.t Hints.hints_path_atom_gen - [@@deriving sexp,hash,compare] -end - -let ser_wit_hintbases_path_atom = let module M = Ser_genarg.GS(A18) in M.genser - module A19 = struct type raw = string list option [@@deriving sexp,hash,compare] @@ -447,7 +436,6 @@ let register () = Ser_genarg.register_genser G_auto.wit_auto_using ser_wit_auto_using; Ser_genarg.register_genser G_auto.wit_hintbases ser_wit_hintbases; Ser_genarg.register_genser G_auto.wit_hints_path ser_wit_hintbases_path; - Ser_genarg.register_genser G_auto.wit_hints_path_atom ser_wit_hintbases_path_atom; Ser_genarg.register_genser G_auto.wit_opthints ser_wit_opthints; Ser_genarg.register_genser G_rewrite.wit_binders G_rewrite.ser_wit_binders;