diff options
author | 2003-03-26 15:16:19 +0000 | |
---|---|---|
committer | 2003-03-26 15:16:19 +0000 | |
commit | 611bab7e223707ab23ee4b6d9f074dd6981e1ff3 (patch) | |
tree | 8e60639cbc22f438a45f52f0114529b6926a196b /library/lib.ml | |
parent | 8e13e6233ee4fc002f42290f1b7ae64a6e627162 (diff) |
ajout d'une fonction reset_mod
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3791 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/lib.ml')
-rw-r--r-- | library/lib.ml | 33 |
1 files changed, 33 insertions, 0 deletions
diff --git a/library/lib.ml b/library/lib.ml index c686e2ccf..985d9efba 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 |