Bug des locaux au premier niveau des modules qui disparaissaient de l'environnement (changement de is_section_p)

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

2 files changed, 35 insertions, 31 deletions

diff --git a/library/lib.ml b/library/lib.ml
index df48bc7cbd..d0a015bd95 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -29,14 +29,17 @@ and library_segment = library_entry list
 let lib_stk = ref ([] : (section_path * node) list)
 
 let module_name = ref None
-let path_prefix = ref (["Scratch"] : dir_path)
+let path_prefix = ref ([Nametab.default_root] : dir_path)
+
+let module_sp () =
+  match !module_name with Some m -> m | None -> [Nametab.default_root]
 
 let recalc_path_prefix () =
   let rec recalc = function
     | (sp, OpenedSection _) :: _ ->
 	let (pl,id,_) = repr_path sp in pl@[string_of_id id]
     | _::l -> recalc l
-    | [] -> (match !module_name with Some m -> m | None -> ["Scratch"])
+    | [] -> module_sp ()
   in
   path_prefix := recalc !lib_stk
 
@@ -116,8 +119,10 @@ let check_for_module () =
   with Not_found -> ()
 
 let start_module s =
-  if !module_name <> None then error "a module is already started";
-  if !path_prefix <> ["Scratch"] then error "some sections are already opened";
+  if !module_name <> None then
+    error "a module is already started";
+  if !path_prefix <> [Nametab.default_root] then
+    error "some sections are already opened";
   module_name := Some s;
   Univ.set_module s;
   let _ = add_anonymous_entry (Module s) in
@@ -195,7 +200,10 @@ let reset_name id =
   in
   reset_to sp
 
-let is_section_p sp = dirpath_prefix_of sp !path_prefix
+(* [dir] is a section dir if [module] < [dir] <= [path_prefix] *)
+let is_section_p sp =
+  not (dirpath_prefix_of sp (module_sp ()))
+  & (dirpath_prefix_of sp !path_prefix)
 
 (* State and initialization. *)
 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 41085d3508..30d293ba98 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -54,30 +54,29 @@ let constr_of_constr_entry ce =
     | None -> ce.const_entry_body 
     | Some t -> mkCast (ce.const_entry_body, t)
 
+let declare_global_definition ident ce n local =
+  declare_constant ident (ConstantEntry ce,n,false);
+  if local then
+    wARNING [< pr_id ident; 'sTR" is declared as a global definition" >];
+  if is_verbose() then
+    message ((string_of_id ident) ^ " is defined")
+
 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,false);
-	if local then warning ();
-	if is_verbose() then message ((string_of_id ident) ^ " is defined")
+    | NeverDischarge -> declare_global_definition ident ce n local
     | DischargeAt disch_sp ->
         if Lib.is_section_p disch_sp then begin
 	  let c = constr_of_constr_entry ce 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; 
+            mSGERRNL [< 'sTR"Warning: Local definition "; pr_id ident; 
                         'sTR" is not visible from current goals" >]
-        end else begin
-	  declare_constant ident (ConstantEntry ce',n,false);
-	  warning ();
-	  if is_verbose() then message ((string_of_id ident) ^ " is defined")
-	end
+        end
+	else
+	  declare_global_definition ident ce' n true
 
 let definition_body = definition_body_red None
 
@@ -93,17 +92,15 @@ let parameter_def_var ident c =
   let c = interp_type Evd.empty (Global.env()) c in
   declare_parameter (id_of_string ident) c;
   if is_verbose() then message (ident ^ " is assumed")
-    
+
+let declare_global_assumption ident c =
+  parameter_def_var ident c;
+  wARNING [< 'sTR ident; 'sTR" is declared as a parameter";
+             'sTR" because it is at a global level" >]
+
 let hypothesis_def_var is_refining ident n c =
-  let warning () = 
-    mSGERRNL [< 'sTR"Warning: "; 'sTR ident; 
-                'sTR" is declared as a parameter";
-                'sTR" because it is at a global level" >]
-  in
   match n with
-    | NeverDischarge -> 
-	parameter_def_var ident c;
-	warning()
+    | NeverDischarge -> declare_global_assumption ident c
     | DischargeAt disch_sp ->
         if Lib.is_section_p disch_sp then begin
 	  let t = interp_type Evd.empty (Global.env()) c in
@@ -113,10 +110,9 @@ let hypothesis_def_var is_refining ident n c =
           if is_refining then 
             mSGERRNL [< 'sTR"Warning: Variable "; 'sTR ident; 
                         'sTR" is not visible from current goals" >]
-        end else begin
-          parameter_def_var ident c;
-	  warning()
-	end
+        end
+	else
+	  declare_global_assumption ident c
 
 (* 3| Mutual Inductive definitions *)