diff options
author | Stephane Glondu <steph@glondu.net> | 2010-08-06 16:15:08 -0400 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-08-06 16:17:55 -0400 |
commit | f18e6146f4fd6ed5b8ded10a3e602f5f64f919f4 (patch) | |
tree | c413c5bb42d20daf5307634ae6402526bb994fd6 /interp/coqlib.mli | |
parent | b9f47391f7f259c24119d1de0a87839e2cc5e80c (diff) |
Imported Upstream version 8.3~rc1+dfsgupstream/8.3.rc1.dfsg
Diffstat (limited to 'interp/coqlib.mli')
-rw-r--r-- | interp/coqlib.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/interp/coqlib.mli b/interp/coqlib.mli index 12791139..81cc3baa 100644 --- a/interp/coqlib.mli +++ b/interp/coqlib.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: coqlib.mli 13332 2010-07-26 22:12:43Z msozeau $ i*) (*i*) open Names @@ -14,6 +14,7 @@ open Libnames open Nametab open Term open Pattern +open Util (*i*) (*s This module collects the global references, constructions and @@ -86,9 +87,8 @@ val glob_jmeq : global_reference at compile time. Therefore, we can only provide methods to build them at runtime. This is the purpose of the [constr delayed] and [constr_pattern delayed] types. Objects of this time needs to be - applied to [()] to get the actual constr or pattern at runtime *) - -type 'a delayed = unit -> 'a + forced with [delayed_force] to get the actual constr or pattern + at runtime. *) type coq_bool_data = { andb : constr; |