diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/declaremods.ml | 2 | ||||
| -rw-r--r-- | library/libnames.ml | 3 | ||||
| -rw-r--r-- | library/libnames.mli | 3 | ||||
| -rw-r--r-- | library/library.ml | 4 | ||||
| -rw-r--r-- | library/nametab.mli | 2 | ||||
| -rw-r--r-- | library/summary.mli | 2 |
6 files changed, 11 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/libnames.ml b/library/libnames.ml index 87c4de42e8..41b38e0378 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -162,6 +162,9 @@ let qualid_basename qid = let qualid_path qid = qid.CAst.v.dirpath +let idset_mem_qualid qid s = + qualid_is_ident qid && Id.Set.mem (qualid_basename qid) s + (* Default paths *) let default_library = Names.DirPath.initial (* = ["Top"] *) diff --git a/library/libnames.mli b/library/libnames.mli index bbb4d2a058..7d77d95991 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -88,6 +88,9 @@ val qualid_is_ident : qualid -> bool val qualid_path : qualid -> DirPath.t val qualid_basename : qualid -> Id.t +val idset_mem_qualid : qualid -> Id.Set.t -> bool +(** false when the qualid is not an ident *) + (** {6 ... } *) (** some preset paths *) diff --git a/library/library.ml b/library/library.ml index f99bcc7ecf..9f4eb531ed 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 @@ -268,7 +268,7 @@ let in_import_library : DirPath.t list * bool -> obj = (** {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 |