aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/doc/changes.md9
-rw-r--r--dev/top_printers.ml22
-rw-r--r--engine/termops.ml11
-rw-r--r--engine/termops.mli32
-rw-r--r--plugins/cc/ccalgo.ml12
-rw-r--r--plugins/ltac/tactic_debug.ml11
-rw-r--r--pretyping/evarconv.ml7
-rw-r--r--pretyping/evardefine.ml2
-rw-r--r--pretyping/globEnv.ml2
-rw-r--r--pretyping/inductiveops.ml2
-rw-r--r--pretyping/pretyping.ml4
-rw-r--r--pretyping/recordops.ml12
-rw-r--r--pretyping/reductionops.ml12
-rw-r--r--pretyping/reductionops.mli4
-rw-r--r--pretyping/unification.ml6
-rw-r--r--printing/printer.ml2
-rw-r--r--proofs/clenv.ml4
-rw-r--r--proofs/tacmach.ml4
-rw-r--r--tactics/class_tactics.ml5
-rw-r--r--tactics/tacticals.ml2
20 files changed, 111 insertions, 54 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 4f3d793ed4..fdeb0abed4 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -1,3 +1,12 @@
+## Changes between Coq 8.9 and Coq 8.10
+
+### ML API
+
+Termops:
+
+- Internal printing functions have been placed under the
+ `Termops.Internal` namespace.
+
## Changes between Coq 8.8 and Coq 8.9
### ML API
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index ab679a71ce..ced6ea2614 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -64,8 +64,14 @@ let ppwf_paths x = pp (Rtree.pp_tree prrecarg x)
let envpp pp = let sigma,env = Pfedit.get_current_context () in pp env sigma
let rawdebug = ref false
let ppevar evk = pp (Evar.print evk)
-let ppconstr x = pp (Termops.print_constr (EConstr.of_constr x))
-let ppeconstr x = pp (Termops.print_constr x)
+let pr_constr t =
+ let sigma, env = Pfedit.get_current_context () in
+ Printer.pr_constr_env env sigma t
+let pr_econstr t =
+ let sigma, env = Pfedit.get_current_context () in
+ Printer.pr_econstr_env env sigma t
+let ppconstr x = pp (pr_constr x)
+let ppeconstr x = pp (pr_econstr x)
let ppconstr_expr x = pp (Ppconstr.pr_constr_expr x)
let ppsconstr x = ppconstr (Mod_subst.force_constr x)
let ppconstr_univ x = Constrextern.with_universes ppconstr x
@@ -95,9 +101,9 @@ let ppidmapgen l = pp (pridmapgen l)
let ppevarsubst = ppidmap (fun id0 -> prset (fun (c,copt,id) ->
hov 0
- (Termops.print_constr (EConstr.of_constr c) ++
+ (pr_constr c ++
(match copt with None -> mt () | Some c -> spc () ++ str "<expanded: " ++
- Termops.print_constr (EConstr.of_constr c) ++ str">") ++
+ pr_constr c ++ str">") ++
(if id = id0 then mt ()
else spc () ++ str "<canonical: " ++ Id.print id ++ str ">"))))
@@ -106,7 +112,7 @@ let ppididmap = ppidmap (fun _ -> Id.print)
let prconstrunderbindersidmap = pridmap (fun _ (l,c) ->
hov 1 (str"[" ++ prlist_with_sep spc Id.print l ++ str"]")
- ++ str "," ++ spc () ++ Termops.print_constr c)
+ ++ str "," ++ spc () ++ pr_econstr c)
let ppconstrunderbindersidmap l = pp (prconstrunderbindersidmap l)
@@ -155,9 +161,9 @@ let ppdelta s = pp (Mod_subst.debug_pr_delta s)
let pp_idpred s = pp (pr_idpred s)
let pp_cpred s = pp (pr_cpred s)
let pp_transparent_state s = pp (pr_transparent_state s)
-let pp_stack_t n = pp (Reductionops.Stack.pr (EConstr.of_constr %> Termops.print_constr) n)
-let pp_cst_stack_t n = pp (Reductionops.Cst_stack.pr n)
-let pp_state_t n = pp (Reductionops.pr_state n)
+let pp_stack_t n = pp (Reductionops.Stack.pr (EConstr.of_constr %> pr_econstr) n)
+let pp_cst_stack_t n = pp (Reductionops.Cst_stack.pr Global.(env()) Evd.empty n)
+let pp_state_t n = pp (Reductionops.pr_state Global.(env()) Evd.empty n)
(* proof printers *)
let pr_evar ev = Pp.int (Evar.repr ev)
diff --git a/engine/termops.ml b/engine/termops.ml
index 710743e92d..efe1525c9a 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -22,6 +22,8 @@ module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration
module CompactedDecl = Context.Compacted.Declaration
+module Internal = struct
+
(* Sorts and sort family *)
let print_sort = function
@@ -98,12 +100,16 @@ let rec pr_constr c = match kind c with
cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++
str"}")
-let term_printer = ref (fun _env _sigma c -> pr_constr (EConstr.Unsafe.to_constr c))
+let debug_print_constr c = pr_constr EConstr.Unsafe.(to_constr c)
+let debug_print_constr_env env sigma c = pr_constr EConstr.(to_constr sigma c)
+let term_printer = ref debug_print_constr_env
+
let print_constr_env env sigma t = !term_printer env sigma t
let print_constr t =
let env = Global.env () in
let evd = Evd.from_env env in
!term_printer env evd t
+
let set_print_constr f = term_printer := f
module EvMap = Evar.Map
@@ -1537,3 +1543,6 @@ let env_rel_context_chop k env =
let ctx1,ctx2 = List.chop k rels in
push_rel_context ctx2 (reset_with_named_context (named_context_val env) env),
ctx1
+end
+
+include Internal
diff --git a/engine/termops.mli b/engine/termops.mli
index 9ce2db9234..aa0f837938 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -311,18 +311,40 @@ val pr_metaset : Metaset.t -> Pp.t
val pr_evar_universe_context : UState.t -> Pp.t
val pr_evd_level : evar_map -> Univ.Level.t -> Pp.t
-(** Internal hook to register user-level printer *)
+module Internal : sig
-val set_print_constr : (env -> Evd.evar_map -> constr -> Pp.t) -> unit
+(** NOTE: to print terms you always want to use functions in
+ Printer, not these ones which are for very special cases. *)
-(** User-level printers *)
+(** debug printers: print raw form for terms, both with
+ evar-substitution and without. *)
+val debug_print_constr : constr -> Pp.t
+val debug_print_constr_env : env -> evar_map -> constr -> Pp.t
-val print_constr : constr -> Pp.t
+(** Pretty-printer hook: [print_constr_env env sigma c] will pretty
+ print c if the pretty printing layer has been linked into the Coq
+ binary. *)
val print_constr_env : env -> Evd.evar_map -> constr -> Pp.t
-(** debug printer: do not use to display terms to the casual user... *)
+(** [set_print_constr f] sets f to be the pretty printer *)
+val set_print_constr : (env -> Evd.evar_map -> constr -> Pp.t) -> unit
+(** Printers for contexts *)
val print_named_context : env -> Pp.t
val pr_rel_decl : env -> Constr.rel_declaration -> Pp.t
val print_rel_context : env -> Pp.t
val print_env : env -> Pp.t
+
+val print_constr : constr -> Pp.t
+[@@deprecated "use print_constr_env"]
+
+end
+
+val print_constr : constr -> Pp.t
+[@@deprecated "use Internal.print_constr_env"]
+
+val print_constr_env : env -> Evd.evar_map -> constr -> Pp.t
+[@@deprecated "use Internal.print_constr_env"]
+
+val print_rel_context : env -> Pp.t
+[@@deprecated "use Internal.print_rel_context"]
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index ce620d5312..f26ec0f401 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -26,6 +26,10 @@ let init_size=5
let cc_verbose=ref false
+let print_constr t =
+ let sigma, env = Pfedit.get_current_context () in
+ Printer.pr_econstr_env env sigma t
+
let debug x =
if !cc_verbose then Feedback.msg_debug (x ())
@@ -483,10 +487,10 @@ let rec inst_pattern subst = function
args t
let pr_idx_term uf i = str "[" ++ int i ++ str ":=" ++
- Termops.print_constr (EConstr.of_constr (constr_of_term (term uf i))) ++ str "]"
+ print_constr (EConstr.of_constr (constr_of_term (term uf i))) ++ str "]"
let pr_term t = str "[" ++
- Termops.print_constr (EConstr.of_constr (constr_of_term t)) ++ str "]"
+ print_constr (EConstr.of_constr (constr_of_term t)) ++ str "]"
let rec add_term state t=
let uf=state.uf in
@@ -601,7 +605,7 @@ let add_inst state (inst,int_subst) =
begin
debug (fun () ->
(str "Adding new equality, depth="++ int state.rew_depth) ++ fnl () ++
- (str " [" ++ Termops.print_constr (EConstr.of_constr prf) ++ str " : " ++
+ (str " [" ++ print_constr (EConstr.of_constr prf) ++ str " : " ++
pr_term s ++ str " == " ++ pr_term t ++ str "]"));
add_equality state prf s t
end
@@ -609,7 +613,7 @@ let add_inst state (inst,int_subst) =
begin
debug (fun () ->
(str "Adding new disequality, depth="++ int state.rew_depth) ++ fnl () ++
- (str " [" ++ Termops.print_constr (EConstr.of_constr prf) ++ str " : " ++
+ (str " [" ++ print_constr (EConstr.of_constr prf) ++ str " : " ++
pr_term s ++ str " <> " ++ pr_term t ++ str "]"));
add_disequality state (Hyp prf) s t
end
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index 48d677a864..6bab8d0353 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -12,7 +12,6 @@ open Util
open Names
open Pp
open Tacexpr
-open Termops
let (ltac_trace_info : ltac_trace Exninfo.t) = Exninfo.make ()
@@ -51,8 +50,8 @@ let msg_tac_notice s = Proofview.NonLogical.print_notice (s++fnl())
let db_pr_goal gl =
let env = Proofview.Goal.env gl in
let concl = Proofview.Goal.concl gl in
- let penv = print_named_context env in
- let pc = print_constr_env env (Tacmach.New.project gl) concl in
+ let penv = Termops.Internal.print_named_context env in
+ let pc = Printer.pr_econstr_env env (Tacmach.New.project gl) concl in
str" " ++ hv 0 (penv ++ fnl () ++
str "============================" ++ fnl () ++
str" " ++ pc) ++ fnl ()
@@ -243,7 +242,7 @@ let db_constr debug env sigma c =
let open Proofview.NonLogical in
is_debug debug >>= fun db ->
if db then
- msg_tac_debug (str "Evaluated term: " ++ print_constr_env env sigma c)
+ msg_tac_debug (str "Evaluated term: " ++ Printer.pr_econstr_env env sigma c)
else return ()
(* Prints the pattern rule *)
@@ -268,7 +267,7 @@ let db_matched_hyp debug env sigma (id,_,c) ido =
is_debug debug >>= fun db ->
if db then
msg_tac_debug (str "Hypothesis " ++ Id.print id ++ hyp_bound ido ++
- str " has been matched: " ++ print_constr_env env sigma c)
+ str " has been matched: " ++ Printer.pr_econstr_env env sigma c)
else return ()
(* Prints the matched conclusion *)
@@ -276,7 +275,7 @@ let db_matched_concl debug env sigma c =
let open Proofview.NonLogical in
is_debug debug >>= fun db ->
if db then
- msg_tac_debug (str "Conclusion has been matched: " ++ print_constr_env env sigma c)
+ msg_tac_debug (str "Conclusion has been matched: " ++ Printer.pr_econstr_env env sigma c)
else return ()
(* Prints a success message when the goal has been matched *)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 6c52dacaa9..7d480b8d48 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -588,7 +588,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
(* Evar must be undefined since we have flushed evars *)
let () = if !debug_unification then
let open Pp in
- Feedback.msg_notice (v 0 (pr_state appr1 ++ cut () ++ pr_state appr2 ++ cut ())) in
+ Feedback.msg_notice (v 0 (pr_state env evd appr1 ++ cut () ++ pr_state env evd appr2 ++ cut ())) in
match (flex_kind_of_term (fst ts) env evd term1 sk1,
flex_kind_of_term (fst ts) env evd term2 sk2) with
| Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) ->
@@ -1225,8 +1225,9 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
let (term2,l2 as appr2) = try destApp evd t2 with DestKO -> (t2, [||]) in
let () = if !debug_unification then
let open Pp in
- Feedback.msg_notice (v 0 (str "Heuristic:" ++ spc () ++ print_constr t1
- ++ cut () ++ print_constr t2 ++ cut ())) in
+ Feedback.msg_notice (v 0 (str "Heuristic:" ++ spc () ++
+ Termops.Internal.print_constr_env env evd t1 ++ cut () ++
+ Termops.Internal.print_constr_env env evd t2 ++ cut ())) in
let app_empty = Array.is_empty l1 && Array.is_empty l2 in
match EConstr.kind evd term1, EConstr.kind evd term2 with
| Evar (evk1,args1), (Rel _|Var _) when app_empty
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index b452755b10..571be7466c 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -201,4 +201,4 @@ let lift_tycon n = Option.map (lift n)
let pr_tycon env sigma = function
None -> str "None"
- | Some t -> Termops.print_constr_env env sigma t
+ | Some t -> Termops.Internal.print_constr_env env sigma t
diff --git a/pretyping/globEnv.ml b/pretyping/globEnv.ml
index 25510826cc..63a66b471b 100644
--- a/pretyping/globEnv.ml
+++ b/pretyping/globEnv.ml
@@ -140,7 +140,7 @@ let protected_get_type_of env sigma c =
try Retyping.get_type_of ~lax:true env sigma c
with Retyping.RetypeError _ ->
user_err
- (str "Cannot reinterpret " ++ quote (print_constr c) ++
+ (str "Cannot reinterpret " ++ quote (Termops.Internal.print_constr_env env sigma c) ++
str " in the current environment.")
let invert_ltac_bound_name env id0 id =
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index b040e63cd2..0fa573b9a6 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -358,7 +358,7 @@ let make_case_or_project env sigma indf ci pred c branches =
not (has_dependent_elim mib) then
user_err ~hdr:"make_case_or_project"
Pp.(str"Dependent case analysis not allowed" ++
- str" on inductive type " ++ print_constr_env env sigma (mkInd ind))
+ str" on inductive type " ++ Termops.Internal.print_constr_env env sigma (mkInd ind))
in
let branch = branches.(0) in
let ctx, br = decompose_lam_n_assum sigma (Array.length ps) branch in
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index a4c2cb2352..b9345190fb 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -976,9 +976,9 @@ and pretype_instance k0 resolve_tc env evdref loc hyps evk update =
pr_existential_key !evdref evk ++
strbrk " in current context: binding for " ++ Id.print id ++
strbrk " is not convertible to its expected definition (cannot unify " ++
- quote (print_constr_env !!env !evdref b) ++
+ quote (Termops.Internal.print_constr_env !!env !evdref b) ++
strbrk " and " ++
- quote (print_constr_env !!env !evdref c) ++
+ quote (Termops.Internal.print_constr_env !!env !evdref c) ++
str ").")
| Some b, None ->
user_err ?loc (str "Cannot interpret " ++
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 77ad96d2cf..c25416405e 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -229,7 +229,7 @@ let warn_projection_no_head_constant =
let env = Termops.push_rels_assum sign env in
let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con) in
let proji_sp_pp = Nametab.pr_global_env Id.Set.empty (ConstRef proji_sp) in
- let term_pp = Termops.print_constr_env env (Evd.from_env env) (EConstr.of_constr t) in
+ let term_pp = Termops.Internal.print_constr_env env (Evd.from_env env) (EConstr.of_constr t) in
strbrk "Projection value has no head constant: "
++ term_pp ++ strbrk " in canonical instance "
++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.")
@@ -295,8 +295,12 @@ let add_canonical_structure warn o =
in match ocs with
| None -> object_table := GlobRef.Map.add proj ((pat,s)::l) !object_table;
| Some (c, cs) ->
- let old_can_s = (Termops.print_constr (EConstr.of_constr cs.o_DEF))
- and new_can_s = (Termops.print_constr (EConstr.of_constr s.o_DEF)) in
+ (* XXX: Undesired global access to env *)
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ let old_can_s = (Termops.Internal.print_constr_env env sigma (EConstr.of_constr cs.o_DEF))
+ and new_can_s = (Termops.Internal.print_constr_env env sigma (EConstr.of_constr s.o_DEF))
+ in
let prj = (Nametab.pr_global_env Id.Set.empty proj)
and hd_val = (pr_cs_pattern cs_pat) in
if warn then warn_redundant_canonical_projection (hd_val,prj,new_can_s,old_can_s))
@@ -362,7 +366,7 @@ let check_and_decompose_canonical_structure ref =
try lookup_structure indsp
with Not_found ->
error_not_structure ref
- (str "Could not find the record or structure " ++ Termops.print_constr (EConstr.mkInd indsp)) in
+ (str "Could not find the record or structure " ++ Termops.Internal.print_constr_env env evd (EConstr.mkInd indsp)) in
let ntrue_projs = List.count snd s.s_PROJKIND in
if s.s_EXPECTEDPARAM + ntrue_projs > Array.length args then
error_not_structure ref (str "Got too few arguments to the record or structure constructor.");
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index a0d20b7ce4..e8c3b3e2b3 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -254,9 +254,9 @@ module Cst_stack = struct
(applist (cst, List.rev params))
t) cst_l c
- let pr l =
+ let pr env sigma l =
let open Pp in
- let p_c c = Termops.print_constr c in
+ let p_c c = Termops.Internal.print_constr_env env sigma c in
prlist_with_sep pr_semicolon
(fun (c,params,args) ->
hov 1 (str"(" ++ p_c c ++ str ")" ++ spc () ++ pr_sequence p_c params ++ spc () ++ str "(args:" ++
@@ -615,9 +615,9 @@ type contextual_state_reduction_function =
type state_reduction_function = contextual_state_reduction_function
type local_state_reduction_function = evar_map -> state -> state
-let pr_state (tm,sk) =
+let pr_state env sigma (tm,sk) =
let open Pp in
- let pr c = Termops.print_constr c in
+ let pr c = Termops.Internal.print_constr_env env sigma c in
h 0 (pr tm ++ str "|" ++ cut () ++ Stack.pr pr sk)
(*************************************)
@@ -855,10 +855,10 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
let rec whrec cst_l (x, stack) =
let () = if !debug_RAKAM then
let open Pp in
- let pr c = Termops.print_constr c in
+ let pr c = Termops.Internal.print_constr_env env sigma c in
Feedback.msg_notice
(h 0 (str "<<" ++ pr x ++
- str "|" ++ cut () ++ Cst_stack.pr cst_l ++
+ str "|" ++ cut () ++ Cst_stack.pr env sigma cst_l ++
str "|" ++ cut () ++ Stack.pr pr stack ++
str ">>"))
in
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index dd3cd26f0f..c0ff6723f6 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -60,7 +60,7 @@ module Cst_stack : sig
val best_cst : t -> (constr * constr list) option
val best_replace : Evd.evar_map -> constr -> t -> constr -> constr
val reference : Evd.evar_map -> t -> Constant.t option
- val pr : t -> Pp.t
+ val pr : env -> Evd.evar_map -> t -> Pp.t
end
module Stack : sig
@@ -140,7 +140,7 @@ type contextual_state_reduction_function =
type state_reduction_function = contextual_state_reduction_function
type local_state_reduction_function = evar_map -> state -> state
-val pr_state : state -> Pp.t
+val pr_state : env -> evar_map -> state -> Pp.t
(** {6 Reduction Function Operators } *)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index fc1f6fc81e..e223674579 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -684,8 +684,10 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
and cN = Evarutil.whd_head_evar sigma curn in
let () =
if !debug_unification then
- Feedback.msg_debug (print_constr_env curenv sigma cM ++ str" ~= " ++ print_constr_env curenv sigma cN)
- in
+ Feedback.msg_debug (
+ Termops.Internal.print_constr_env curenv sigma cM ++ str" ~= " ++
+ Termops.Internal.print_constr_env curenv sigma cN)
+ in
match (EConstr.kind sigma cM, EConstr.kind sigma cN) with
| Meta k1, Meta k2 ->
if Int.equal k1 k2 then substn else
diff --git a/printing/printer.ml b/printing/printer.ml
index 3a2450c426..6cd4daa374 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -192,7 +192,7 @@ let pr_constr_pattern t =
let pr_sort sigma s = pr_glob_sort (extern_sort sigma s)
-let _ = Termops.set_print_constr
+let _ = Termops.Internal.set_print_constr
(fun env sigma t -> pr_lconstr_expr (extern_constr ~lax:true false env sigma t))
let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)"
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 79b7e1599b..95e908c4dd 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -575,8 +575,8 @@ let make_clenv_binding env sigma = make_clenv_binding_gen false None env sigma
let pr_clenv clenv =
h 0
- (str"TEMPL: " ++ print_constr clenv.templval.rebus ++
- str" : " ++ print_constr clenv.templtyp.rebus ++ fnl () ++
+ (str"TEMPL: " ++ Termops.Internal.print_constr_env clenv.env clenv.evd clenv.templval.rebus ++
+ str" : " ++ Termops.Internal.print_constr_env clenv.env clenv.evd clenv.templtyp.rebus ++ fnl () ++
pr_evar_map (Some 2) clenv.evd)
(****************************************************************)
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 092bb5c276..182b38d350 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -127,8 +127,8 @@ open Pp
let db_pr_goal sigma g =
let env = Goal.V82.env sigma g in
- let penv = print_named_context env in
- let pc = print_constr_env env sigma (Goal.V82.concl sigma g) in
+ let penv = Termops.Internal.print_named_context env in
+ let pc = Termops.Internal.print_constr_env env sigma (Goal.V82.concl sigma g) in
str" " ++ hv 0 (penv ++ fnl () ++
str "============================" ++ fnl () ++
str" " ++ pc) ++ fnl ()
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 3456d13bbe..f3581f17dd 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -693,8 +693,9 @@ module Search = struct
let msg =
match fst ie with
| Pretype_errors.PretypeError (env, evd, Pretype_errors.CannotUnify (x,y,_)) ->
- str"Cannot unify " ++ print_constr_env env evd x ++ str" and " ++
- print_constr_env env evd y
+ str"Cannot unify " ++
+ Printer.pr_econstr_env env evd x ++ str" and " ++
+ Printer.pr_econstr_env env evd y
| ReachedLimitEx -> str "Proof-search reached its limit."
| NoApplicableEx -> str "Proof-search failed."
| e -> CErrors.iprint ie
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 878e2b1f01..596feeec8b 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -655,7 +655,7 @@ module New = struct
| _ ->
let name_elim =
match EConstr.kind sigma elim with
- | Const _ | Var _ -> str " " ++ print_constr_env (pf_env gl) sigma elim
+ | Const _ | Var _ -> str " " ++ Printer.pr_econstr_env (pf_env gl) sigma elim
| _ -> mt ()
in
user_err ~hdr:"Tacticals.general_elim_then_using"
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:39:37 +0000