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

2 files changed, 3 insertions, 6 deletions

diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 54a1d61491..76a4cf88a9 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -180,14 +180,11 @@ type coq_bool_data  = {
   andb_prop : constr;
   andb_true_intro : constr}
 
-type 'a delayed = unit -> 'a
-
 let build_bool_type () =
   { andb =  init_constant ["Datatypes"] "andb";
     andb_prop =  init_constant ["Datatypes"] "andb_prop";
     andb_true_intro =  init_constant ["Datatypes"] "andb_true_intro" }
 
-
 let build_sigma_set () = anomaly "Use build_sigma_type"
 
 let build_sigma_type () =
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index 73427d902d..c4693479b9 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -11,6 +11,7 @@ open Libnames
 open Nametab
 open Term
 open Pattern
+open Util
 
 (** This module collects the global references, constructions and
     patterns of the standard library used in ocaml files *)
@@ -84,9 +85,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;