diff options
author | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-03-17 20:14:19 +0000 |
---|---|---|
committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-03-17 20:14:19 +0000 |
commit | f848b8bf579ed8fa7613174388a8fbc9ab2f6344 (patch) | |
tree | 432b42016aa61fd459849991dd750897a0831e88 /theories/Lists/ListTactics.v | |
parent | 1b3cd12fcb148a743aec66e5ac9f6e6e9eadeb32 (diff) |
- gros commit sur ring et field: passage des arguments simplifie
- tacinterp.ml: les arguments tactiques de Tactic Notation n'etaient
pas evalues, laissant des variables libres (symptome: exc Not_found)
- reals: Open Local --> Local Open
- ListTactics: syntaxe des listes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11989 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Lists/ListTactics.v')
-rw-r--r-- | theories/Lists/ListTactics.v | 30 |
1 files changed, 15 insertions, 15 deletions
diff --git a/theories/Lists/ListTactics.v b/theories/Lists/ListTactics.v index 233b40b88..017a2fe2a 100644 --- a/theories/Lists/ListTactics.v +++ b/theories/Lists/ListTactics.v @@ -13,13 +13,13 @@ 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) + | ?x :: ?tl => fcons x ltac:(list_fold_right fcons fnil tl) | nil => fnil end. Ltac lazy_list_fold_right fcons fnil l := match l with - | (cons ?x ?tl) => + | ?x :: ?tl => let cont := lazy_list_fold_right fcons fnil in fcons x cont tl | nil => fnil @@ -27,19 +27,19 @@ Ltac lazy_list_fold_right fcons fnil l := Ltac list_fold_left fcons fnil l := match l with - | (cons ?x ?tl) => list_fold_left fcons ltac:(fcons x fnil) tl + | ?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 + | ?x :: ?tl => f x; list_iter f tl | nil => idtac end. Ltac list_iter_gen seq f l := match l with - | (cons ?x ?tl) => + | ?x :: ?tl => let t1 _ := f x in let t2 _ := list_iter_gen seq f tl in seq t1 t2 @@ -48,30 +48,30 @@ Ltac list_iter_gen seq f l := 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') + | nil => constr:(a::nil) + | a :: _ => l + | ?x :: ?l => let l' := AddFvTail a l in constr:(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 + | nil => fail 100 "anomaly: Find_at" + | a :: _ => eval compute in n + | _ :: ?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" + | _ :: ?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" + | _ => fail 100 "anomaly: built an ill-typed list" end. |