1 files changed, 69 insertions, 0 deletions
diff --git a/theories/Lists/ListTactics.v b/theories/Lists/ListTactics.v
new file mode 100644
index 00000000..a3b4e647
--- /dev/null
+++ b/theories/Lists/ListTactics.v
@@ -0,0 +1,69 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: ListTactics.v 9290 2006-10-26 19:20:42Z herbelin $ i*)
+
+Require Import BinPos.
+Require Import List.
+
+Ltac list_fold_right fcons fnil l :=
+  match l with
+  | (cons ?x ?tl) => fcons x ltac:(list_fold_right fcons fnil 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
+  | nil => fnil
+  end.
+
+Ltac list_iter f l :=
+  match l with
+  | (cons ?x ?tl) => f x; list_iter f tl
+  | nil => idtac
+  end.
+
+Ltac list_iter_gen seq f l :=
+  match l with
+  | (cons ?x ?tl) =>
+      let t1 _ := f x in
+      let t2 _ := list_iter_gen seq f tl in
+      seq t1 t2
+  | nil => idtac
+  end.
+
+Ltac AddFvTail a l :=
+ match l with
+ | nil          => constr:(cons a l)
+ | (cons a _)   => l
+ | (cons ?x ?l) => let l' := AddFvTail a l in constr:(cons x l')
+ end.
+
+Ltac Find_at a l :=
+ let rec find n l :=
+   match l with
+   | nil => fail 100 "anomaly: Find_at"
+   | (cons a _) => eval compute in n
+   | (cons _ ?l) => find (Psucc n) l
+   end
+ in find 1%positive l.
+
+Ltac check_is_list t :=
+  match t with
+  | cons _ ?l => check_is_list l
+  | nil => idtac
+  | _ => fail 100 "anomaly: failed to build a canonical list"
+  end.
+
+Ltac check_fv l :=
+  check_is_list l;
+  match type of l with 
+  | list _ => idtac
+  | _ => fail 100 "anomaly: built an ill-typed list"
+  end.