ajout d'une fonction reset_mod

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

2 files changed, 34 insertions, 0 deletions

diff --git a/library/lib.ml b/library/lib.ml
index c686e2ccf0..985d9efba8 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -140,6 +140,13 @@ let find_entry_p p =
   in
   find !lib_stk
 
+let find_split_p p = 
+  let rec find = function
+    | [] -> raise Not_found
+    | ent::l -> if p ent then ent,l else find l
+  in
+  find !lib_stk
+
 let split_lib sp = 
   let rec collect after equal = function
     | ((sp',_) as hd)::before ->
@@ -432,6 +439,32 @@ let reset_name (loc,id) =
   in
   reset_to sp
 
+let is_mod_node = function 
+  | OpenedModule _ | OpenedModtype _ | OpenedSection _ 
+  | ClosedSection _ -> true | _ -> false
+
+(* Reset on a module or section name in order to bypass constants with 
+   the same name *) 
+
+let reset_mod (loc,id) =
+  let (ent,before) = 
+    try
+      find_split_p (fun (sp,node) -> 
+                    let (_,spi) = repr_path (fst sp) in id = spi 
+                    && is_mod_node node)
+    with Not_found ->
+      user_err_loc (loc,"reset_mod",pr_id id ++ str ": no such entry")
+  in
+  lib_stk := before;
+  recalc_path_prefix ();
+  let spf = match find_entry_p is_frozen_state with
+    | (sp, FrozenState f) -> unfreeze_summaries f; sp
+    | _ -> assert false
+  in
+  let (after,_,_) = split_lib spf in
+  recache_context after
+
+
 let point_obj =
   let (f,_) = declare_object {(default_object "DOT") with
 				classify_function = (fun _ -> Dispose)} in
diff --git a/library/lib.mli b/library/lib.mli
index 6acb565a8f..2f51d441d9 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -128,6 +128,7 @@ val close_section : export:bool -> identifier ->
 
 val reset_to : object_name -> unit
 val reset_name : identifier located -> unit
+val reset_mod : identifier located -> unit
 
 (* [back n] resets to the place corresponding to the $n$-th call of 
    [mark_end_of_command] (counting backwards) *)