diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-02-20 18:13:28 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-02-20 18:13:28 +0000 |
| commit | 4231d1907b1277bb45e86909a07d6fc893fa89fa (patch) | |
| tree | a0fc5227294ab87f2319e53cfff05210841481f4 /parsing | |
| parent | 5be5a0ff384bbac3bc529860793e975189c3c110 (diff) | |
Keep ClosedSection marker for reset
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6758 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/prettyp.ml | 6 | ||||
| -rw-r--r-- | parsing/search.ml | 2 |
2 files changed, 4 insertions, 4 deletions
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index eded75be9..2122e3a8f 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -390,7 +390,7 @@ let rec print_library_entry with_values ent = print_leaf_entry with_values sep (oname,lobj) | (oname,Lib.OpenedSection (dir,_)) -> Some (str " >>>>>>> Section " ++ pr_name oname) - | (oname,Lib.ClosedSection _) -> + | (oname,Lib.ClosedSection) -> Some (str " >>>>>>> Closed Section " ++ pr_name oname) | (_,Lib.CompilingLibrary (dir,_)) -> Some (str " >>>>>>> Library " ++ pr_dirpath dir) @@ -440,9 +440,9 @@ let read_sec_context r = with Not_found -> user_err_loc (loc,"read_sec_context", str "Unknown section") in let rec get_cxt in_cxt = function - | ((_,Lib.OpenedSection ((dir',_),_)) as hd)::rest -> + | (_,Lib.OpenedSection ((dir',_),_) as hd)::rest -> if dir = dir' then (hd::in_cxt) else get_cxt (hd::in_cxt) rest - | ((_,Lib.ClosedSection (_,_,ctxt)) as hd)::rest -> + | (_,Lib.ClosedSection)::rest -> error "Cannot print the contents of a closed section" | [] -> [] | hd::rest -> get_cxt (hd::in_cxt) rest diff --git a/parsing/search.ml b/parsing/search.ml index da57d9002..84022e7b1 100644 --- a/parsing/search.ml +++ b/parsing/search.ml @@ -80,7 +80,7 @@ let gen_crible refopt (fn : global_reference -> env -> constr -> unit) = | _ -> () in try - Declaremods.iter_all_segments false crible_rec + Declaremods.iter_all_segments crible_rec with Not_found -> () |