aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac/rewrite.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac/rewrite.ml')
-rw-r--r--plugins/ltac/rewrite.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index bbd7834d5..75b665aad 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1461,7 +1461,7 @@ let solve_constraints env (evars,cstrs) =
let nf_zeta =
Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
-exception RewriteFailure of Pp.std_ppcmds
+exception RewriteFailure of Pp.t
type result = (evar_map * constr option * types) option option