Branchement des Local sur des SectionLocalDef

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

1 files changed, 21 insertions, 3 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 264cd139e1..aa9545210f 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -52,8 +52,26 @@ let red_constant_entry ce = function
 let definition_body_red ident n com comtypeopt red_option = 
   let ce = constant_entry_of_com (com,comtypeopt) in
   let ce' = red_constant_entry ce red_option in
-  declare_constant ident (ConstantEntry ce',n);
-  if is_verbose() then message ((string_of_id ident) ^ " is defined")
+  match n with
+    | NeverDischarge ->
+	declare_constant ident (ConstantEntry ce',n);
+	if is_verbose() then message ((string_of_id ident) ^ " is defined")
+    | DischargeAt disch_sp ->
+        if Lib.is_section_p disch_sp then begin
+	  let c = match ce.const_entry_type with
+	    | None -> ce.const_entry_body 
+	    | Some t -> mkCast (ce.const_entry_body, t) in
+          declare_variable ident (SectionLocalDef c,n,false);
+	  if is_verbose() then message ((string_of_id ident) ^ " is defined");
+          if Pfedit.refining () then 
+            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);
+	  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
 
@@ -93,7 +111,7 @@ let hypothesis_def_var is_refining ident n c =
 	  warning();
           parameter_def_var ident c
 	end
-	  
+
 (* 3| Mutual Inductive definitions *)
 
 let minductive_message = function