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 | |
| parent | 20a464396fd89449569dc69b8cfb37cb69766733 (diff) | |
Fixing typos - Part 2
Diffstat (limited to 'library')
| -rw-r--r-- | library/declaremods.ml | 2 | ||||
| -rw-r--r-- | library/library.ml | 4 | ||||
| -rw-r--r-- | library/nametab.mli | 2 | ||||
| -rw-r--r-- | library/summary.mli | 2 |
4 files changed, 5 insertions, 5 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml index 5fd11e187a..d74bdd484c 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -51,7 +51,7 @@ let inl2intopt = function - Then comes either the object segment itself (for interactive modules), or a compact way to store derived objects (path to - a earlier module + subtitution). + a earlier module + substitution). *) type algebraic_objects = 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. *) diff --git a/library/nametab.mli b/library/nametab.mli index a4f177aad0..33cb4faf99 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -38,7 +38,7 @@ open Globnames } {- [exists : full_user_name -> bool] - Is the [full_user_name] already atributed as an absolute user name + Is the [full_user_name] already attributed as an absolute user name of some object? } {- [locate : qualid -> object_reference] diff --git a/library/summary.mli b/library/summary.mli index 0d77d725ac..3875bcfe9e 100644 --- a/library/summary.mli +++ b/library/summary.mli @@ -28,7 +28,7 @@ type 'a summary_declaration = { Beware: for tables registered dynamically after the initialization of Coq, their init functions may not be run immediately. It is hence - the responsability of plugins to initialize themselves properly. + the responsibility of plugins to initialize themselves properly. *) val declare_summary : string -> 'a summary_declaration -> unit |