Move [delayed] to util and use [force_delayed] everywhere to force

thunks. Move from [lazy] to [delayed] in subtac.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13227 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 6 insertions, 0 deletions

diff --git a/lib/util.mli b/lib/util.mli
index f8fbc1f68c..bbef3462ad 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -291,6 +291,12 @@ val iterate : ('a -> 'a) -> int -> 'a -> 'a
 val repeat : int -> ('a -> unit) -> 'a -> unit
 val iterate_for : int -> int -> (int -> 'a -> 'a) -> 'a -> 'a
 
+(** {6 Delayed computations. } *)
+
+type 'a delayed = unit -> 'a
+
+val delayed_force : 'a delayed -> 'a
+
 (** {6 Misc. } *)
 
 type ('a,'b) union = Inl of 'a | Inr of 'b