From 283579ff70d324296e2b7ee2535b1187ca32e0cb Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Fri, 19 Aug 2016 07:38:25 +0200
Subject: Remove extraneous dot in error message (bug #4832).

---
 tactics/equality.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 819a995db..06a9b317a 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -610,7 +610,7 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
   in
   match evd with
   | None ->
-    tclFAIL 0 (str"Terms do not have convertible types.")
+    tclFAIL 0 (str"Terms do not have convertible types")
   | Some evd ->
     let e = build_coq_eq () in
     let sym = build_coq_eq_sym () in
-- 
cgit v1.2.3