4 files changed, 17 insertions, 15 deletions
diff --git a/engine/evd.ml b/engine/evd.ml
index d8a658e3e3..9c05c6c028 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1265,7 +1265,7 @@ let protect f x =
 
 let (f_print_constr, print_constr_hook) = Hook.make ()
 
-let print_constr a = protect (fun c -> Hook.get f_print_constr (Global.env ()) c) a
+let print_constr a = protect (fun c -> Hook.get f_print_constr (Global.env ()) empty c) a
 
 let pr_meta_map mmap =
   let pr_name = function
@@ -1423,11 +1423,11 @@ let pr_evar_constraints pbs =
       Namegen.make_all_name_different env
     in
     print_env_short env ++ spc () ++ str "|-" ++ spc () ++
-      Hook.get f_print_constr env t1 ++ spc () ++
+      Hook.get f_print_constr env empty t1 ++ spc () ++
       str (match pbty with
             | Reduction.CONV -> "=="
             | Reduction.CUMUL -> "<=") ++
-      spc () ++ Hook.get f_print_constr env t2
+      spc () ++ Hook.get f_print_constr env empty t2
   in
   prlist_with_sep fnl pr_evconstr pbs
 
diff --git a/engine/evd.mli b/engine/evd.mli
index 5c9effd4be..4e8284675e 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -607,7 +607,7 @@ val pr_evar_suggested_name : existential_key -> evar_map -> Id.t
 
 (** {5 Debug pretty-printers} *)
 
-val print_constr_hook : (Environ.env -> constr -> Pp.std_ppcmds) Hook.t
+val print_constr_hook : (Environ.env -> evar_map -> constr -> Pp.std_ppcmds) Hook.t
 val pr_evar_info : evar_info -> Pp.std_ppcmds
 val pr_evar_constraints : evar_constraint list -> Pp.std_ppcmds
 val pr_evar_map : ?with_univs:bool -> int option -> evar_map -> Pp.std_ppcmds
diff --git a/engine/termops.ml b/engine/termops.ml
index 465832c10d..46e9ad927f 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -97,11 +97,11 @@ let rec pr_constr c = match kind_of_term c with
            cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++
          str"}")
 
-let term_printer = ref (fun _ -> pr_constr)
-let print_constr_env t = !term_printer t
-let print_constr t = !term_printer (Global.env()) t
+let term_printer = ref (fun _env _sigma c -> pr_constr (EConstr.Unsafe.to_constr c))
+let print_constr_env env sigma t = !term_printer env sigma t
+let print_constr t = !term_printer (Global.env()) Evd.empty t
 let set_print_constr f = term_printer := f
-let () = Hook.set Evd.print_constr_hook (fun env c -> !term_printer env c)
+let () = Hook.set Evd.print_constr_hook (fun env sigma c -> !term_printer env sigma (EConstr.of_constr c))
 
 let pr_var_decl env decl =
   let open NamedDecl in
@@ -109,9 +109,10 @@ let pr_var_decl env decl =
     | LocalAssum _ ->  mt ()
     | LocalDef (_,c,_) ->
 	(* Force evaluation *)
-	let pb = print_constr_env env c in
+	let c = EConstr.of_constr c in
+	let pb = print_constr_env env Evd.empty c in
 	  (str" := " ++ pb ++ cut () ) in
-  let pt = print_constr_env env (get_type decl) in
+  let pt = print_constr_env env Evd.empty (EConstr.of_constr (get_type decl)) in
   let ptyp = (str" : " ++ pt) in
     (pr_id (get_id decl) ++ hov 0 (pbody ++ ptyp))
 
@@ -121,9 +122,10 @@ let pr_rel_decl env decl =
     | LocalAssum _ -> mt ()
     | LocalDef (_,c,_) ->
 	(* Force evaluation *)
-	let pb = print_constr_env env c in
+	let c = EConstr.of_constr c in
+	let pb = print_constr_env env Evd.empty c in
 	  (str":=" ++ spc () ++ pb ++ spc ()) in
-  let ptyp = print_constr_env env (get_type decl) in
+  let ptyp = print_constr_env env Evd.empty (EConstr.of_constr (get_type decl)) in
     match get_name decl with
       | Anonymous -> hov 0 (str"<>" ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
       | Name id -> hov 0 (pr_id id ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
diff --git a/engine/termops.mli b/engine/termops.mli
index d7d9c743da..3f924cfa14 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -21,9 +21,9 @@ val pr_sort_family : sorts_family -> std_ppcmds
 val pr_fix : ('a -> std_ppcmds) -> ('a, 'a) pfixpoint -> std_ppcmds
 
 (** debug printer: do not use to display terms to the casual user... *)
-val set_print_constr : (env -> Constr.constr -> std_ppcmds) -> unit
-val print_constr     : Constr.constr -> std_ppcmds
-val print_constr_env : env -> Constr.constr -> std_ppcmds
+val set_print_constr : (env -> Evd.evar_map -> constr -> std_ppcmds) -> unit
+val print_constr     : constr -> std_ppcmds
+val print_constr_env : env -> Evd.evar_map -> constr -> std_ppcmds
 val print_named_context : env -> std_ppcmds
 val pr_rel_decl : env -> Context.Rel.Declaration.t -> std_ppcmds
 val print_rel_context : env -> std_ppcmds