aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--pretyping/reductionops.ml4
1 files changed, 3 insertions, 1 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 2aa2f9013..eae0e249e 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1314,7 +1314,9 @@ let pb_equal = function
| Reduction.CONV -> Reduction.CONV
let report_anomaly e =
- let e = UserError (None, Pp.(str "Conversion test raised an anomaly" ++ print e)) in
+ let msg = Pp.(str "Conversion test raised an anomaly:" ++
+ spc () ++ CErrors.print e) in
+ let e = UserError (None,msg) in
let e = CErrors.push e in
iraise e