From a20a5bd63b4fa9ccfd386db7f4fd066537fc4ab2 Mon Sep 17 00:00:00 2001
From: bertot
Date: Tue, 24 Apr 2001 06:13:57 +0000
Subject: Removing a debug message for the search command.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1678 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/interface/centaur.ml | 2 --
 1 file changed, 2 deletions(-)

diff --git a/contrib/interface/centaur.ml b/contrib/interface/centaur.ml
index 79fd23b075..f48f04e7c3 100644
--- a/contrib/interface/centaur.ml
+++ b/contrib/interface/centaur.ml
@@ -242,10 +242,8 @@ let filter_by_module_from_varg_list (l:vernac_arg list) =
     Search.filter_by_module_from_list (dir_list, b);;
 
 let add_search (global_reference:global_reference) assumptions cstr =
-  mSGNL [< 'sTR "DEBUG: entering add_search" >];
   try 
   let id_string = string_of_qualid (Global.qualid_of_global global_reference) in
-  let _ = mSGNL [< 'sTR "DEBUG: " ; 'sTR id_string >] in
   let ast = 
     try
       CT_premise (CT_ident id_string, translate_constr assumptions cstr)
-- 
cgit v1.2.3