aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/reductionops.ml4
1 files changed, 3 insertions, 1 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 308896f3a..32c993224 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