Transformation de Remark/Fact en constantes non visibles sans qualification

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

3 files changed, 27 insertions, 11 deletions

diff --git a/library/declare.ml b/library/declare.ml
index c07a8577f7..53a6ef83f5 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -123,7 +123,10 @@ let load_parameter (sp,_) =
 let open_parameter (sp,_) =
   Nametab.push_short_name sp (ConstRef sp)
 
-let export_parameter x = Some x
+(* Hack to reduce the size of .vo: we keep only what load/open needs *)
+let dummy_parameter_entry = mkProp
+
+let export_parameter c = Some dummy_parameter_entry
 
 let (in_parameter, out_parameter) =
   let od = {
@@ -167,7 +170,12 @@ let cache_constant (sp,(cdt,stre,op)) =
     | ConstantRecipe r -> Global.add_discharged_constant sp r sc
   end;
   Nametab.push sp (ConstRef sp);
-  Nametab.push_short_name sp (ConstRef sp);
+  (match stre with
+    (* Remark & Fact outside their scope aren't visible without qualif *)
+    | DischargeAt sp when not (is_dirpath_prefix_of sp (Lib.cwd ())) -> ()
+    (* Theorem, Lemma & Definition are accessible from the base name *)
+    | NeverDischarge| DischargeAt _ -> Nametab.push_short_name sp (ConstRef sp)
+    | NotDeclare -> assert false);
   if op then Global.set_opaque sp;
   csttab := Spmap.add sp stre !csttab
 
diff --git a/library/nametab.ml b/library/nametab.ml
index a33bb97055..1fadea6aeb 100755
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -78,23 +78,31 @@ let dirpath_of_extended_ref = function
   | TrueGlobal ref -> dirpath_of_reference ref
   | SyntacticDef sp -> dirpath sp
 
-(* How necessarily_open works: concretely, roots and directory are
-   always open but libraries are open only during their interactive
-   construction or on demand if a precompiled one; then for a name
+(* How [visibility] works: a value of [0] means all suffixes of [dir] are
+   allowed to access the object, a value of [1] means all suffixes, except the
+   base name, are available, [2] means all suffixes except the base name and
+   the name qualified by the module name *)
+
+(* Concretely, library roots and directory are
+   always open but modules/files are open only during their interactive
+   construction or on demand if a precompiled one: for a name
    "Root.Rep.Lib.name", then "Lib.name", "Rep.Lib.name" and
-   "Root.Rep.Lib.name", but not "name" are pushed *)
+   "Root.Rep.Lib.name", but not "name" are pushed; which means, visibility is
+   always 1 *)
+
+let visibility = 1
 
 (* We add a binding of [[modid1;...;modidn;id]] to [o] in the name tab *)
 (* We proceed in the reverse way, looking first to [id] *)
 let push_tree extract_dirpath tab dir o =
-  let rec push necessarily_open (current,dirmap) = function
+  let rec push level (current,dirmap) = function
     | modid :: path as dir ->
 	let mc = 
 	  try ModIdmap.find modid dirmap
 	  with Not_found -> (None, ModIdmap.empty)
 	in
 	let this =
-          if necessarily_open then
+          if level >= visibility then
             if option_app extract_dirpath current = Some dir then
               (* This is an absolute name, we must keep it otherwise it may
                  become unaccessible forever *)
@@ -102,9 +110,9 @@ let push_tree extract_dirpath tab dir o =
             else
               Some o
           else current in
-	(this, ModIdmap.add modid (push true mc path) dirmap)
+	(this, ModIdmap.add modid (push (level+1) mc path) dirmap)
     | [] -> (Some o,dirmap) in
-  push false tab (List.rev dir)
+  push 0 tab (List.rev dir)
 
 let push_idtree extract_dirpath tab dir id o =
   let modtab =
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 5620473fe5..f53f26b8d4 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -437,7 +437,7 @@ let apply_tac_not_declare id pft = function
 let save opacity id ({const_entry_body = pft; const_entry_type = tpo} as const)
   strength =
   begin match strength with
-    | DischargeAt disch_sp when Lib.is_section_p disch_sp (*&& not opacity*) ->
+    | DischargeAt disch_sp when Lib.is_section_p disch_sp && not opacity ->
 	let c = constr_of_constr_entry const in
 	let _ = declare_variable id (SectionLocalDef c,strength,opacity) in ()
     | NeverDischarge | DischargeAt _ ->