diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-07 16:01:55 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-07 16:01:55 +0000 |
commit | 07947f6e3b3327f10f99d02227635eaedf615733 (patch) | |
tree | 4f9af77289a6227e0b549dc77561867cddd3ea92 /library | |
parent | 04e56c85ba8aca14bdc1360a9d2212994c7e359c (diff) |
Probleme synchronisation roots / inputstate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1346 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library')
-rwxr-xr-x | library/nametab.ml | 20 |
1 files changed, 12 insertions, 8 deletions
diff --git a/library/nametab.ml b/library/nametab.ml index 821de2a0b..4e6b81d3b 100755 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -148,12 +148,13 @@ let constant_sp_of_id id = | ConstRef sp -> sp | _ -> raise Not_found -let check_absoluteness = function - | a::_ when List.mem a !roots -> () - | l -> anomaly ("Not an absolute path: "^(string_of_dirpath l)) +let check_absoluteness sp = + match dirpath sp with + | a::_ when List.mem a !roots -> () + | _ -> anomaly ("Not an absolute path: "^(string_of_path sp)) let absolute_reference sp = - check_absoluteness (dirpath sp); + check_absoluteness sp; locate (qualid_of_sp sp) (* These are entry points to make the contents of a module/section visible *) @@ -185,11 +186,14 @@ let exists_module sp = (********************************************************************) (* Registration of persistent tables as a global table and rollback *) -type frozen = module_contents * dir_path list +(* Warning: We do not register roots, because otherwise option -R is + overwritten by the next input state *) -let init () = persistent_nametab := empty; roots := [] -let freeze () = !persistent_nametab, !roots -let unfreeze (mc,r) = persistent_nametab := mc; roots := r +type frozen = module_contents + +let init () = persistent_nametab := empty +let freeze () = !persistent_nametab +let unfreeze mc = persistent_nametab := mc let _ = Summary.declare_summary "persistent-names" |