diff options
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 eded75be9d..2122e3a8f9 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 da57d90023..84022e7b1f 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 -> () |