aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/pretty.ml
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/pretty.ml')
-rw-r--r--parsing/pretty.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index 7c4c40aa1..1d1deed7d 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -248,7 +248,7 @@ let rec print_library_entry with_values ent =
match ent with
| (sp,Lib.Leaf lobj) ->
[< print_leaf_entry with_values sep (sp,lobj) >]
- | (_,Lib.OpenedSection str) ->
+ | (_,Lib.OpenedSection (str,_)) ->
[< 'sTR(" >>>>>>> Section " ^ str); 'fNL >]
| (sp,Lib.ClosedSection _) ->
[< 'sTR(" >>>>>>> Closed Section " ^ (string_of_id (basename sp)));
@@ -286,7 +286,7 @@ let list_filter_vec f vec =
let read_sec_context sec =
let rec get_cxt in_cxt = function
- | ((sp,Lib.OpenedSection str) as hd)::rest ->
+ | ((sp,Lib.OpenedSection (str,_)) as hd)::rest ->
if str = sec then (hd::in_cxt) else get_cxt (hd::in_cxt) rest
| [] -> []
| hd::rest -> get_cxt (hd::in_cxt) rest