From e0fd6e50800bc5aec4eafddd315941d6f7bc6efc Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 26 Apr 2016 05:53:40 +0200
Subject: Fixing space in an error message.

---
 ltac/tacinterp.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index b742bb328d..0c9d7ff801 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -151,7 +151,7 @@ module Value = struct
     let pr_v = Pptactic.pr_value Pptactic.ltop v in
     let Val.Dyn (tag, _) = v in
     let tag = Val.pr tag in
-    errorlabstrm "" (str "Type error: value " ++ pr_v ++ str "is a " ++ tag
+    errorlabstrm "" (str "Type error: value " ++ pr_v ++ str " is a " ++ tag
       ++ str " while type " ++ Genarg.pr_argument_type (unquote (rawwit wit)) ++ str " was expected.")
 
   let prj : type a. a Val.tag -> Val.t -> a option = fun t v ->
-- 
cgit v1.2.3