From 60b5e9c05e0c168e30eafede545c221e63d12ea2 Mon Sep 17 00:00:00 2001
From: mlasson
Date: Thu, 25 Jun 2015 19:50:15 +0200
Subject: Also there's an extra space in the error message.

---
 toplevel/himsg.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index ac8ca3a11d..7a3bcfba80 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -1086,7 +1086,7 @@ let error_bad_ind_parameters env c n v1 v2  =
   let pv1 = pr_lconstr_env env Evd.empty v1 in
   let pv2 = pr_lconstr_env env Evd.empty v2 in
   str "Last occurrence of " ++ pv2 ++ str " must have " ++ pv1 ++
-  str " as " ++ pr_nth n ++ str " argument in " ++ brk(1,1) ++ pc ++ str "."
+  str " as " ++ pr_nth n ++ str " argument in" ++ brk(1,1) ++ pc ++ str "."
 
 let error_same_names_types id =
   str "The name" ++ spc () ++ pr_id id ++ spc () ++
-- 
cgit v1.2.3