From df0f615f240dabddfc1d605b697edd0b533eb3e0 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Mon, 13 Dec 1999 09:15:15 +0000
Subject: petite erreur dans Command

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@246 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/command.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'toplevel/command.ml')

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 6fb0018ddb..f0e40d7bf8 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -79,7 +79,7 @@ let abstraction_definition ident arity com =
 let parameter_def_var ident c =
   let c = constr_of_com1 true Evd.empty (Global.env()) c in
   declare_parameter (id_of_string ident) c;
-  if is_verbose() then message ((string_of_id ident) ^ " is assumed")
+  if is_verbose() then message (ident ^ " is assumed")
     
 let hypothesis_def_var is_refining ident n c =
   let warning () = 
@@ -95,7 +95,7 @@ let hypothesis_def_var is_refining ident n c =
         if Lib.is_section_p disch_sp then begin
           declare_variable (id_of_string ident)
              (constr_of_com1 true Evd.empty (Global.env()) c,n,false);
-	  if is_verbose() then message ((string_of_id ident) ^ " is assumed");
+	  if is_verbose() then message (ident ^ " is assumed");
           if is_refining then 
             mSGERRNL [< 'sTR"Warning: Variable "; 'sTR ident; 
                         'sTR" is not visible from current goals" >]
-- 
cgit v1.2.3