From 464ef8adf143b4c08252aa5148583aa52f65464c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Wed, 8 Nov 2017 12:32:09 +0100
Subject: Fixing missing separator in an error message.

The message is the "Conversion test raised an anomaly" one.
---
 pretyping/reductionops.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'pretyping/reductionops.ml')

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
 
-- 
cgit v1.2.3