Merge PR #21095: Ltac2 builtin printers: fix some too-tight precedence levels

Reviewed-by: proux01
Co-authored-by: proux01 <proux01@users.noreply.github.com>

Author: coqbot-app[bot]

plugins/ltac2/tac2extravals.ml

@@ -75,7 +75,7 @@ let () =
   let intern = intern_constr_tacexpr in
   let interp ist c = interp_constr Tac2core.constr_flags ist c in
   let print env sigma c = str "constr:(" ++ Printer.pr_lglob_constr_env env sigma c ++ str ")" in
-  let raw_print env sigma c = str "constr:(" ++ Ppconstr.pr_constr_expr env sigma c ++ str ")" in
+  let raw_print env sigma c = str "constr:(" ++ Ppconstr.pr_lconstr_expr env sigma c ++ str ")" in
   let subst subst c = Detyping.subst_glob_constr (Global.env()) subst c in
   let obj = {
     ml_intern = intern;
@@ -90,7 +90,7 @@ let () =
   let intern = intern_constr_tacexpr in
   let interp ist c = interp_constr Tac2core.open_constr_no_classes_flags ist c in
   let print env sigma c = str "open_constr:(" ++ Printer.pr_lglob_constr_env env sigma c ++ str ")" in
-  let raw_print env sigma c = str "open_constr:(" ++ Ppconstr.pr_constr_expr env sigma c ++ str ")" in
+  let raw_print env sigma c = str "open_constr:(" ++ Ppconstr.pr_lconstr_expr env sigma c ++ str ")" in
   let subst subst c = Detyping.subst_glob_constr (Global.env()) subst c in
   let obj = {
     ml_intern = intern;
@@ -131,7 +131,7 @@ let () =
     Patternops.subst_uninstantiated_pattern env sigma subst c
   in
   let print env sigma pat = str "pat:(" ++ Printer.pr_uninstantiated_lconstr_pattern_env env sigma pat ++ str ")" in
-  let raw_print env sigma pat = str "pat:(" ++ Ppconstr.pr_constr_pattern_expr env sigma pat ++ str ")" in
+  let raw_print env sigma pat = str "pat:(" ++ Ppconstr.pr_lconstr_pattern_expr env sigma pat ++ str ")" in
   let interp env c =
     let ist = to_lvar env in
     Tac2core.pf_apply ~catch_exceptions:true begin fun env sigma ->
@@ -175,7 +175,7 @@ let () =
     in
     hov 2 (str "preterm:(" ++ ppids ++ Printer.pr_lglob_constr_env env sigma c ++ str ")")
   in
-  let raw_print env sigma c = str "preterm:(" ++ Ppconstr.pr_constr_expr env sigma c ++ str ")" in
+  let raw_print env sigma c = str "preterm:(" ++ Ppconstr.pr_lconstr_expr env sigma c ++ str ")" in
   let obj = {
     ml_intern = intern;
     ml_interp = interp;

plugins/ltac2/tac2print.ml

@@ -963,7 +963,7 @@ end
 let () = register_init "preterm" begin fun env sigma c ->
   let c = to_preterm c in
   (* XXX should we get the ltac2 env out of the closure and print it too? Maybe with a debug flag? *)
-  let c = try Printer.pr_closed_glob_env env sigma c with _ -> str "..." in
+  let c = try Printer.pr_closed_lglob_env env sigma c with _ -> str "..." in
   hov 2 (str "preterm:(" ++ c ++ str ")")
 end
 

printing/printer.ml

@@ -110,6 +110,8 @@ let pr_closed_glob_n_env ?goal_concl_style ?inctx ?scope env sigma n c =
   pr_constr_expr_n env sigma n (extern_closed_glob ?goal_concl_style ?inctx ?scope env sigma c)
 let pr_closed_glob_env ?goal_concl_style ?inctx ?scope env sigma c =
   pr_constr_expr env sigma (extern_closed_glob ?goal_concl_style ?inctx ?scope env sigma c)
+let pr_closed_lglob_env ?goal_concl_style ?inctx ?scope env sigma c =
+  pr_lconstr_expr env sigma (extern_closed_glob ?goal_concl_style ?inctx ?scope env sigma c)
 
 let pr_lconstr_pattern_env env sigma c =
   pr_lconstr_pattern_expr env sigma (extern_constr_pattern (Termops.names_of_rel_context env) sigma c)

printing/printer.mli

@@ -103,6 +103,7 @@ val pr_type_env            : ?goal_concl_style:bool -> env -> evar_map -> types
 
 val pr_closed_glob_n_env   : ?goal_concl_style:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Constrexpr.entry_relative_level -> closed_glob_constr -> Pp.t
 val pr_closed_glob_env     : ?goal_concl_style:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> closed_glob_constr -> Pp.t
+val pr_closed_lglob_env    : ?goal_concl_style:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> closed_glob_constr -> Pp.t
 
 val pr_ljudge_env          : env -> evar_map -> EConstr.unsafe_judgment -> Pp.t * Pp.t