4 files changed, 9 insertions, 9 deletions
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 198e057ebc..05474d5f84 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -44,9 +44,6 @@ let typecheck_evar ev env sigma =
   let sigma, _ = Typing.sort_of env sigma (Evd.evar_concl info) in
   sigma
 
-let (pr_constrv,pr_constr) =
-  Hook.make ~default:(fun _env _sigma _c -> Pp.str"<constr>") ()
-
 (* Get the side-effect's constant declarations to update the monad's
   * environmnent *)
 let add_if_undefined env eff =
@@ -111,7 +108,7 @@ let generic_refine ~typecheck f gl =
   let sigma = CList.fold_left Proofview.Unsafe.mark_as_goal sigma comb in
   let comb = CList.map (fun x -> Proofview.goal_with_state x state) comb in
   let trace () = Pp.(hov 2 (str"simple refine"++spc()++
-                            Hook.get pr_constrv env sigma (EConstr.Unsafe.to_constr c))) in
+                            Termops.Internal.print_constr_env env sigma c)) in
   Proofview.Trace.name_tactic trace (Proofview.tclUNIT v) >>= fun v ->
   Proofview.Unsafe.tclSETENV (Environ.reset_context env) <*>
   Proofview.Unsafe.tclEVARS sigma <*>
diff --git a/proofs/refine.mli b/proofs/refine.mli
index 70a23a9fba..1af6463a02 100644
--- a/proofs/refine.mli
+++ b/proofs/refine.mli
@@ -17,10 +17,6 @@ open Proofview
 
 (** {6 The refine tactic} *)
 
-(** Printer used to print the constr which refine refines. *)
-val pr_constr :
-  (Environ.env -> Evd.evar_map -> Constr.constr -> Pp.t) Hook.t
-
 (** {7 Refinement primitives} *)
 
 val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit tactic
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 182b38d350..9e42a71ea8 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -227,4 +227,9 @@ module New = struct
 
   let pf_nf_evar gl t = nf_evar (project gl) t
 
+  let pf_undefined_evars gl =
+    let sigma = Proofview.Goal.sigma gl in
+    let ev = Proofview.Goal.goal gl in
+    let evi = Evd.find sigma ev in
+      Evarutil.filtered_undefined_evars_of_evar_info sigma evi
 end
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 31496fb3d5..b4cb2be2b8 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -95,7 +95,7 @@ val refine           : constr -> tactic
 val pr_gls    : goal sigma -> Pp.t
 val pr_glls   : goal list sigma -> Pp.t
 
-(* Variants of [Tacmach] functions built with the new proof engine *)
+(** Variants of [Tacmach] functions built with the new proof engine *)
 module New : sig
   val pf_apply : (env -> evar_map -> 'a) -> Proofview.Goal.t -> 'a
   val pf_global : Id.t -> Proofview.Goal.t -> GlobRef.t
@@ -139,4 +139,6 @@ module New : sig
 
   val pf_nf_evar : Proofview.Goal.t -> constr -> constr
 
+  (** Gathers the undefined evars of the given goal. *)
+  val pf_undefined_evars : Proofview.Goal.t -> Evar.Set.t
 end