diff options
| author | JPR | 2019-05-22 21:40:57 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-05-23 01:49:04 +0200 |
| commit | 467eb67bb960c15e1335f375af29b4121ac5262b (patch) | |
| tree | 1ad2454c535b090738748cd8123330451a498854 /library/library.ml | |
| parent | 20a464396fd89449569dc69b8cfb37cb69766733 (diff) | |
Fixing typos - Part 2
Diffstat (limited to 'library/library.ml')
| -rw-r--r-- | library/library.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/library/library.ml b/library/library.ml index 500e77f89b..d8eaf5f659 100644 --- a/library/library.ml +++ b/library/library.ml @@ -208,7 +208,7 @@ let register_open_library export m = let open_library export explicit_libs m = if (* Only libraries indirectly to open are not reopen *) - (* Libraries explicitly mentionned by the user are always reopen *) + (* Libraries explicitly mentioned by the user are always reopen *) List.exists (fun m' -> DirPath.equal m m') explicit_libs || not (library_is_opened m) then begin @@ -347,7 +347,7 @@ let try_locate_absolute_library dir = (** {6 Tables of opaque proof terms} *) (** We now store opaque proof terms apart from the rest of the environment. - See the [Indirect] contructor in [Lazyconstr.lazy_constr]. This way, + See the [Indirect] constructor in [Lazyconstr.lazy_constr]. This way, we can quickly load a first half of a .vo file without these opaque terms, and access them only when a specific command (e.g. Print or Print Assumptions) needs it. *) |