Mise en place de noms contenant la section pour Fact et Remark

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

4 files changed, 12 insertions, 1 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 53a6ef83f5..7bede57581 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -172,7 +172,7 @@ let cache_constant (sp,(cdt,stre,op)) =
   Nametab.push 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 ())) -> ()
+    | 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);
@@ -219,6 +219,10 @@ let declare_constant id cd =
   if is_implicit_args() then declare_constant_implicits sp;
   sp
 
+let redeclare_constant sp cd =
+  add_absolutely_named_lead sp (in_constant cd);
+  if is_implicit_args() then declare_constant_implicits sp
+
 (* Inductives. *)
 
 
diff --git a/library/declare.mli b/library/declare.mli
index e17be37e3a..08c45f4626 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -52,6 +52,8 @@ type constant_declaration = constant_declaration_type * strength * opacity
    the full path of the declaration *)
 val declare_constant : identifier -> constant_declaration -> constant_path
 
+val redeclare_constant : constant_path -> constant_declaration -> unit
+
 val declare_parameter : identifier -> constr -> constant_path
 
 (* [declare_mind me] declares a block of inductive types with
diff --git a/library/lib.ml b/library/lib.ml
index 5995a9600d..94cba5e0cc 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -95,6 +95,10 @@ let add_anonymous_entry node =
   add_entry sp node;
   sp
 
+let add_absolutely_named_lead sp obj =
+  cache_object (sp,obj);
+  add_entry sp (Leaf obj)
+
 let add_leaf id kind obj =
   let sp = make_path id kind in
   cache_object (sp,obj);
diff --git a/library/lib.mli b/library/lib.mli
index 4c802a0f80..27fec78bfa 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -34,6 +34,7 @@ and library_segment = library_entry list
   current list of operations (most recent ones coming first). *)
 
 val add_leaf : identifier -> path_kind -> obj -> section_path
+val add_absolutely_named_lead : section_path -> obj -> unit
 val add_anonymous_leaf : obj -> unit
 val add_frozen_state : unit -> unit