From cd248e01d6834bc43d733c08b5955c332d2146a6 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Thu, 2 Feb 2017 10:04:16 +0100 Subject: comment: typo --- interp/coqlib.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'interp') 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 -- cgit v1.2.3