Merge pull request #586 from SkySkimmer/indirect

Don't pierce Qed in debug message (adapt to coq/coq#18422)
mattam82 · Mar 22, 2024 · 962c005 · 962c005
2 parents e43c620 + eba7646
commit 962c005
Showing 1 changed file with 3 additions and 2 deletions.
diff --git a/src/splitting.ml b/src/splitting.ml
@@ -1174,8 +1174,9 @@ let solve_equations_obligations_program ~pm flags recids loc i sigma hook =
       let hd, args = decompose_app !evd t in
       if EConstr.isRef !evd hd then
         (if !Equations_common.debug then
-           Feedback.msg_debug (str"mapping obligation to " ++ Printer.pr_econstr_env env !evd t ++
-                               Prettyp.print_name env !evd (CAst.make (Constrexpr.AN (Libnames.qualid_of_ident id))) None);
+           Feedback.msg_debug
+             (str"mapping obligation to " ++ Printer.pr_econstr_env env !evd t ++
+              Prettyp.print_about env !evd (CAst.make (Constrexpr.AN (Libnames.qualid_of_ident id))) None);
          let cst, i = EConstr.destConst !evd hd in
          let ctx = Environ.constant_context (Global.env ()) cst in
          let ctx = gather_fresh_context !evd (EConstr.EInstance.kind sigma i) ctx in