diff options
Diffstat (limited to 'theories/Lists/ListTactics.v')
| -rw-r--r-- | theories/Lists/ListTactics.v | 10 |
1 files changed, 9 insertions, 1 deletions
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 |