diff options
| author | Maxime Dénès | 2018-07-19 23:58:52 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-07-20 18:43:37 +0200 |
| commit | 32caa7b700cb2f561edec9b86fbb4583d2962d4d (patch) | |
| tree | 96071b71c12b72b0932c044f5bc2a4eb28f536de /printing | |
| parent | 6a9d0dc7b5c9a6a1c10c0c94eba5e72543080399 (diff) | |
Also remove ClosedSection (same reasoning as ClosedModule)
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/prettyp.ml | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 6911013464..170b96280f 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -657,8 +657,6 @@ let gallina_print_library_entry env sigma with_values ent = gallina_print_leaf_entry env sigma with_values (oname,lobj) | (oname,Lib.OpenedSection (dir,_)) -> Some (str " >>>>>>> Section " ++ pr_name oname) - | (oname,Lib.ClosedSection _) -> - Some (str " >>>>>>> Closed Section " ++ pr_name oname) | (_,Lib.CompilingLibrary { obj_dir; _ }) -> Some (str " >>>>>>> Library " ++ DirPath.print obj_dir) | (oname,Lib.OpenedModule _) -> @@ -791,9 +789,6 @@ let read_sec_context qid = let rec get_cxt in_cxt = function | (_,Lib.OpenedSection ({obj_dir;_},_) as hd)::rest -> if DirPath.equal dir obj_dir then (hd::in_cxt) else get_cxt (hd::in_cxt) rest - | (_,Lib.ClosedSection _)::rest -> - user_err Pp.(str "Cannot print the contents of a closed section.") - (* LEM: Actually, we could if we wanted to. *) | [] -> [] | hd::rest -> get_cxt (hd::in_cxt) rest in |