aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/refine.mli
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/refine.mli')
-rw-r--r--proofs/refine.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/refine.mli b/proofs/refine.mli
index 20f5a0791..3b0a9e5b6 100644
--- a/proofs/refine.mli
+++ b/proofs/refine.mli
@@ -17,7 +17,7 @@ open Proofview
(** Printer used to print the constr which refine refines. *)
val pr_constr :
- (Environ.env -> Evd.evar_map -> Term.constr -> Pp.std_ppcmds) Hook.t
+ (Environ.env -> Evd.evar_map -> Term.constr -> Pp.t) Hook.t
(** {7 Refinement primitives} *)