From 55ce117e8083477593cf1ff2e51a3641c7973830 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Tue, 13 Feb 2007 13:48:12 +0000
Subject: Imported Upstream version 8.1+dfsg

---
 theories/Lists/ListTactics.v | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

(limited to 'theories/Lists')

diff --git a/theories/Lists/ListTactics.v b/theories/Lists/ListTactics.v
index a3b4e647..e46f1279 100644
--- a/theories/Lists/ListTactics.v
+++ b/theories/Lists/ListTactics.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ListTactics.v 9290 2006-10-26 19:20:42Z herbelin $ i*)
+(*i $Id: ListTactics.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
 
 Require Import BinPos.
 Require Import List.
@@ -17,6 +17,14 @@ Ltac list_fold_right fcons fnil l :=
   | nil => fnil
   end.
 
+Ltac lazy_list_fold_right fcons fnil l :=
+  match l with
+  | (cons ?x ?tl) => 
+       let cont := lazy_list_fold_right fcons fnil in
+       fcons x cont tl
+  | nil => fnil 
+  end.
+
 Ltac list_fold_left fcons fnil l :=
   match l with
   | (cons ?x ?tl) => list_fold_left fcons ltac:(fcons x fnil) tl
-- 
cgit v1.2.3