Merge PR #11141: Moving the diversity of constr printers to a label style

Ack-by: SkySkimmer
Reviewed-by: ejgallego

14 files changed, 152 insertions, 104 deletions

diff --git a/dev/ci/user-overlays/11141-herbelin-master+labelled-pr_lconstr-and-co.sh b/dev/ci/user-overlays/11141-herbelin-master+labelled-pr_lconstr-and-co.sh
new file mode 100644
index 0000000000..fb66217487
--- /dev/null
+++ b/dev/ci/user-overlays/11141-herbelin-master+labelled-pr_lconstr-and-co.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "11141" ] || [ "$CI_BRANCH" = "master+labelled-pr_lconstr-and-co" ]; then
+
+    quickchick_CI_REF=master+adapt-coq-pr11141
+    quickchick_CI_GITURL=https://github.com/herbelin/QuickChick
+
+fi
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 7d394c3401..04b20c6889 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -1,5 +1,15 @@
 ## Changes between Coq 8.11 and Coq 8.12
 
+### ML API
+
+Printers:
+
+- Functions such as Printer.pr_lconstr_goal_style_env have been
+  removed, use instead functions such as pr_lconstr with label
+  `goal_concl_style:true`. Functions such as
+  Constrextern.extern_constr which were taking a boolean argument for
+  the goal style now take instead a label.
+
 ## Changes between Coq 8.10 and Coq 8.11
 
 ### ML API
diff --git a/ide/idetop.ml b/ide/idetop.ml
index 7e55eb4d13..7d92cff365 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -196,7 +196,7 @@ let process_goal sigma g =
   let min_env = Environ.reset_context env in
   let id = Goal.uid g in
   let ccl =
-    pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g)
+    pr_letype_env ~goal_concl_style:true env sigma (Goal.V82.concl sigma g)
   in
   let process_hyp d (env,l) =
     let d' = CompactedDecl.to_named_context d in
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index a31dddbbd5..28f4f5aed6 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1199,7 +1199,15 @@ let extern_glob_type vars c =
 (******************************************************************)
 (* Main translation function from constr -> constr_expr *)
 
-let extern_constr_gen lax goal_concl_style scopt env sigma t =
+let extern_constr ?lax ?(inctx=false) ?scope env sigma t =
+  let r = Detyping.detype Detyping.Later ?lax false Id.Set.empty env sigma t in
+  let vars = vars_of_env env in
+  extern inctx (InConstrEntrySomeLevel,(scope,[])) vars r
+
+let extern_constr_in_scope ?lax ?inctx scope env sigma t =
+  extern_constr ?lax ?inctx ~scope env sigma t
+
+let extern_type ?lax ?(goal_concl_style=false) env sigma t =
   (* "goal_concl_style" means do alpha-conversion using the "goal" convention *)
   (* i.e.: avoid using the names of goal/section/rel variables and the short *)
   (* names of global definitions of current module when computing names for *)
@@ -1208,30 +1216,18 @@ let extern_constr_gen lax goal_concl_style scopt env sigma t =
   (* those goal/section/rel variables that occurs in the subterm under *)
   (* consideration; see namegen.ml for further details *)
   let avoid = if goal_concl_style then vars_of_env env else Id.Set.empty in
-  let r = Detyping.detype Detyping.Later ~lax:lax goal_concl_style avoid env sigma t in
-  let vars = vars_of_env env in
-  extern false (InConstrEntrySomeLevel,(scopt,[])) vars r
-
-let extern_constr_in_scope goal_concl_style scope env sigma t =
-  extern_constr_gen false goal_concl_style (Some scope) env sigma t
-
-let extern_constr ?(lax=false) goal_concl_style env sigma t =
-  extern_constr_gen lax goal_concl_style None env sigma t
-
-let extern_type goal_concl_style env sigma t =
-  let avoid = if goal_concl_style then vars_of_env env else Id.Set.empty in
-  let r = Detyping.detype Detyping.Later goal_concl_style avoid env sigma t in
+  let r = Detyping.detype Detyping.Later ?lax goal_concl_style avoid env sigma t in
   extern_glob_type (vars_of_env env) r
 
 let extern_sort sigma s = extern_glob_sort (detype_sort sigma s)
 
-let extern_closed_glob ?lax goal_concl_style env sigma t =
+let extern_closed_glob ?lax ?(goal_concl_style=false) ?(inctx=false) ?scope env sigma t =
   let avoid = if goal_concl_style then vars_of_env env else Id.Set.empty in
   let r =
     Detyping.detype_closed_glob ?lax goal_concl_style avoid env sigma t
   in
   let vars = vars_of_env env in
-  extern false (InConstrEntrySomeLevel,(None,[])) vars r
+  extern inctx (InConstrEntrySomeLevel,(scope,[])) vars r
 
 (******************************************************************)
 (* Main translation function from pattern -> constr_expr *)
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index aa6aa5f5f9..fa263cbeb7 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -28,7 +28,8 @@ val extern_glob_constr : Id.Set.t -> 'a glob_constr_g -> constr_expr
 val extern_glob_type : Id.Set.t -> 'a glob_constr_g -> constr_expr
 val extern_constr_pattern : names_context -> Evd.evar_map ->
   constr_pattern -> constr_expr
-val extern_closed_glob : ?lax:bool -> bool -> env -> Evd.evar_map -> closed_glob_constr -> constr_expr
+val extern_closed_glob : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool -> ?scope:scope_name ->
+  env -> Evd.evar_map -> closed_glob_constr -> constr_expr
 
 (** If [b=true] in [extern_constr b env c] then the variables in the first
    level of quantification clashing with the variables in [env] are renamed.
@@ -36,10 +37,12 @@ val extern_closed_glob : ?lax:bool -> bool -> env -> Evd.evar_map -> closed_glob
     env, sigma
 *)
 
-val extern_constr : ?lax:bool -> bool -> env -> Evd.evar_map -> constr -> constr_expr
-val extern_constr_in_scope : bool -> scope_name -> env -> Evd.evar_map -> constr -> constr_expr
+val extern_constr : ?lax:bool -> ?inctx:bool -> ?scope:scope_name ->
+  env -> Evd.evar_map -> constr -> constr_expr
+val extern_constr_in_scope : ?lax:bool -> ?inctx:bool -> scope_name ->
+  env -> Evd.evar_map -> constr -> constr_expr
 val extern_reference : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid
-val extern_type : bool -> env -> Evd.evar_map -> types -> constr_expr
+val extern_type : ?lax:bool -> ?goal_concl_style:bool -> env -> Evd.evar_map -> types -> constr_expr
 val extern_sort : Evd.evar_map -> Sorts.t -> glob_sort
 val extern_rel_context : constr option -> env -> Evd.evar_map ->
   rel_context -> local_binder_expr list
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 9ff05c33e4..7d84ee6851 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -231,7 +231,7 @@ let print_cmap map=
   let print_entry c l s=
     let env = Global.env () in
     let sigma = Evd.from_env env in
-    let xc=Constrextern.extern_constr false env sigma (EConstr.of_constr c) in
+    let xc=Constrextern.extern_constr env sigma (EConstr.of_constr c) in
       str "| " ++
       prlist Printer.pr_global l ++
       str " : " ++
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 6add56dd5b..58efee1518 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -142,7 +142,7 @@ let recompute_binder_list fixpoint_exprl =
         with rec_order = ComFixpoint.adjust_rec_order ~structonly:false fix.binders fix.rec_order }) fixpoint_exprl in
   let ((_,_,_,typel),_,ctx,_) = ComFixpoint.interp_fixpoint ~cofix:false fixl in
   let constr_expr_typel =
-    with_full_print (List.map (fun c -> Constrextern.extern_constr false (Global.env ()) (Evd.from_ctx ctx) (EConstr.of_constr c))) typel in
+    with_full_print (List.map (fun c -> Constrextern.extern_constr (Global.env ()) (Evd.from_ctx ctx) (EConstr.of_constr c))) typel in
   let fixpoint_exprl_with_new_bl =
     List.map2 (fun ({ Vernacexpr.binders } as fp) fix_typ ->
         let binders, rtype = rebuild_bl [] binders fix_typ in
@@ -1902,8 +1902,8 @@ let make_graph (f_ref : GlobRef.t) =
      let env = Global.env () in
      let extern_body,extern_type =
        with_full_print (fun () ->
-           (Constrextern.extern_constr false env sigma (EConstr.of_constr body),
-            Constrextern.extern_type false env sigma
+           (Constrextern.extern_constr env sigma (EConstr.of_constr body),
+            Constrextern.extern_type env sigma
               (EConstr.of_constr (*FIXME*) c_body.Declarations.const_type)
            )
          )
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 6df068883c..0e8c225a8f 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -1273,7 +1273,7 @@ let pr_intro_pattern_env p = Genprint.TopPrinterNeedsContext (fun env sigma ->
   Miscprint.pr_intro_pattern print_constr p)
 
 let pr_red_expr_env r = Genprint.TopPrinterNeedsContext (fun env sigma ->
-  pr_red_expr env sigma (pr_econstr_env, pr_leconstr_env,
+  pr_red_expr env sigma ((fun e -> pr_econstr_env e), (fun e -> pr_leconstr_env e),
                          pr_evaluable_reference_env env, pr_constr_pattern_env) r)
 
 let pr_bindings_env bl = Genprint.TopPrinterNeedsContext (fun env sigma ->
diff --git a/printing/printer.ml b/printing/printer.ml
index a85e268306..bb54f587fd 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -76,25 +76,22 @@ let () =
    and only names of goal/section variables and rel names that do
    _not_ occur in the scope of the binder to be printed are avoided. *)
 
-let pr_econstr_n_core goal_concl_style env sigma n t =
-  pr_constr_expr_n env sigma n (extern_constr goal_concl_style env sigma t)
-let pr_econstr_core goal_concl_style env sigma t =
-  pr_constr_expr env sigma (extern_constr goal_concl_style env sigma t)
-let pr_leconstr_core = Proof_diffs.pr_leconstr_core
-
-let pr_constr_n_env env sigma n c = pr_econstr_n_core false env sigma n (EConstr.of_constr c)
+let pr_econstr_n_env ?lax ?inctx ?scope env sigma n t =
+  pr_constr_expr_n env sigma n (extern_constr ?lax ?inctx ?scope env sigma t)
+let pr_econstr_env ?lax ?inctx ?scope env sigma t =
+  pr_constr_expr env sigma (extern_constr ?lax ?inctx ?scope env sigma t)
+let pr_leconstr_env = Proof_diffs.pr_leconstr_env
+
+let pr_constr_n_env ?lax ?inctx ?scope env sigma n c =
+  pr_econstr_n_env ?lax ?inctx ?scope env sigma n (EConstr.of_constr c)
+let pr_constr_env ?lax ?inctx ?scope env sigma c =
+  pr_econstr_env ?lax ?inctx ?scope env sigma (EConstr.of_constr c)
 let pr_lconstr_env = Proof_diffs.pr_lconstr_env
-let pr_constr_env env sigma c = pr_econstr_core false env sigma (EConstr.of_constr c)
-
-let pr_lconstr_goal_style_env env sigma c = pr_leconstr_core true env sigma (EConstr.of_constr c)
-let pr_constr_goal_style_env env sigma c = pr_econstr_core true env sigma (EConstr.of_constr c)
 
-let pr_econstr_n_env env sigma c = pr_econstr_n_core false env sigma c
-let pr_leconstr_env env sigma c = pr_leconstr_core false env sigma c
-let pr_econstr_env env sigma c = pr_econstr_core false env sigma c
-
-let pr_open_lconstr_env env sigma (_,c) = pr_leconstr_env env sigma c
-let pr_open_constr_env env sigma (_,c) = pr_econstr_env env sigma c
+let pr_open_lconstr_env ?lax ?inctx ?scope env sigma (_,c) =
+  pr_leconstr_env ?lax ?inctx ?scope env sigma c
+let pr_open_constr_env ?lax ?inctx ?scope env sigma (_,c) =
+  pr_econstr_env ?lax ?inctx ?scope env sigma c
 
 let pr_constr_under_binders_env_gen pr env sigma (ids,c) =
   (* Warning: clashes can occur with variables of same name in env but *)
@@ -106,16 +103,14 @@ let pr_constr_under_binders_env_gen pr env sigma (ids,c) =
 let pr_constr_under_binders_env = pr_constr_under_binders_env_gen pr_econstr_env
 let pr_lconstr_under_binders_env = pr_constr_under_binders_env_gen pr_leconstr_env
 
-let pr_etype_core goal_concl_style env sigma t =
-  pr_constr_expr env sigma (extern_type goal_concl_style env sigma t)
-let pr_letype_core = Proof_diffs.pr_letype_core
-
-let pr_ltype_env env sigma c = pr_letype_core false env sigma (EConstr.of_constr c)
-let pr_type_env env sigma c = pr_etype_core false env sigma (EConstr.of_constr c)
+let pr_etype_env ?lax ?goal_concl_style env sigma t =
+  pr_constr_expr env sigma (extern_type ?lax ?goal_concl_style env sigma t)
+let pr_letype_env = Proof_diffs.pr_letype_env
 
-let pr_etype_env env sigma c = pr_etype_core false env sigma c
-let pr_letype_env env sigma c = pr_letype_core false env sigma c
-let pr_goal_concl_style_env env sigma c = pr_letype_core true env sigma c
+let pr_type_env ?lax ?goal_concl_style env sigma c =
+  pr_etype_env ?lax ?goal_concl_style env sigma (EConstr.of_constr c)
+let pr_ltype_env ?lax ?goal_concl_style env sigma c =
+  pr_letype_env ?lax ?goal_concl_style env sigma (EConstr.of_constr c)
 
 let pr_ljudge_env env sigma j =
   (pr_leconstr_env env sigma j.uj_val, pr_leconstr_env env sigma j.uj_type)
@@ -125,10 +120,10 @@ let pr_lglob_constr_env env c =
 let pr_glob_constr_env env c =
   pr_constr_expr env (Evd.from_env env) (extern_glob_constr (Termops.vars_of_env env) c)
 
-let pr_closed_glob_n_env env sigma n c =
-  pr_constr_expr_n env sigma n (extern_closed_glob false env sigma c)
-let pr_closed_glob_env env sigma c =
-  pr_constr_expr env sigma (extern_closed_glob false env sigma c)
+let pr_closed_glob_n_env ?lax ?goal_concl_style ?inctx ?scope env sigma n c =
+  pr_constr_expr_n env sigma n (extern_closed_glob ?lax ?goal_concl_style ?inctx ?scope env sigma c)
+let pr_closed_glob_env ?lax ?goal_concl_style ?inctx ?scope env sigma c =
+  pr_constr_expr env sigma (extern_closed_glob ?lax ?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)
@@ -141,7 +136,7 @@ let pr_cases_pattern t =
 let pr_sort sigma s = pr_glob_sort (extern_sort sigma s)
 
 let () = Termops.Internal.set_print_constr
-  (fun env sigma t -> pr_lconstr_expr env sigma (extern_constr ~lax:true false env sigma t))
+  (fun env sigma t -> pr_lconstr_expr env sigma (extern_constr ~lax:true env sigma t))
 
 let pr_in_comment x = str "(* " ++ x ++ str " *)"
 
@@ -462,7 +457,7 @@ let pr_goal ?(diffs=false) ?og_s g_s =
     else
       pr_context_of env sigma ++ cut () ++
         str "============================" ++ cut ()  ++
-        pr_goal_concl_style_env env sigma concl
+        pr_letype_env ~goal_concl_style:true env sigma concl
   in
   str "  " ++ v 0 goal
 
@@ -489,7 +484,7 @@ let pr_concl n ?(diffs=false) ?og_s sigma g =
     if diffs then
       Proof_diffs.diff_concl ?og_s sigma g
     else
-      pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g)
+      pr_letype_env ~goal_concl_style:true env sigma (Goal.V82.concl sigma g)
   in
   let header = pr_goal_header (int n) sigma g in
   header ++ str " is:" ++ cut () ++ str" "  ++ pc
diff --git a/printing/printer.mli b/printing/printer.mli
index 87b09ff755..1d7a25cbb6 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -15,55 +15,93 @@ open Pattern
 open Evd
 open Glob_term
 open Ltac_pretype
+open Notation_term
 
 (** These are the entry points for printing terms, context, tac, ... *)
 
-
 val enable_unfocused_goal_printing: bool ref
 val enable_goal_tags_printing      : bool ref
 val enable_goal_names_printing     : bool ref
 
 (** Terms *)
 
-val pr_lconstr_env         : env -> evar_map -> constr -> Pp.t
-val pr_lconstr_goal_style_env : env -> evar_map -> constr -> Pp.t
+(** Printers for terms.
+
+    The "lconstr" variant does not require parentheses to isolate the
+    expression from the surrounding context (for instance [3 + 4]
+    will be written [3 + 4]). The "constr" variant (w/o "l")
+    enforces parentheses whenever the term is not an atom (for
+    instance, [3] will be written [3] but [3 + 4] will be
+    written [(3 + 4)].
+
+    [~inctx:true] indicates that the term is intended to be printed in
+    a context where its type is known so that a head coercion would be
+    skipped, or implicit arguments inferable from the context will not
+    be made explicit. For instance, if [foo] is declared as a
+    coercion, [foo bar] will be printed as [bar] if [inctx] is [true]
+    and as [foo bar] otherwise.
+
+    [~scope:some_scope_name] indicates that the head of the term is
+    intended to be printed in scope [some_scope_name]. It defaults to
+    [None].
+
+    [~lax:true] is for debugging purpose. It defaults to [~lax:false]. *)
 
-val pr_constr_env          : env -> evar_map -> constr -> Pp.t
-val pr_constr_goal_style_env : env -> evar_map -> constr -> Pp.t
 
-val pr_constr_n_env        : env -> evar_map -> Notation_gram.tolerability -> constr -> Pp.t
+val pr_constr_env          : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> constr -> Pp.t
+val pr_lconstr_env         : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> constr -> Pp.t
+
+val pr_constr_n_env        : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Notation_gram.tolerability -> constr -> Pp.t
 
 (** Same, but resilient to [Nametab] errors. Prints fully-qualified
     names when [shortest_qualid_of_global] has failed. Prints "??"
     in case of remaining issues (such as reference not in env). *)
 
-val safe_pr_lconstr_env         : env -> evar_map -> constr -> Pp.t
-
-val safe_pr_constr_env          : env -> evar_map -> constr -> Pp.t
-
-val pr_econstr_env     : env -> evar_map -> EConstr.t -> Pp.t
-val pr_leconstr_env     : env -> evar_map -> EConstr.t -> Pp.t
+val safe_pr_constr_env  : env -> evar_map -> constr -> Pp.t
+val safe_pr_lconstr_env : env -> evar_map -> constr -> Pp.t
 
-val pr_econstr_n_env    : env -> evar_map -> Notation_gram.tolerability -> EConstr.t -> Pp.t
+val pr_econstr_env      : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> EConstr.t -> Pp.t
+val pr_leconstr_env     : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> EConstr.t -> Pp.t
 
-val pr_etype_env           : env -> evar_map -> EConstr.types -> Pp.t
-val pr_letype_env           : env -> evar_map -> EConstr.types -> Pp.t
+val pr_econstr_n_env    : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Notation_gram.tolerability -> EConstr.t -> Pp.t
 
-val pr_open_constr_env     : env -> evar_map -> open_constr -> Pp.t
+val pr_etype_env        : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> EConstr.types -> Pp.t
+val pr_letype_env       : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> EConstr.types -> Pp.t
 
-val pr_open_lconstr_env    : env -> evar_map -> open_constr -> Pp.t
+val pr_open_constr_env  : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> open_constr -> Pp.t
+val pr_open_lconstr_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> open_constr -> Pp.t
 
 val pr_constr_under_binders_env  : env -> evar_map -> constr_under_binders -> Pp.t
 
 val pr_lconstr_under_binders_env : env -> evar_map -> constr_under_binders -> Pp.t
 
-val pr_goal_concl_style_env : env -> evar_map -> EConstr.types -> Pp.t
-val pr_ltype_env           : env -> evar_map -> types -> Pp.t
-
-val pr_type_env            : env -> evar_map -> types -> Pp.t
-
-val pr_closed_glob_n_env   : env -> evar_map -> Notation_gram.tolerability -> closed_glob_constr -> Pp.t
-val pr_closed_glob_env     : env -> evar_map -> closed_glob_constr -> Pp.t
+(** Printers for types. Types are printed in scope "type_scope" and
+    under the constraint of being of type a sort.
+
+    The "ltype" variant does not require parentheses to isolate the
+    expression from the surrounding context (for instance [nat * bool]
+    will be written [nat * bool]). The "type" variant (w/o "l")
+    enforces parentheses whenever the term is not an atom (for
+    instance, [nat] will be written [nat] but [nat * bool] will be
+    written [(nat * bool)].
+
+    [~goal_concl_style:true] tells to print the type the same way as
+    command [Show] would print a goal. Concretely, it means that all
+    names of goal/section variables and all names of variables
+    referred by de Bruijn indices (if any) in the given environment
+    and all short names of global definitions of the current module
+    must be avoided while printing bound variables. Otherwise, short
+    names of global definitions are printed qualified and only names
+    of goal/section variables and rel names that do _not_ occur in the
+    scope of the binder to be printed are avoided.
+
+    [~lax:true] is for debugging purpose. *)
+
+val pr_ltype_env           : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> types -> Pp.t
+val pr_type_env            : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> types -> Pp.t
+
+val pr_closed_glob_n_env   : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Notation_gram.tolerability -> closed_glob_constr -> Pp.t
+val pr_closed_glob_env     : ?lax:bool -> ?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
 
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index 233163d097..dec87f8071 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -245,18 +245,18 @@ let process_goal sigma g : EConstr.t reified_goal =
   let hyps      = List.map to_tuple hyps in
   { name; ty; hyps; env; sigma };;
 
-let pr_letype_core goal_concl_style env sigma t =
-  Ppconstr.pr_lconstr_expr env sigma (Constrextern.extern_type goal_concl_style env sigma t)
+let pr_letype_env ?lax ?goal_concl_style env sigma t =
+  Ppconstr.pr_lconstr_expr env sigma
+    (Constrextern.extern_type ?lax ?goal_concl_style env sigma t)
 
 let pp_of_type env sigma ty =
-  pr_letype_core true env sigma ty
+  pr_letype_env ~goal_concl_style:true env sigma ty
 
-let pr_leconstr_core goal_concl_style env sigma t =
-  Ppconstr.pr_lconstr_expr env sigma (Constrextern.extern_constr goal_concl_style env sigma t)
+let pr_leconstr_env ?lax ?inctx ?scope env sigma t =
+  Ppconstr.pr_lconstr_expr env sigma (Constrextern.extern_constr ?lax ?inctx ?scope env sigma t)
 
-let pr_lconstr_env env sigma c = pr_leconstr_core false env sigma (EConstr.of_constr c)
-
-let pr_lconstr_env_econstr env sigma c = pr_leconstr_core false env sigma c
+let pr_lconstr_env ?lax ?inctx ?scope env sigma c =
+  pr_leconstr_env ?lax ?inctx ?scope env sigma (EConstr.of_constr c)
 
 let diff_concl ?og_s nsigma ng =
   let open Evd in
@@ -301,7 +301,7 @@ let goal_info goal sigma =
     line_idents := idents :: !line_idents;
     let mid = match body with
     | Some c ->
-      let pb = pr_lconstr_env_econstr env sigma c in
+      let pb = pr_leconstr_env env sigma c in
       let pb = if EConstr.isCast sigma c then surround pb else pb in
       str " := " ++ pb
     | None -> mt() in
@@ -556,7 +556,7 @@ let to_constr pf =
   (* pprf generally has only one element, but it may have more in the derive plugin *)
   let t = List.hd pprf in
   let sigma, env = get_proof_context pf in
-  let x = Constrextern.extern_constr false env sigma t in  (* todo: right options?? *)
+  let x = Constrextern.extern_constr env sigma t in  (* todo: right options?? *)
   x.v
 
 
diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli
index a806ab7123..eebdaccd32 100644
--- a/printing/proof_diffs.mli
+++ b/printing/proof_diffs.mli
@@ -57,9 +57,9 @@ val diff_goal : ?og_s:(Goal.goal sigma) -> Goal.goal -> Evd.evar_map -> Pp.t
 (** Convert a string to a list of token strings using the lexer *)
 val tokenize_string : string -> string list
 
-val pr_letype_core         : bool -> Environ.env -> Evd.evar_map -> EConstr.types -> Pp.t
-val pr_leconstr_core       : bool -> Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t
-val pr_lconstr_env         : env -> evar_map -> constr -> Pp.t
+val pr_letype_env          : ?lax:bool -> ?goal_concl_style:bool -> Environ.env -> Evd.evar_map -> EConstr.types -> Pp.t
+val pr_leconstr_env        : ?lax:bool -> ?inctx:bool -> ?scope:Notation_term.scope_name -> Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t
+val pr_lconstr_env         : ?lax:bool -> ?inctx:bool -> ?scope:Notation_term.scope_name -> env -> evar_map -> constr -> Pp.t
 
 (** Computes diffs for a single conclusion *)
 val diff_concl : ?og_s:Goal.goal sigma -> Evd.evar_map -> Goal.goal -> Pp.t
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 33c9c11350..c44082cd88 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -934,7 +934,7 @@ let is_local_unfold env flags =
 let reduce redexp cl =
   let trace env sigma =
     let open Printer in
-    let pr = (pr_econstr_env, pr_leconstr_env, pr_evaluable_reference, pr_constr_pattern_env) in
+    let pr = ((fun e -> pr_econstr_env e), (fun e -> pr_leconstr_env e), pr_evaluable_reference, pr_constr_pattern_env) in
     Pp.(hov 2 (Ppred.pr_red_expr_env env sigma pr str redexp))
   in
   Proofview.Trace.name_tactic trace begin
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 2e58bf4a93..19ec0a3642 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -117,8 +117,8 @@ let display_eq ~flags env sigma t1 t2 =
   let open Constrextern in
   let t1 = canonize_constr sigma t1 in
   let t2 = canonize_constr sigma t2 in
-  let ct1 = Flags.with_options flags (fun () -> extern_constr false env sigma t1) () in
-  let ct2 = Flags.with_options flags (fun () -> extern_constr false env sigma t2) () in
+  let ct1 = Flags.with_options flags (fun () -> extern_constr env sigma t1) () in
+  let ct2 = Flags.with_options flags (fun () -> extern_constr env sigma t2) () in
   Constrexpr_ops.constr_expr_eq ct1 ct2
 
 (** This function adds some explicit printing flags if the two arguments are
@@ -134,9 +134,9 @@ let rec pr_explicit_aux env sigma t1 t2 = function
     pr_explicit_aux env sigma t1 t2 rem
   else
     let open Constrextern in
-    let ct1 = Flags.with_options flags (fun () -> extern_constr false env sigma t1) ()
+    let ct1 = Flags.with_options flags (fun () -> extern_constr env sigma t1) ()
     in
-    let ct2 = Flags.with_options flags (fun () -> extern_constr false env sigma t2) ()
+    let ct2 = Flags.with_options flags (fun () -> extern_constr env sigma t2) ()
     in
     Ppconstr.pr_lconstr_expr env sigma ct1, Ppconstr.pr_lconstr_expr env sigma ct2
 
@@ -697,7 +697,7 @@ let explain_cannot_find_well_typed_abstraction env sigma p l e =
   str "Abstracting over the " ++
   str (String.plural (List.length l) "term") ++ spc () ++
   hov 0 (pr_enum (fun c -> pr_lconstr_env env sigma (EConstr.to_constr sigma c)) l) ++ spc () ++
-  str "leads to a term" ++ spc () ++ pr_lconstr_goal_style_env env sigma p ++
+  str "leads to a term" ++ spc () ++ pr_ltype_env ~goal_concl_style:true env sigma p ++
   spc () ++ str "which is ill-typed." ++
   (match e with None -> mt () | Some e -> fnl () ++ str "Reason is: " ++ e)
 
@@ -1183,7 +1183,7 @@ let error_ill_formed_constructor env id c v nparams nargs =
 
 let pr_ltype_using_barendregt_convention_env env c =
   (* Use goal_concl_style as an approximation of Barendregt's convention (?) *)
-  quote (pr_goal_concl_style_env env (Evd.from_env env) (EConstr.of_constr c))
+  quote (pr_ltype_env ~goal_concl_style:true env (Evd.from_env env) c)
 
 let error_bad_ind_parameters env c n v1 v2  =
   let pc = pr_ltype_using_barendregt_convention_env env c in
@@ -1338,7 +1338,7 @@ let explain_reduction_tactic_error = function
   | Tacred.InvalidAbstraction (env,sigma,c,(env',e)) ->
       let e = map_ptype_error EConstr.of_constr e in
       str "The abstracted term" ++ spc () ++
-      quote (pr_goal_concl_style_env env sigma c) ++
+      quote (pr_letype_env ~goal_concl_style:true env sigma c) ++
       spc () ++ str "is not well typed." ++ fnl () ++
       explain_type_error env' (Evd.from_env env') e