From 4f70016289f15526b162582fc267374e2b60448e Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 30 Jun 2010 19:43:44 +0000
Subject: 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
---
 lib/util.ml | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'lib/util.ml')

diff --git a/lib/util.ml b/lib/util.ml
index ad48e7981a..2711eee24a 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -1179,6 +1179,12 @@ let iterate_for a b f x =
   let rec iterate i v = if i > b then v else iterate (succ i) (f i v) in
   iterate a x
 
+(* Delayed computations *)
+
+type 'a delayed = unit -> 'a
+
+let delayed_force f = f ()
+
 (* Misc *)
 
 type ('a,'b) union = Inl of 'a | Inr of 'b
-- 
cgit v1.2.3