From 34c7ef490d26e67ad1545dba65db7080744ffbe0 Mon Sep 17 00:00:00 2001
From: Matěj Grabovský
Date: Wed, 11 Feb 2015 10:04:20 +0100
Subject: Missing space in error message

---
 tactics/tactics.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 9265328a47..a298bba978 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -425,7 +425,7 @@ let pf_reduce_decl redfun where (id,c,ty) gl =
   match c with
   | None ->
       if where == InHypValueOnly then
-	errorlabstrm "" (pr_id id ++ str "has no value.");
+	errorlabstrm "" (pr_id id ++ str " has no value.");
       (id,None,redfun' ty)
   | Some b ->
       let b' = if where != InHypTypeOnly then redfun' b else b in
@@ -522,7 +522,7 @@ let pf_e_reduce_decl redfun where (id,c,ty) gl =
   match c with
   | None ->
       if where == InHypValueOnly then
-	errorlabstrm "" (pr_id id ++ str "has no value.");
+	errorlabstrm "" (pr_id id ++ str " has no value.");
     let sigma, ty' = redfun sigma ty in
       sigma, (id,None,ty')
   | Some b ->
@@ -565,7 +565,7 @@ let e_pf_change_decl (redfun : bool -> e_reduction_function) where (id,c,ty) env
   match c with
   | None ->
       if where == InHypValueOnly then
-	errorlabstrm "" (pr_id id ++ str "has no value.");
+	errorlabstrm "" (pr_id id ++ str " has no value.");
     let sigma',ty' = redfun false env sigma ty in
       sigma', (id,None,ty')
   | Some b ->
-- 
cgit v1.2.3