diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-02 18:50:33 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-02 18:50:33 +0000 |
commit | 0fb8601151a0e316554c95608de2ae4dbdac2ed3 (patch) | |
tree | eef149e1c23427c2bd4943cf72b3a276a3a82808 /theories | |
parent | d70800791ded96209c8f71e682f602201f93d56b (diff) |
Remove various useless {struct} annotations
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12458 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories')
36 files changed, 102 insertions, 110 deletions
diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v index 7cfad89e4..4ddae9372 100644 --- a/theories/Arith/EqNat.v +++ b/theories/Arith/EqNat.v @@ -16,7 +16,7 @@ Implicit Types m n x y : nat. (** * Propositional equality *) -Fixpoint eq_nat n m {struct n} : Prop := +Fixpoint eq_nat n m : Prop := match n, m with | O, O => True | O, S _ => False @@ -68,7 +68,7 @@ Defined. (** * Boolean equality on [nat] *) -Fixpoint beq_nat n m {struct n} : bool := +Fixpoint beq_nat n m : bool := match n, m with | O, O => true | O, S _ => false diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v index c7e81505c..62250fc33 100644 --- a/theories/Arith/Max.v +++ b/theories/Arith/Max.v @@ -16,7 +16,7 @@ Implicit Types m n p : nat. (** * Maximum of two natural numbers *) -Fixpoint max n m {struct n} : nat := +Fixpoint max n m : nat := match n, m with | O, _ => m | S n', O => n diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v index 1cf6d0ed1..62948093f 100644 --- a/theories/Arith/Min.v +++ b/theories/Arith/Min.v @@ -16,7 +16,7 @@ Implicit Types m n p : nat. (** * minimum of two natural numbers *) -Fixpoint min n m {struct n} : nat := +Fixpoint min n m : nat := match n, m with | O, _ => 0 | S n', O => 0 diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v index b6ea04c01..cd6c0a29e 100644 --- a/theories/Arith/Minus.v +++ b/theories/Arith/Minus.v @@ -10,7 +10,7 @@ (** [minus] (difference between two natural numbers) is defined in [Init/Peano.v] as: << -Fixpoint minus (n m:nat) {struct n} : nat := +Fixpoint minus (n m:nat) : nat := match n, m with | O, _ => n | S k, O => S k diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v index 7b48ffe05..8346cae38 100644 --- a/theories/Arith/Mult.v +++ b/theories/Arith/Mult.v @@ -223,7 +223,7 @@ Qed. tail-recursive, whereas [mult] is not. This can be useful when extracting programs. *) -Fixpoint mult_acc (s:nat) m n {struct n} : nat := +Fixpoint mult_acc (s:nat) m n : nat := match n with | O => s | S p => mult_acc (tail_plus m s) m p diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v index cba87f9e5..9b7c62615 100644 --- a/theories/Arith/Plus.v +++ b/theories/Arith/Plus.v @@ -10,7 +10,7 @@ (** Properties of addition. [add] is defined in [Init/Peano.v] as: << -Fixpoint plus (n m:nat) {struct n} : nat := +Fixpoint plus (n m:nat) : nat := match n with | O => m | S p => S (p + m) @@ -198,7 +198,7 @@ Qed. tail-recursive, whereas [plus] is not. This can be useful when extracting programs. *) -Fixpoint tail_plus n m {struct n} : nat := +Fixpoint tail_plus n m : nat := match n with | O => m | S n => tail_plus n (S m) diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v index d142cb77f..5bc5d2a58 100644 --- a/theories/Arith/Wf_nat.v +++ b/theories/Arith/Wf_nat.v @@ -262,7 +262,7 @@ Unset Implicit Arguments. (** [n]th iteration of the function [f] *) -Fixpoint iter_nat (n:nat) (A:Type) (f:A -> A) (x:A) {struct n} : A := +Fixpoint iter_nat (n:nat) (A:Type) (f:A -> A) (x:A) : A := match n with | O => x | S n' => f (iter_nat n' A f x) diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v index 19b6a8164..7ecfa43f2 100644 --- a/theories/Bool/Bvector.v +++ b/theories/Bool/Bvector.v @@ -233,22 +233,19 @@ Definition BshiftRl (n:nat) (bv:Bvector (S n)) (carry:bool) := Definition BshiftRa (n:nat) (bv:Bvector (S n)) := Bhigh (S n) (Vshiftrepeat bool n bv). -Fixpoint BshiftL_iter (n:nat) (bv:Bvector (S n)) (p:nat) {struct p} : - Bvector (S n) := +Fixpoint BshiftL_iter (n:nat) (bv:Bvector (S n)) (p:nat) : Bvector (S n) := match p with | O => bv | S p' => BshiftL n (BshiftL_iter n bv p') false end. -Fixpoint BshiftRl_iter (n:nat) (bv:Bvector (S n)) (p:nat) {struct p} : - Bvector (S n) := +Fixpoint BshiftRl_iter (n:nat) (bv:Bvector (S n)) (p:nat) : Bvector (S n) := match p with | O => bv | S p' => BshiftRl n (BshiftRl_iter n bv p') false end. -Fixpoint BshiftRa_iter (n:nat) (bv:Bvector (S n)) (p:nat) {struct p} : - Bvector (S n) := +Fixpoint BshiftRa_iter (n:nat) (bv:Bvector (S n)) (p:nat) : Bvector (S n) := match p with | O => bv | S p' => BshiftRa n (BshiftRa_iter n bv p') diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v index bafbac3f1..0a35ef45e 100644 --- a/theories/Classes/EquivDec.v +++ b/theories/Classes/EquivDec.v @@ -130,7 +130,7 @@ Require Import List. Program Instance list_eqdec `(eqa : EqDec A eq) : ! EqDec (list A) eq := { equiv_dec := - fix aux (x : list A) y { struct x } := + fix aux (x y : list A) := match x, y with | nil, nil => in_left | cons hd tl, cons hd' tl' => diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v index 9ad2f65cf..56fc35d89 100644 --- a/theories/FSets/FMapList.v +++ b/theories/FSets/FMapList.v @@ -357,7 +357,7 @@ Qed. (** * [equal] *) -Function equal (cmp:elt->elt->bool)(m m' : t elt) { struct m } : bool := +Function equal (cmp:elt->elt->bool)(m m' : t elt) {struct m} : bool := match m, m' with | nil, nil => true | (x,e)::l, (x',e')::l' => @@ -518,13 +518,13 @@ Variable elt':Type. (** * [map] and [mapi] *) -Fixpoint map (f:elt -> elt') (m:t elt) {struct m} : t elt' := +Fixpoint map (f:elt -> elt') (m:t elt) : t elt' := match m with | nil => nil | (k,e)::m' => (k,f e) :: map f m' end. -Fixpoint mapi (f: key -> elt -> elt') (m:t elt) {struct m} : t elt' := +Fixpoint mapi (f: key -> elt -> elt') (m:t elt) : t elt' := match m with | nil => nil | (k,e)::m' => (k,f k e) :: mapi f m' @@ -1171,7 +1171,7 @@ Definition t := MapS.t D.t. Definition cmp e e' := match D.compare e e' with EQ _ => true | _ => false end. -Fixpoint eq_list (m m' : list (X.t * D.t)) { struct m } : Prop := +Fixpoint eq_list (m m' : list (X.t * D.t)) : Prop := match m, m' with | nil, nil => True | (x,e)::l, (x',e')::l' => @@ -1184,7 +1184,7 @@ Fixpoint eq_list (m m' : list (X.t * D.t)) { struct m } : Prop := Definition eq m m' := eq_list m.(this) m'.(this). -Fixpoint lt_list (m m' : list (X.t * D.t)) {struct m} : Prop := +Fixpoint lt_list (m m' : list (X.t * D.t)) : Prop := match m, m' with | nil, nil => False | nil, _ => True diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v index f5ee8b23f..56ad2ed11 100644 --- a/theories/FSets/FMapPositive.v +++ b/theories/FSets/FMapPositive.v @@ -38,7 +38,7 @@ Module PositiveOrderedTypeBits <: UsualOrderedType. Definition eq_sym := @sym_eq t. Definition eq_trans := @trans_eq t. - Fixpoint bits_lt (p q:positive) { struct p } : Prop := + Fixpoint bits_lt (p q:positive) : Prop := match p, q with | xH, xI _ => True | xH, _ => False @@ -117,7 +117,7 @@ End PositiveOrderedTypeBits. (** Other positive stuff *) -Fixpoint append (i j : positive) {struct i} : positive := +Fixpoint append (i j : positive) : positive := match i with | xH => j | xI ii => xI (append ii j) @@ -177,14 +177,14 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Definition empty : t A := Leaf. - Fixpoint is_empty (m : t A) {struct m} : bool := + Fixpoint is_empty (m : t A) : bool := match m with | Leaf => true | Node l None r => (is_empty l) && (is_empty r) | _ => false end. - Fixpoint find (i : positive) (m : t A) {struct i} : option A := + Fixpoint find (i : positive) (m : t A) : option A := match m with | Leaf => None | Node l o r => @@ -195,7 +195,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. end end. - Fixpoint mem (i : positive) (m : t A) {struct i} : bool := + Fixpoint mem (i : positive) (m : t A) : bool := match m with | Leaf => false | Node l o r => @@ -206,7 +206,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. end end. - Fixpoint add (i : positive) (v : A) (m : t A) {struct i} : t A := + Fixpoint add (i : positive) (v : A) (m : t A) : t A := match m with | Leaf => match i with @@ -222,7 +222,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. end end. - Fixpoint remove (i : positive) (m : t A) {struct i} : t A := + Fixpoint remove (i : positive) (m : t A) : t A := match i with | xH => match m with @@ -254,8 +254,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. (** [elements] *) - Fixpoint xelements (m : t A) (i : positive) {struct m} - : list (positive * A) := + Fixpoint xelements (m : t A) (i : positive) : list (positive * A) := match m with | Leaf => nil | Node l None r => @@ -381,7 +380,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. exact (xelements_correct m i xH H). Qed. - Fixpoint xfind (i j : positive) (m : t A) {struct j} : option A := + Fixpoint xfind (i j : positive) (m : t A) : option A := match i, j with | _, xH => find i m | xO ii, xO jj => xfind ii jj m @@ -394,7 +393,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. xfind i (append j (xO xH)) m1 = Some v -> xfind i j (Node m1 o m2) = Some v. Proof. induction j; intros; destruct i; simpl; simpl in H; auto; try congruence. - destruct i; congruence. + destruct i; simpl in *; auto. Qed. Lemma xelements_ii : @@ -821,7 +820,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Variable f : positive -> A -> B. - Fixpoint xmapi (m : t A) (i : positive) {struct m} : t B := + Fixpoint xmapi (m : t A) (i : positive) : t B := match m with | Leaf => @Leaf B | Node l o r => Node (xmapi l (append i (xO xH))) @@ -906,7 +905,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Implicit Arguments Leaf [A]. - Fixpoint xmap2_l (m : t A) {struct m} : t C := + Fixpoint xmap2_l (m : t A) : t C := match m with | Leaf => Leaf | Node l o r => Node (xmap2_l l) (f o None) (xmap2_l r) @@ -918,7 +917,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. induction i; intros; destruct m; simpl; auto. Qed. - Fixpoint xmap2_r (m : t B) {struct m} : t C := + Fixpoint xmap2_r (m : t B) : t C := match m with | Leaf => Leaf | Node l o r => Node (xmap2_r l) (f None o) (xmap2_r r) @@ -930,7 +929,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. induction i; intros; destruct m; simpl; auto. Qed. - Fixpoint _map2 (m1 : t A)(m2 : t B) {struct m1} : t C := + Fixpoint _map2 (m1 : t A)(m2 : t B) : t C := match m1 with | Leaf => xmap2_r m2 | Node l1 o1 r1 => @@ -1028,7 +1027,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. rewrite xfoldi_1; reflexivity. Qed. - Fixpoint equal (A:Type)(cmp : A -> A -> bool)(m1 m2 : t A) {struct m1} : bool := + Fixpoint equal (A:Type)(cmp : A -> A -> bool)(m1 m2 : t A) : bool := match m1, m2 with | Leaf, _ => is_empty m2 | _, Leaf => is_empty m1 diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v index e29bde236..38ed172b8 100644 --- a/theories/FSets/FMapWeakList.v +++ b/theories/FSets/FMapWeakList.v @@ -455,13 +455,13 @@ Variable elt':Type. (** * [map] and [mapi] *) -Fixpoint map (f:elt -> elt') (m:t elt) {struct m} : t elt' := +Fixpoint map (f:elt -> elt') (m:t elt) : t elt' := match m with | nil => nil | (k,e)::m' => (k,f e) :: map f m' end. -Fixpoint mapi (f: key -> elt -> elt') (m:t elt) {struct m} : t elt' := +Fixpoint mapi (f: key -> elt -> elt') (m:t elt) : t elt' := match m with | nil => nil | (k,e)::m' => (k,f k e) :: mapi f m' diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index 9924d8a65..12a8f7a4b 100644 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -89,7 +89,7 @@ Hint Resolve n_Sn: core. (** Addition *) -Fixpoint plus (n m:nat) {struct n} : nat := +Fixpoint plus (n m:nat) : nat := match n with | O => m | S p => S (p + m) @@ -129,7 +129,7 @@ Notation plus_succ_r_reverse := plus_n_Sm (only parsing). (** Multiplication *) -Fixpoint mult (n m:nat) {struct n} : nat := +Fixpoint mult (n m:nat) : nat := match n with | O => 0 | S p => m + p * m @@ -160,7 +160,7 @@ Notation mult_succ_r_reverse := mult_n_Sm (only parsing). (** Truncated subtraction: [m-n] is [0] if [n>=m] *) -Fixpoint minus (n m:nat) {struct n} : nat := +Fixpoint minus (n m:nat) : nat := match n, m with | O, _ => n | S k, O => n diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v index f1baf71a7..3209860f3 100644 --- a/theories/Init/Wf.v +++ b/theories/Init/Wf.v @@ -72,7 +72,7 @@ Section Well_founded. Variable P : A -> Type. Variable F : forall x:A, (forall y:A, R y x -> P y) -> P x. - Fixpoint Fix_F (x:A) (a:Acc x) {struct a} : P x := + Fixpoint Fix_F (x:A) (a:Acc x) : P x := F (fun (y:A) (h:R y x) => Fix_F (Acc_inv a h)). Scheme Acc_inv_dep := Induction for Acc Sort Prop. @@ -129,8 +129,7 @@ Section Well_founded_2. forall (x:A) (x':B), (forall (y:A) (y':B), R (y, y') (x, x') -> P y y') -> P x x'. - Fixpoint Fix_F_2 (x:A) (x':B) (a:Acc R (x, x')) {struct a} : - P x x' := + Fixpoint Fix_F_2 (x:A) (x':B) (a:Acc R (x, x')) : P x x' := F (fun (y:A) (y':B) (h:R (y, y') (x, x')) => Fix_F_2 (x:=y) (x':=y') (Acc_inv a (y,y') h)). diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 01b1c066a..b34bf65b3 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -445,7 +445,7 @@ Section Elts. Hypothesis eq_dec : forall x y : A, {x = y}+{x <> y}. - Fixpoint remove (x : A) (l : list A){struct l} : list A := + Fixpoint remove (x : A) (l : list A) : list A := match l with | nil => nil | y::tl => if (eq_dec x y) then remove x tl else y::(remove x tl) @@ -470,7 +470,7 @@ Section Elts. (** [last l d] returns the last element of the list [l], or the default value [d] if [l] is empty. *) - Fixpoint last (l:list A) (d:A) {struct l} : A := + Fixpoint last (l:list A) (d:A) : A := match l with | nil => d | a :: nil => a @@ -479,7 +479,7 @@ Section Elts. (** [removelast l] remove the last element of [l] *) - Fixpoint removelast (l:list A) {struct l} : list A := + Fixpoint removelast (l:list A) : list A := match l with | nil => nil | a :: nil => nil @@ -530,7 +530,7 @@ Section Elts. Hypotheses eqA_dec : forall x y : A, {x = y}+{x <> y}. - Fixpoint count_occ (l : list A) (x : A){struct l} : nat := + Fixpoint count_occ (l : list A) (x : A) : nat := match l with | nil => 0 | y :: tl => @@ -686,7 +686,7 @@ Section ListOps. (** An alternative tail-recursive definition for reverse *) - Fixpoint rev_append (l l': list A) {struct l} : list A := + Fixpoint rev_append (l l': list A) : list A := match l with | nil => l' | a::l => rev_append l (a::l') @@ -1015,9 +1015,7 @@ Section Map. Lemma in_map : forall (l:list A) (x:A), In x l -> In (f x) (map l). Proof. - induction l as [| a l IHl]; simpl in |- *; - [ auto - | destruct 1; [ left; apply f_equal with (f := f); assumption | auto ] ]. + induction l; firstorder (subst; auto). Qed. Lemma in_map_iff : forall l y, In y (map l) <-> exists x, f x = y /\ In x l. @@ -1067,7 +1065,7 @@ Section Map. (** [flat_map] *) Definition flat_map (f:A -> list B) := - fix flat_map (l:list A) {struct l} : list B := + fix flat_map (l:list A) : list B := match l with | nil => nil | cons x t => (f x)++(flat_map t) @@ -1121,7 +1119,7 @@ Section Fold_Left_Recursor. Variables A B : Type. Variable f : A -> B -> A. - Fixpoint fold_left (l:list B) (a0:A) {struct l} : A := + Fixpoint fold_left (l:list B) (a0:A) : A := match l with | nil => a0 | cons b t => fold_left t (f a0 b) @@ -1214,7 +1212,7 @@ End Fold_Right_Recursor. (** [(list_power x y)] is [y^x], or the set of sequences of elts of [y] indexed by elts of [x], sorted in lexicographic order. *) - Fixpoint list_power (A B:Type)(l:list A) (l':list B) {struct l} : + Fixpoint list_power (A B:Type)(l:list A) (l':list B) : list (list (A * B)) := match l with | nil => cons nil nil @@ -1235,7 +1233,7 @@ End Fold_Right_Recursor. (** find whether a boolean function can be satisfied by an elements of the list. *) - Fixpoint existsb (l:list A) {struct l}: bool := + Fixpoint existsb (l:list A) : bool := match l with | nil => false | a::l => f a || existsb l @@ -1275,7 +1273,7 @@ End Fold_Right_Recursor. (** find whether a boolean function is satisfied by all the elements of a list. *) - Fixpoint forallb (l:list A) {struct l} : bool := + Fixpoint forallb (l:list A) : bool := match l with | nil => true | a::l => f a && forallb l @@ -1326,7 +1324,7 @@ End Fold_Right_Recursor. (** [partition] *) - Fixpoint partition (l:list A) {struct l} : list A * list A := + Fixpoint partition (l:list A) : list A * list A := match l with | nil => (nil, nil) | x :: tl => let (g,d) := partition tl in @@ -1347,7 +1345,7 @@ End Fold_Right_Recursor. (** [split] derives two lists from a list of pairs *) - Fixpoint split (l:list (A*B)) { struct l }: list A * list B := + Fixpoint split (l:list (A*B)) : list A * list B := match l with | nil => (nil, nil) | (x,y) :: tl => let (g,d) := split tl in (x::g, y::d) @@ -1402,7 +1400,7 @@ End Fold_Right_Recursor. Lists given to [combine] are meant to be of same length. If not, [combine] stops on the shorter list *) - Fixpoint combine (l : list A) (l' : list B){struct l} : list (A*B) := + Fixpoint combine (l : list A) (l' : list B) : list (A*B) := match l,l' with | x::tl, y::tl' => (x,y)::(combine tl tl') | _, _ => nil @@ -1470,7 +1468,7 @@ End Fold_Right_Recursor. [combine], it adds every possible pairs, not only those at the same position. *) - Fixpoint list_prod (l:list A) (l':list B) {struct l} : + Fixpoint list_prod (l:list A) (l':list B) : list (A * B) := match l with | nil => nil @@ -1661,7 +1659,7 @@ Section Cutting. Variable A : Type. - Fixpoint firstn (n:nat)(l:list A) {struct n} : list A := + Fixpoint firstn (n:nat)(l:list A) : list A := match n with | 0 => nil | S n => match l with @@ -1670,7 +1668,7 @@ Section Cutting. end end. - Fixpoint skipn (n:nat)(l:list A) { struct n } : list A := + Fixpoint skipn (n:nat)(l:list A) : list A := match n with | 0 => l | S n => match l with @@ -1804,7 +1802,7 @@ Section NatSeq. (** [seq] computes the sequence of [len] contiguous integers that starts at [start]. For instance, [seq 2 3] is [2::3::4::nil]. *) - Fixpoint seq (start len:nat) {struct len} : list nat := + Fixpoint seq (start len:nat) : list nat := match len with | 0 => nil | S len => start :: seq (S start) len diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v index d8a8183f3..e6c3a435b 100644 --- a/theories/Lists/ListSet.v +++ b/theories/Lists/ListSet.v @@ -27,7 +27,7 @@ Section first_definitions. Definition empty_set : set := nil. - Fixpoint set_add (a:A) (x:set) {struct x} : set := + Fixpoint set_add (a:A) (x:set) : set := match x with | nil => a :: nil | a1 :: x1 => @@ -38,7 +38,7 @@ Section first_definitions. end. - Fixpoint set_mem (a:A) (x:set) {struct x} : bool := + Fixpoint set_mem (a:A) (x:set) : bool := match x with | nil => false | a1 :: x1 => @@ -49,7 +49,7 @@ Section first_definitions. end. (** If [a] belongs to [x], removes [a] from [x]. If not, does nothing *) - Fixpoint set_remove (a:A) (x:set) {struct x} : set := + Fixpoint set_remove (a:A) (x:set) : set := match x with | nil => empty_set | a1 :: x1 => @@ -67,14 +67,14 @@ Section first_definitions. if set_mem a1 y then a1 :: set_inter x1 y else set_inter x1 y end. - Fixpoint set_union (x y:set) {struct y} : set := + Fixpoint set_union (x y:set) : set := match y with | nil => x | a1 :: y1 => set_add a1 (set_union x y1) end. (** returns the set of all els of [x] that does not belong to [y] *) - Fixpoint set_diff (x y:set) {struct x} : set := + Fixpoint set_diff (x y:set) : set := match x with | nil => nil | a1 :: x1 => diff --git a/theories/Lists/StreamMemo.v b/theories/Lists/StreamMemo.v index e10ad325f..d906cfa44 100644 --- a/theories/Lists/StreamMemo.v +++ b/theories/Lists/StreamMemo.v @@ -80,7 +80,7 @@ Variable f: forall n, A n. Inductive memo_val: Type := memo_mval: forall n, A n -> memo_val. -Fixpoint is_eq (n m : nat) {struct n}: {n = m} + {True} := +Fixpoint is_eq (n m : nat) : {n = m} + {True} := match n, m return {n = m} + {True} with | 0, 0 =>left True (refl_equal 0) | 0, S m1 => right (0 = S m1) I diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v index ace157749..3fa053b7f 100644 --- a/theories/Lists/Streams.v +++ b/theories/Lists/Streams.v @@ -29,7 +29,7 @@ Definition tl (x:Stream) := match x with end. -Fixpoint Str_nth_tl (n:nat) (s:Stream) {struct n} : Stream := +Fixpoint Str_nth_tl (n:nat) (s:Stream) : Stream := match n with | O => s | S m => Str_nth_tl m (tl s) diff --git a/theories/Lists/TheoryList.v b/theories/Lists/TheoryList.v index 5185f2c53..da3018a48 100644 --- a/theories/Lists/TheoryList.v +++ b/theories/Lists/TheoryList.v @@ -97,7 +97,7 @@ Qed. (****************************************) (* length is defined in List *) -Fixpoint Length_l (l:list A) (n:nat) {struct l} : nat := +Fixpoint Length_l (l:list A) (n:nat) : nat := match l with | nil => n | _ :: m => Length_l m (S n) @@ -146,7 +146,7 @@ Hint Resolve allS_nil allS_cons. Hypothesis eqA_dec : forall a b:A, {a = b} + {a <> b}. -Fixpoint mem (a:A) (l:list A) {struct l} : bool := +Fixpoint mem (a:A) (l:list A) : bool := match l with | nil => false | b :: m => if eqA_dec a b then true else mem a m @@ -201,7 +201,7 @@ Lemma nth_le_length : induction 1; simpl in |- *; auto with arith. Qed. -Fixpoint Nth_func (l:list A) (n:nat) {struct l} : Exc A := +Fixpoint Nth_func (l:list A) (n:nat) : Exc A := match l, n with | a :: _, S O => value a | _ :: l', S (S p) => Nth_func l' (S p) @@ -237,7 +237,7 @@ Qed. Require Import Minus. Require Import DecBool. -Fixpoint index_p (a:A) (l:list A) {struct l} : nat -> Exc nat := +Fixpoint index_p (a:A) (l:list A) : nat -> Exc nat := match l with | nil => fun p => error | b :: m => fun p => ifdec (eqA_dec a b) (value p) (index_p a m (S p)) @@ -359,7 +359,7 @@ End Find_sec. Section Assoc_sec. Variable B : Type. -Fixpoint assoc (a:A) (l:list (A * B)) {struct l} : +Fixpoint assoc (a:A) (l:list (A * B)) : Exc B := match l with | nil => error diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v index a35682767..2456e1706 100644 --- a/theories/NArith/Ndigits.v +++ b/theories/NArith/Ndigits.v @@ -17,7 +17,7 @@ Require Import BinNat. (** [xor] *) -Fixpoint Pxor (p1 p2:positive) {struct p1} : N := +Fixpoint Pxor (p1 p2:positive) : N := match p1, p2 with | xH, xH => N0 | xH, xO p2 => Npos (xI p2) @@ -409,7 +409,7 @@ Qed. (** a lexicographic order on bits, starting from the lowest bit *) -Fixpoint Nless_aux (a a':N) (p:positive) {struct p} : bool := +Fixpoint Nless_aux (a a':N) (p:positive) : bool := match p with | xO p' => Nless_aux (Ndiv2 a) (Ndiv2 a') p' | _ => andb (negb (Nbit0 a)) (Nbit0 a') @@ -579,7 +579,7 @@ Definition N2Bv (n:N) : Bvector (Nsize n) := | Npos p => P2Bv p end. -Fixpoint Bv2N (n:nat)(bv:Bvector n) {struct bv} : N := +Fixpoint Bv2N (n:nat)(bv:Bvector n) : N := match bv with | Vnil => N0 | Vcons false n bv => Ndouble (Bv2N n bv) @@ -629,7 +629,7 @@ Qed. (** To state nonetheless a second result about composition of conversions, we define a conversion on a given number of bits : *) -Fixpoint N2Bv_gen (n:nat)(a:N) { struct n } : Bvector n := +Fixpoint N2Bv_gen (n:nat)(a:N) : Bvector n := match n return Bvector n with | 0 => Bnil | S n => match a with diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index 9b7ea0474..c4d06fd72 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -27,7 +27,7 @@ Section Well_founded. Variable F_sub : forall x:A, (forall y: { y : A | R y x }, P (proj1_sig y)) -> P x. - Fixpoint Fix_F_sub (x : A) (r : Acc R x) {struct r} : P x := + Fixpoint Fix_F_sub (x : A) (r : Acc R x) : P x := F_sub x (fun y: { y : A | R y x} => Fix_F_sub (proj1_sig y) (Acc_inv r (proj2_sig y))). diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v index 266d81e01..34d6267e3 100644 --- a/theories/QArith/Qcanon.v +++ b/theories/QArith/Qcanon.v @@ -449,7 +449,7 @@ Qed. (** Rational to the n-th power *) -Fixpoint Qcpower (q:Qc)(n:nat) { struct n } : Qc := +Fixpoint Qcpower (q:Qc)(n:nat) : Qc := match n with | O => 1 | S n => q * (Qcpower q n) diff --git a/theories/Reals/RList.v b/theories/Reals/RList.v index a95985d3b..545bd68b2 100644 --- a/theories/Reals/RList.v +++ b/theories/Reals/RList.v @@ -16,7 +16,7 @@ Inductive Rlist : Type := | nil : Rlist | cons : R -> Rlist -> Rlist. -Fixpoint In (x:R) (l:Rlist) {struct l} : Prop := +Fixpoint In (x:R) (l:Rlist) : Prop := match l with | nil => False | cons a l' => x = a \/ In x l' @@ -70,7 +70,7 @@ Proof. reflexivity. Qed. -Fixpoint AbsList (l:Rlist) (x:R) {struct l} : Rlist := +Fixpoint AbsList (l:Rlist) (x:R) : Rlist := match l with | nil => nil | cons a l' => cons (Rabs (a - x) / 2) (AbsList l' x) @@ -150,7 +150,7 @@ Proof. left; reflexivity. Qed. -Fixpoint pos_Rl (l:Rlist) (i:nat) {struct l} : R := +Fixpoint pos_Rl (l:Rlist) (i:nat) : R := match l with | nil => 0 | cons a l' => match i with @@ -221,7 +221,7 @@ Qed. Definition ordered_Rlist (l:Rlist) : Prop := forall i:nat, (i < pred (Rlength l))%nat -> pos_Rl l i <= pos_Rl l (S i). -Fixpoint insert (l:Rlist) (x:R) {struct l} : Rlist := +Fixpoint insert (l:Rlist) (x:R) : Rlist := match l with | nil => cons x nil | cons a l' => @@ -231,25 +231,25 @@ Fixpoint insert (l:Rlist) (x:R) {struct l} : Rlist := end end. -Fixpoint cons_Rlist (l k:Rlist) {struct l} : Rlist := +Fixpoint cons_Rlist (l k:Rlist) : Rlist := match l with | nil => k | cons a l' => cons a (cons_Rlist l' k) end. -Fixpoint cons_ORlist (k l:Rlist) {struct k} : Rlist := +Fixpoint cons_ORlist (k l:Rlist) : Rlist := match k with | nil => l | cons a k' => cons_ORlist k' (insert l a) end. -Fixpoint app_Rlist (l:Rlist) (f:R -> R) {struct l} : Rlist := +Fixpoint app_Rlist (l:Rlist) (f:R -> R) : Rlist := match l with | nil => nil | cons a l' => cons (f a) (app_Rlist l' f) end. -Fixpoint mid_Rlist (l:Rlist) (x:R) {struct l} : Rlist := +Fixpoint mid_Rlist (l:Rlist) (x:R) : Rlist := match l with | nil => nil | cons a l' => cons ((x + a) / 2) (mid_Rlist l' a) diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v index 11be9772e..7371c8acf 100644 --- a/theories/Reals/Rfunctions.v +++ b/theories/Reals/Rfunctions.v @@ -676,7 +676,7 @@ Definition decimal_exp (r:R) (z:Z) : R := (r * 10 ^Z z). (** * Sum of n first naturals *) (*******************************) (*********) -Boxed Fixpoint sum_nat_f_O (f:nat -> nat) (n:nat) {struct n} : nat := +Boxed Fixpoint sum_nat_f_O (f:nat -> nat) (n:nat) : nat := match n with | O => f 0%nat | S n' => (sum_nat_f_O f n' + f (S n'))%nat @@ -696,7 +696,7 @@ Definition sum_nat (s n:nat) : nat := sum_nat_f s n (fun x:nat => x). (** * Sum *) (*******************************) (*********) -Fixpoint sum_f_R0 (f:nat -> R) (N:nat) {struct N} : R := +Fixpoint sum_f_R0 (f:nat -> R) (N:nat) : R := match N with | O => f 0%nat | S i => sum_f_R0 f i + f (S i) diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v index 63684c1f3..ae2c3d77f 100644 --- a/theories/Reals/RiemannInt.v +++ b/theories/Reals/RiemannInt.v @@ -466,7 +466,7 @@ Proof. elim (Rlt_irrefl _ H7) ] ]. Qed. -Fixpoint SubEquiN (N:nat) (x y:R) (del:posreal) {struct N} : Rlist := +Fixpoint SubEquiN (N:nat) (x y:R) (del:posreal) : Rlist := match N with | O => cons y nil | S p => cons x (SubEquiN p (x + del) y del) diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v index e7f0375f0..f9b1b890f 100644 --- a/theories/Reals/RiemannInt_SF.v +++ b/theories/Reals/RiemannInt_SF.v @@ -149,7 +149,7 @@ Definition subdivision_val (a b:R) (f:StepFun a b) : Rlist := | existT a b => a end. -Boxed Fixpoint Int_SF (l k:Rlist) {struct l} : R := +Boxed Fixpoint Int_SF (l k:Rlist) : R := match l with | nil => 0 | cons a l' => diff --git a/theories/Reals/Rpow_def.v b/theories/Reals/Rpow_def.v index c9fb56292..c7d1893be 100644 --- a/theories/Reals/Rpow_def.v +++ b/theories/Reals/Rpow_def.v @@ -10,7 +10,7 @@ Require Import Rdefinitions. -Fixpoint pow (r:R) (n:nat) {struct n} : R := +Fixpoint pow (r:R) (n:nat) : R := match n with | O => R1 | S n => Rmult r (pow r n) diff --git a/theories/Reals/Rprod.v b/theories/Reals/Rprod.v index f02b77564..bb3df6bb8 100644 --- a/theories/Reals/Rprod.v +++ b/theories/Reals/Rprod.v @@ -17,7 +17,7 @@ Require Import Binomial. Open Local Scope R_scope. (** TT Ak; 0<=k<=N *) -Boxed Fixpoint prod_f_R0 (f:nat -> R) (N:nat) {struct N} : R := +Boxed Fixpoint prod_f_R0 (f:nat -> R) (N:nat) : R := match N with | O => f O | S p => prod_f_R0 f p * f (S p) diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v index 87d8e1350..1f90c06cf 100644 --- a/theories/Strings/Ascii.v +++ b/theories/Strings/Ascii.v @@ -59,7 +59,7 @@ Defined. looking at the last n bits, ie z mod 2^n *) Fixpoint ascii_of_pos_aux (res acc : ascii) (z : positive) - (n : nat) {struct n} : ascii := + (n : nat) : ascii := match n with | O => res | S n1 => diff --git a/theories/Strings/String.v b/theories/Strings/String.v index 21c0a15e9..15f298218 100644 --- a/theories/Strings/String.v +++ b/theories/Strings/String.v @@ -38,7 +38,7 @@ Defined. Reserved Notation "x ++ y" (right associativity, at level 60). -Fixpoint append (s1 s2 : string) {struct s1} : string := +Fixpoint append (s1 s2 : string) : string := match s1 with | EmptyString => s2 | String c s1' => String c (s1' ++ s2) @@ -122,7 +122,7 @@ Qed. at position [n] and of length [m]; if this does not make sense it returns [""] *) -Fixpoint substring (n m : nat) (s : string) {struct s} : string := +Fixpoint substring (n m : nat) (s : string) : string := match n, m, s with | 0, 0, _ => EmptyString | 0, S m', EmptyString => s @@ -205,7 +205,7 @@ Qed. (** Test if, starting at position [n], [s1] occurs in [s2]; if so it returns the position *) -Fixpoint index (n : nat) (s1 s2 : string) {struct s2} : option nat := +Fixpoint index (n : nat) (s1 s2 : string) : option nat := match s2, n with | EmptyString, 0 => match s1 with diff --git a/theories/ZArith/ZOdiv_def.v b/theories/ZArith/ZOdiv_def.v index c73b6f091..88d573bb0 100644 --- a/theories/ZArith/ZOdiv_def.v +++ b/theories/ZArith/ZOdiv_def.v @@ -17,7 +17,7 @@ Definition NPgeb (a:N)(b:positive) := | Npos na => match Pcompare na b Eq with Lt => false | _ => true end end. -Fixpoint Pdiv_eucl (a b:positive) {struct a} : N * N := +Fixpoint Pdiv_eucl (a b:positive) : N * N := match a with | xH => match b with xH => (1, 0)%N | _ => (0, 1)%N end diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v index 0929d965a..08cc564de 100644 --- a/theories/ZArith/Zcomplements.v +++ b/theories/ZArith/Zcomplements.v @@ -160,7 +160,7 @@ Qed. Require Import List. -Fixpoint Zlength_aux (acc:Z) (A:Type) (l:list A) {struct l} : Z := +Fixpoint Zlength_aux (acc:Z) (A:Type) (l:list A) : Z := match l with | nil => acc | _ :: l => Zlength_aux (Zsucc acc) A l diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index bc35ba405..f3e656970 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -35,8 +35,7 @@ Open Local Scope Z_scope. *) -Unboxed Fixpoint Zdiv_eucl_POS (a:positive) (b:Z) {struct a} : - Z * Z := +Unboxed Fixpoint Zdiv_eucl_POS (a:positive) (b:Z) : Z * Z := match a with | xH => if Zge_bool b 2 then (0, 1) else (1, 0) | xO a' => @@ -1071,7 +1070,7 @@ Qed. (** * A direct way to compute Zmod *) -Fixpoint Zmod_POS (a : positive) (b : Z) {struct a} : Z := +Fixpoint Zmod_POS (a : positive) (b : Z) : Z := match a with | xI a' => let r := Zmod_POS a' b in diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v index 93ac74d54..178ae5f15 100644 --- a/theories/ZArith/Zmisc.v +++ b/theories/ZArith/Zmisc.v @@ -20,7 +20,7 @@ Open Local Scope Z_scope. (** [n]th iteration of the function [f] *) -Fixpoint iter_pos (n:positive) (A:Type) (f:A -> A) (x:A) {struct n} : A := +Fixpoint iter_pos (n:positive) (A:Type) (f:A -> A) (x:A) : A := match n with | xH => f x | xO n' => iter_pos n' A f (iter_pos n' A f x) diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v index 23a2e510f..2a2751c9d 100644 --- a/theories/ZArith/Znumtheory.v +++ b/theories/ZArith/Znumtheory.v @@ -892,7 +892,7 @@ Qed. Open Scope positive_scope. -Fixpoint Pgcdn (n: nat) (a b : positive) { struct n } : positive := +Fixpoint Pgcdn (n: nat) (a b : positive) : positive := match n with | O => 1 | S n => @@ -1255,7 +1255,7 @@ Qed. Open Scope positive_scope. -Fixpoint Pggcdn (n: nat) (a b : positive) { struct n } : (positive*(positive*positive)) := +Fixpoint Pggcdn (n: nat) (a b : positive) : (positive*(positive*positive)) := match n with | O => (1,(a,b)) | S n => diff --git a/theories/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v index 39aab6331..1d9b3dfc9 100644 --- a/theories/ZArith/Zpow_facts.v +++ b/theories/ZArith/Zpow_facts.v @@ -294,7 +294,7 @@ Qed. (** A direct way to compute Zpower modulo **) -Fixpoint Zpow_mod_pos (a: Z)(m: positive)(n : Z) {struct m} : Z := +Fixpoint Zpow_mod_pos (a: Z)(m: positive)(n : Z) : Z := match m with | xH => a mod n | xO m' => |