Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Adapt w.r.t. coq/coq#18664. #390

Merged
merged 1 commit into from
Feb 19, 2024
Merged

Adapt w.r.t. coq/coq#18664. #390

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 2 additions & 14 deletions serlib/plugins/ltac/ser_tacarg.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down Expand Up @@ -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;
Expand Down
Loading