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#19481. #424

Merged
merged 1 commit into from
Sep 2, 2024
Merged

Adapt w.r.t. coq/coq#19481. #424

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
2 changes: 1 addition & 1 deletion sertop/sername.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,7 @@ let process_line ~pp ~str_pp ~de_bruijn ~body ~doc ~sid line =
| [CoqConstr def_term] ->
let evd = Evd.from_env env in
let edef_term = EConstr.of_constr def_term in
let gdef_term = Detyping.detype Detyping.Now Names.Id.Set.empty env evd edef_term in
let gdef_term = Detyping.detype Detyping.Now env evd edef_term in
Format.pp_set_margin Format.std_formatter 100000;
Format.printf "%s: %!" line;
if str_pp then Format.fprintf Format.std_formatter "\"@[%a@]\" %!" (str_pp_obj env sigma) (CoqConstr def_term);
Expand Down
Loading