From 35219fd89ce9a1b7ce92316ee84e3c8ad40b3831 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 8 Nov 2017 12:28:39 +0100
Subject: Fixing an (apparently misplaced) spc in anomaly reporting message.

---
 lib/cErrors.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lib/cErrors.ml b/lib/cErrors.ml
index 3f4e8aa12f..6d3fdf927e 100644
--- a/lib/cErrors.ml
+++ b/lib/cErrors.ml
@@ -91,7 +91,7 @@ let print_backtrace e = match Backtrace.get_backtrace e with
 
 let print_anomaly askreport e =
   if askreport then
-    hov 0 (str "Anomaly" ++ spc () ++ quote (raw_anomaly e) ++ spc ()) ++
+    hov 0 (str "Anomaly" ++ spc () ++ quote (raw_anomaly e)) ++ spc () ++
     hov 0 (str "Please report at " ++ str Coq_config.wwwbugtracker ++ str ".")
   else
     hov 0 (raw_anomaly e)
-- 
cgit v1.2.3


From 464ef8adf143b4c08252aa5148583aa52f65464c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
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(-)

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 2aa2f90131..eae0e249ef 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