From 9f6f2eda9b288cd31186a7348eca82ea73dbf39b Mon Sep 17 00:00:00 2001
From: barras
Date: Wed, 18 Mar 2009 14:47:35 +0000
Subject: fixed ring/field warning about hyp cleaning up

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11993 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Lists/ListTactics.v | 16 ++++++++++------
 1 file changed, 10 insertions(+), 6 deletions(-)

(limited to 'theories')

diff --git a/theories/Lists/ListTactics.v b/theories/Lists/ListTactics.v
index 017a2fe2a0..2da70c4673 100644
--- a/theories/Lists/ListTactics.v
+++ b/theories/Lists/ListTactics.v
@@ -17,13 +17,17 @@ Ltac list_fold_right fcons fnil l :=
   | nil => fnil
   end.
 
+(* A variant of list_fold_right, to prevent the match of list_fold_right
+   from catching errors raised by fcons. *)
 Ltac lazy_list_fold_right fcons fnil l :=
-  match l with
-  | ?x :: ?tl => 
-       let cont := lazy_list_fold_right fcons fnil in
-       fcons x cont tl
-  | nil => fnil 
-  end.
+  let f :=
+    match l with
+    | ?x :: ?tl => 
+         fun _ =>
+         fcons x ltac:(fun _ => lazy_list_fold_right fcons fnil tl)
+    | nil => fun _ => fnil() 
+    end in
+  f().
 
 Ltac list_fold_left fcons fnil l :=
   match l with
-- 
cgit v1.2.3