From 376a6b66bf4c4181214bb86a07c4677f17112b4c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 7 Oct 2014 14:09:55 +0200
Subject: Removing debugging information committed by mistake.

---
 tactics/tactics.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index cc95430f5a..c40dc40786 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -476,9 +476,9 @@ let weak_check env sigma deep newc origc =
 let change_and_check cv_pb deep t env sigma c =
   let sigma, t' = t env sigma in
   let b = weak_check env sigma deep t' c in
-  if not b then errorlabstrm "convert-check-hyp" (str "Not convertible1.");
+  if not b then errorlabstrm "convert-check-hyp" (str "Not convertible.");
   let sigma, b = infer_conv ~pb:cv_pb env sigma t' c in
-  if not b then errorlabstrm "convert-check-hyp" (str "Not convertible2.");
+  if not b then errorlabstrm "convert-check-hyp" (str "Not convertible.");
   sigma, t'
 
 let change_and_check_subst cv_pb subst t env sigma c =
-- 
cgit v1.2.3