Merge pull request #424 from ppedrot/fast-namegen-detyping

Adapt w.r.t. coq/coq#19481.
rocq-archive · Sep 2, 2024 · 32c50bb · 32c50bb
2 parents b85cd3d + 271fe61
commit 32c50bb
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/sertop/sername.ml b/sertop/sername.ml
@@ -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);