diff options
| author | bertot | 2001-04-24 06:13:57 +0000 |
|---|---|---|
| committer | bertot | 2001-04-24 06:13:57 +0000 |
| commit | a20a5bd63b4fa9ccfd386db7f4fd066537fc4ab2 (patch) | |
| tree | 8fe2c9f45212cbe4eb7c5be099f07692d6ec8005 /contrib/interface | |
| parent | 26e60d7f4d98e6ec6bfb54005409c9555962101b (diff) | |
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
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/centaur.ml | 2 |
1 files changed, 0 insertions, 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) |