Distinction local/global

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

3 files changed, 27 insertions, 24 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index aa9545210..eef22b8a2 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -49,12 +49,16 @@ let red_constant_entry ce = function
 	const_entry_type = 
 	  ce.const_entry_type }
 
-let definition_body_red ident n com comtypeopt red_option = 
+let definition_body_red red_option ident (local,n) com comtypeopt = 
+  let warning () = 
+    mSGERRNL [< 'sTR"Warning: "; pr_id ident; 
+                'sTR" is declared as a global definition" >] in
   let ce = constant_entry_of_com (com,comtypeopt) in
   let ce' = red_constant_entry ce red_option in
   match n with
     | NeverDischarge ->
 	declare_constant ident (ConstantEntry ce',n);
+	if local then warning ();
 	if is_verbose() then message ((string_of_id ident) ^ " is defined")
     | DischargeAt disch_sp ->
         if Lib.is_section_p disch_sp then begin
@@ -67,13 +71,12 @@ let definition_body_red ident n com comtypeopt red_option =
             mSGERRNL [< 'sTR"Warning: Variable "; pr_id ident; 
                         'sTR" is not visible from current goals" >]
         end else begin
-	  mSGERRNL [< 'sTR"Warning: "; pr_id ident; 
-                      'sTR" is declared as a global definition">];
 	  declare_constant ident (ConstantEntry ce',n);
+	  warning ();
 	  if is_verbose() then message ((string_of_id ident) ^ " is defined")
 	end
 
-let definition_body ident n com typ = definition_body_red ident n com typ None
+let definition_body = definition_body_red None
 
 let syntax_definition ident com =
   let c = interp_rawconstr Evd.empty (Global.env()) com in 
@@ -96,8 +99,8 @@ let hypothesis_def_var is_refining ident n c =
   in
   match n with
     | NeverDischarge -> 
-	warning();
-	parameter_def_var ident c
+	parameter_def_var ident c;
+	warning()
     | DischargeAt disch_sp ->
         if Lib.is_section_p disch_sp then begin
 	  let t = interp_type Evd.empty (Global.env()) c in
@@ -108,8 +111,8 @@ let hypothesis_def_var is_refining ident n c =
             mSGERRNL [< 'sTR"Warning: Variable "; 'sTR ident; 
                         'sTR" is not visible from current goals" >]
         end else begin
-	  warning();
-          parameter_def_var ident c
+          parameter_def_var ident c;
+	  warning()
 	end
 
 (* 3| Mutual Inductive definitions *)
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 263d67032..8c34a3eb1 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -10,11 +10,11 @@ open Declare
 (* Declaration functions. The following functions take ASTs, transform them
    into [constr] and then call the corresponding functions of [Declare]. *)
 
-val definition_body : identifier -> strength -> 
+val definition_body : identifier -> bool * strength -> 
   Coqast.t -> Coqast.t option -> unit
 
-val definition_body_red : identifier -> strength ->
-  Coqast.t -> Coqast.t option -> Tacred.red_expr option -> unit
+val definition_body_red : Tacred.red_expr option ->  
+  identifier -> bool * strength -> Coqast.t -> Coqast.t option -> unit
 
 val syntax_definition : identifier -> Coqast.t -> unit
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 0a7aa7862..e94b73f18 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -776,22 +776,22 @@ let _ =
 		 Some t, Some redexp
 	     | _ -> bad_vernac_args "DEFINITION"
 	   in 
-	   let stre,coe,objdef,idcoe = match kind with
-	     | "DEFINITION" -> NeverDischarge,false,false,false
-             | "COERCION" -> NeverDischarge,true,false,false
-             | "LCOERCION" -> make_strength_0(),true,false,false
-             | "LET" -> make_strength_2(),false,false,false
-             | "LOCAL" -> make_strength_0(),false,false,false
-             | "OBJECT" -> NeverDischarge,false,true,false
-             | "LOBJECT" -> make_strength_0(),false,true,false
-             | "OBJCOERCION" -> NeverDischarge,true,true,false
-             | "LOBJCOERCION" -> make_strength_0(),true,true,false
-             | "SUBCLASS" -> NeverDischarge,false,false,true
-             | "LSUBCLASS" -> make_strength_0(),false,false,true
+	   let local,stre,coe,objdef,idcoe = match kind with
+	     | "DEFINITION" -> false,NeverDischarge,false,false,false
+             | "COERCION" -> false,NeverDischarge,true,false,false
+             | "LCOERCION" -> true,make_strength_0(),true,false,false
+             | "LET" -> true,make_strength_2(),false,false,false
+             | "LOCAL" -> true,make_strength_0(),false,false,false
+             | "OBJECT" -> false,NeverDischarge,false,true,false
+             | "LOBJECT" -> true,make_strength_0(),false,true,false
+             | "OBJCOERCION" -> false,NeverDischarge,true,true,false
+             | "LOBJCOERCION" -> true,make_strength_0(),true,true,false
+             | "SUBCLASS" -> false,NeverDischarge,false,false,true
+             | "LSUBCLASS" -> true,make_strength_0(),false,false,true
              | _       -> anomaly "Unexpected string"
 	   in 
 	   fun () ->
-	     definition_body_red id stre c typ_opt red_option;
+	     definition_body_red red_option id (local,stre) c typ_opt;
              if coe then begin
 	       Class.try_add_new_coercion id stre;
                message ((string_of_id id) ^ " is now a coercion")