diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 17 |
1 files changed, 8 insertions, 9 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 29f3b321f..09c63fc43 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -488,15 +488,14 @@ let vernac_end_section = Lib.close_section let vernac_end_segment id = check_no_pending_proofs (); - let o = - try Lib.what_is_opened () - with Not_found -> error "There is nothing to end." in - match o with - | _,Lib.OpenedModule (export,_,_) -> vernac_end_module export id - | _,Lib.OpenedModtype _ -> vernac_end_modtype id - | _,Lib.OpenedSection _ -> vernac_end_section id - | _ -> anomaly "No more opened things" - + let o = try Lib.what_is_opened () with + Not_found -> error "There is nothing to end." in + match o with + | _,Lib.OpenedModule (export,_,_) -> vernac_end_module export id + | _,Lib.OpenedModtype _ -> vernac_end_modtype id + | _,Lib.OpenedSection _ -> vernac_end_section id + | _ -> anomaly "No more opened things" + let vernac_require import _ qidl = let qidl = List.map qualid_of_reference qidl in Library.require_library qidl import |