petite erreur dans Command

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@246 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 6 insertions, 8 deletions

diff --git a/.depend b/.depend
index 17b668afe4..846fc89b7e 100644
--- a/.depend
+++ b/.depend
@@ -70,10 +70,6 @@ parsing/printer.cmi: parsing/coqast.cmi kernel/names.cmi lib/pp.cmi \
     pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi 
 parsing/termast.cmi: parsing/coqast.cmi kernel/names.cmi \
     pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi 
-pretyping/cases.debug.cmi: kernel/environ.cmi pretyping/evarutil.cmi \
-    kernel/evd.cmi kernel/generic.cmi kernel/names.cmi lib/pp.cmi \
-    pretyping/rawterm.cmi pretyping/retyping.cmi kernel/sign.cmi \
-    kernel/term.cmi kernel/type_errors.cmi 
 pretyping/cases.cmi: kernel/environ.cmi pretyping/evarutil.cmi kernel/evd.cmi \
     kernel/names.cmi pretyping/rawterm.cmi kernel/term.cmi 
 pretyping/classops.cmi: library/declare.cmi kernel/environ.cmi kernel/evd.cmi \
@@ -825,6 +821,8 @@ tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo
 tools/coqdep.cmx: config/coq_config.cmx tools/coqdep_lexer.cmx 
 tools/coqdep_lexer.cmo: config/coq_config.cmi 
 tools/coqdep_lexer.cmx: config/coq_config.cmx 
+tools/gallina.cmo: tools/gallina_lexer.cmo 
+tools/gallina.cmx: tools/gallina_lexer.cmx 
 toplevel/class.cmo: pretyping/classops.cmi kernel/constant.cmi \
     library/declare.cmi kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \
     library/global.cmi kernel/inductive.cmi kernel/instantiate.cmi \
@@ -861,12 +859,12 @@ toplevel/coqtop.cmo: config/coq_config.cmi toplevel/coqinit.cmi \
     toplevel/errors.cmi library/lib.cmi library/library.cmi \
     toplevel/mltop.cmi lib/options.cmi lib/pp.cmi parsing/printer.cmi \
     lib/profile.cmi library/states.cmi lib/system.cmi toplevel/toplevel.cmi \
-    toplevel/usage.cmi lib/util.cmi toplevel/vernac.cmi 
+    toplevel/usage.cmi lib/util.cmi toplevel/vernac.cmi toplevel/coqtop.cmi 
 toplevel/coqtop.cmx: config/coq_config.cmx toplevel/coqinit.cmx \
     toplevel/errors.cmx library/lib.cmx library/library.cmx \
     toplevel/mltop.cmi lib/options.cmx lib/pp.cmx parsing/printer.cmx \
     lib/profile.cmx library/states.cmx lib/system.cmx toplevel/toplevel.cmx \
-    toplevel/usage.cmx lib/util.cmx toplevel/vernac.cmx 
+    toplevel/usage.cmx lib/util.cmx toplevel/vernac.cmx toplevel/coqtop.cmi 
 toplevel/discharge.cmo: toplevel/class.cmi pretyping/classops.cmi \
     kernel/constant.cmi library/declare.cmi kernel/environ.cmi kernel/evd.cmi \
     kernel/generic.cmi library/global.cmi kernel/inductive.cmi \
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" >]