diff options
| author | Enrico Tassi | 2018-07-26 18:15:12 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2018-07-26 18:15:12 +0200 |
| commit | 06c78339555a47cebc0f2c0ce4daa6c97488024d (patch) | |
| tree | 27ae59b7b85001deb44c8b18867df5012878b6ca /printing | |
| parent | 85d5f45d7a5374646a31f8829965bbfed0a95070 (diff) | |
| parent | 32caa7b700cb2f561edec9b86fbb4583d2962d4d (diff) | |
Merge PR #8101: Remove ClosedModule and ClosedSection from libstack
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/prettyp.ml | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 7258bb9b72..8b835310de 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -657,14 +657,10 @@ 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 _) -> Some (str " >>>>>>> Module " ++ pr_name oname) - | (oname,Lib.ClosedModule _) -> - Some (str " >>>>>>> Closed Module " ++ pr_name oname) let gallina_print_context env sigma with_values = let rec prec n = function @@ -793,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 |