diff options
| author | Matej Kosik | 2017-02-02 10:04:16 +0100 |
|---|---|---|
| committer | Matej Košík | 2017-04-20 13:11:50 +0200 |
| commit | b3ef24e5008c70801d272aa77251ab0bf4b46855 (patch) | |
| tree | 544c7fc7aea88230080bb46ccf7c22426c59b90a /interp | |
| parent | c86c6558fcf7f8dc4a17aceed24f68f756f28ea9 (diff) | |
correcting a typo in a comment
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/coqlib.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/coqlib.mli b/interp/coqlib.mli index 5ba26d8286..1facb47e1e 100644 --- a/interp/coqlib.mli +++ b/interp/coqlib.mli @@ -19,7 +19,7 @@ open Util (** [find_reference caller_message [dir;subdir;...] s] returns a global reference to the name dir.subdir.(...).s; the corresponding module must have been required or in the process of being compiled so that - it must be used lazyly; it raises an anomaly with the given message + it must be used lazily; it raises an anomaly with the given message if not found *) type message = string |