Small fix in IStream interface.

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

3 files changed, 8 insertions, 11 deletions

diff --git a/lib/iStream.ml b/lib/iStream.ml
index 33424b6e44..64cbb5807e 100644
--- a/lib/iStream.ml
+++ b/lib/iStream.ml
@@ -12,9 +12,13 @@ type 'a node =
 
 and 'a t = 'a node Lazy.t
 
-let empty = Lazy.lazy_from_val Nil
+let lift (n : 'a node) : 'a t = Obj.magic n
+(** Small hack to overcome a missing optimization in OCaml compilation of lazy
+    values. *)
 
-let cons x s = Lazy.lazy_from_val (Cons (x, s))
+let empty = lift Nil
+
+let cons x s = lift (Cons (x, s))
 
 let thunk s = lazy (Lazy.force (Lazy.force s))
 
@@ -76,5 +80,3 @@ let rec concat_node = function
 
 and concat (s : 'a t t) =
   thunk (lazy (concat_node (Lazy.force s)))
-
-let lempty = empty
diff --git a/lib/iStream.mli b/lib/iStream.mli
index 2fcc92675a..caae0ad35a 100644
--- a/lib/iStream.mli
+++ b/lib/iStream.mli
@@ -36,9 +36,7 @@ val peek : 'a t -> ('a * 'a t) option
 
 (** {6 Standard operations}
 
-  The complexity of stream-returning functions depends on the lazy status of the
-  actual content of the stream, i.e. a lazy stream will be processed lazily.
-  Other functions are eager. *)
+    All stream-returning functions are lazy. The other ones are eager. *)
 
 val app : 'a t -> 'a t -> 'a t
 (** Append two streams. Not tail-rec. *)
@@ -70,6 +68,3 @@ val to_list : 'a t -> 'a list
 
 val force : 'a t -> 'a t
 (** Forces the whole stream. *)
-
-val lempty : 'a t
-(** Lazy empty stream. *)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 1918ddc0cb..1b460b060b 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -984,7 +984,7 @@ let match_pat refresh lmatch hyp gl = function
       let lmeta = extended_matches t hyp in
       let lmeta = verify_metas_coherence gl lmatch lmeta in
       let ans = { e_ctx = Id.Map.empty; e_sub = lmeta; } in
-      IStream.cons ans IStream.lempty
+      IStream.cons ans IStream.empty
     with PatternMatchingFailure | Not_coherent_metas -> IStream.empty
   end
 | Subterm (b,ic,t) ->