From ffb64d16132dd80f72ecb619ef87e3eee1fa8bda Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 5 Jul 2012 16:56:37 +0000 Subject: Kills the useless tactic annotations "in |- *" Most of these heavyweight annotations were introduced a long time ago by the automatic 7.x -> 8.0 translator git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15518 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Wellfounded/Disjoint_Union.v | 2 +- theories/Wellfounded/Inclusion.v | 2 +- theories/Wellfounded/Inverse_Image.v | 4 ++-- .../Wellfounded/Lexicographic_Exponentiation.v | 26 +++++++++++----------- theories/Wellfounded/Lexicographic_Product.v | 6 ++--- theories/Wellfounded/Transitive_Closure.v | 4 ++-- theories/Wellfounded/Union.v | 4 ++-- theories/Wellfounded/Well_Ordering.v | 6 ++--- 8 files changed, 27 insertions(+), 27 deletions(-) (limited to 'theories/Wellfounded') diff --git a/theories/Wellfounded/Disjoint_Union.v b/theories/Wellfounded/Disjoint_Union.v index f5daa3014..ec0dfeb81 100644 --- a/theories/Wellfounded/Disjoint_Union.v +++ b/theories/Wellfounded/Disjoint_Union.v @@ -41,7 +41,7 @@ Section Wf_Disjoint_Union. well_founded leA -> well_founded leB -> well_founded Le_AsB. Proof. intros. - unfold well_founded in |- *. + unfold well_founded. destruct a as [a| b]. apply (acc_A_sum a). apply (H a). diff --git a/theories/Wellfounded/Inclusion.v b/theories/Wellfounded/Inclusion.v index 1c83c4816..73d66c847 100644 --- a/theories/Wellfounded/Inclusion.v +++ b/theories/Wellfounded/Inclusion.v @@ -24,7 +24,7 @@ Section WfInclusion. Theorem wf_incl : inclusion A R1 R2 -> well_founded R2 -> well_founded R1. Proof. - unfold well_founded in |- *; auto with sets. + unfold well_founded; auto with sets. Qed. End WfInclusion. diff --git a/theories/Wellfounded/Inverse_Image.v b/theories/Wellfounded/Inverse_Image.v index 27a1c3811..db89cb356 100644 --- a/theories/Wellfounded/Inverse_Image.v +++ b/theories/Wellfounded/Inverse_Image.v @@ -31,7 +31,7 @@ Section Inverse_Image. Theorem wf_inverse_image : well_founded R -> well_founded Rof. Proof. - red in |- *; intros; apply Acc_inverse_image; auto. + red; intros; apply Acc_inverse_image; auto. Qed. Variable F : A -> B -> Prop. @@ -49,7 +49,7 @@ Section Inverse_Image. Theorem wf_inverse_rel : well_founded R -> well_founded RoF. Proof. - red in |- *; constructor; intros. + red; constructor; intros. case H0; intros. apply (Acc_inverse_rel x); auto. Qed. diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v index 6d5b663bd..fe2d83250 100644 --- a/theories/Wellfounded/Lexicographic_Exponentiation.v +++ b/theories/Wellfounded/Lexicographic_Exponentiation.v @@ -36,11 +36,11 @@ Section Wf_Lexicographic_Exponentiation. Proof. simple induction x. simple induction z. - simpl in |- *; intros H. + simpl; intros H. inversion_clear H. - simpl in |- *; intros; apply (Lt_nil A leA). + simpl; intros; apply (Lt_nil A leA). intros a l HInd. - simpl in |- *. + simpl. intros. inversion_clear H. apply (Lt_hd A leA); auto with sets. @@ -54,7 +54,7 @@ Section Wf_Lexicographic_Exponentiation. ltl x (y ++ z) -> ltl x y \/ (exists y' : List, x = y ++ y' /\ ltl y' z). Proof. intros x y; generalize x. - elim y; simpl in |- *. + elim y; simpl. right. exists x0; auto with sets. intros. @@ -196,7 +196,7 @@ Section Wf_Lexicographic_Exponentiation. Descl x0 /\ Descl (l0 ++ Cons x1 Nil)). - simpl in |- *. + simpl. split. generalize (app_inj_tail _ _ _ _ H2); simple induction 1. simple induction 1; auto with sets. @@ -239,7 +239,7 @@ Section Wf_Lexicographic_Exponentiation. Proof. intros a b x. case x. - simpl in |- *. + simpl. simple induction 1. intros. inversion H1; auto with sets. @@ -267,7 +267,7 @@ Section Wf_Lexicographic_Exponentiation. case x. intros; apply (Lt_nil A leA). - simpl in |- *; intros. + simpl; intros. inversion_clear H0. apply (Lt_hd A leA a b); auto with sets. @@ -284,17 +284,17 @@ Section Wf_Lexicographic_Exponentiation. apply (Acc_inv (R:=Lex_Exp) (x:=<< x1 ++ x2, y1 >>)). auto with sets. - unfold lex_exp in |- *; simpl in |- *; auto with sets. + unfold lex_exp; simpl; auto with sets. Qed. Theorem wf_lex_exp : well_founded leA -> well_founded Lex_Exp. Proof. - unfold well_founded at 2 in |- *. + unfold well_founded at 2. simple induction a; intros x y. apply Acc_intro. simple induction y0. - unfold lex_exp at 1 in |- *; simpl in |- *. + unfold lex_exp at 1; simpl. apply rev_ind with (A := A) (P := fun x:List => @@ -335,8 +335,8 @@ Section Wf_Lexicographic_Exponentiation. intro. apply Acc_intro. simple induction y2. - unfold lex_exp at 1 in |- *. - simpl in |- *; intros x4 y3. intros. + unfold lex_exp at 1. + simpl; intros x4 y3. intros. apply (H0 x4 y3); auto with sets. intros. @@ -357,7 +357,7 @@ Section Wf_Lexicographic_Exponentiation. generalize (HInd2 f); intro. apply Acc_intro. simple induction y3. - unfold lex_exp at 1 in |- *; simpl in |- *; intros. + unfold lex_exp at 1; simpl; intros. apply H15; auto with sets. Qed. diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v index 9a1d66f43..a0c639e4e 100644 --- a/theories/Wellfounded/Lexicographic_Product.v +++ b/theories/Wellfounded/Lexicographic_Product.v @@ -60,7 +60,7 @@ Section WfLexicographic_Product. well_founded leA -> (forall x:A, well_founded (leB x)) -> well_founded LexProd. Proof. - intros wfA wfB; unfold well_founded in |- *. + intros wfA wfB; unfold well_founded. destruct a. apply acc_A_B_lexprod; auto with sets; intros. red in wfB. @@ -94,7 +94,7 @@ Section Wf_Symmetric_Product. Lemma wf_symprod : well_founded leA -> well_founded leB -> well_founded Symprod. Proof. - red in |- *. + red. destruct a. apply Acc_symprod; auto with sets. Defined. @@ -161,7 +161,7 @@ Section Swap. Lemma wf_swapprod : well_founded R -> well_founded SwapProd. Proof. - red in |- *. + red. destruct a; intros. apply Acc_swapprod; auto with sets. Defined. diff --git a/theories/Wellfounded/Transitive_Closure.v b/theories/Wellfounded/Transitive_Closure.v index e9bc7ccf7..5d06c6c02 100644 --- a/theories/Wellfounded/Transitive_Closure.v +++ b/theories/Wellfounded/Transitive_Closure.v @@ -18,7 +18,7 @@ Section Wf_Transitive_Closure. Notation trans_clos := (clos_trans A R). Lemma incl_clos_trans : inclusion A R trans_clos. - red in |- *; auto with sets. + red; auto with sets. Qed. Lemma Acc_clos_trans : forall x:A, Acc R x -> Acc trans_clos x. @@ -39,7 +39,7 @@ Section Wf_Transitive_Closure. Theorem wf_clos_trans : well_founded R -> well_founded trans_clos. Proof. - unfold well_founded in |- *; auto with sets. + unfold well_founded; auto with sets. Defined. End Wf_Transitive_Closure. diff --git a/theories/Wellfounded/Union.v b/theories/Wellfounded/Union.v index e3fdc4c5e..c0aa1c0db 100644 --- a/theories/Wellfounded/Union.v +++ b/theories/Wellfounded/Union.v @@ -51,7 +51,7 @@ Section WfUnion. elim strip_commut with x x0 y0; auto with sets; intros. apply Acc_inv_trans with x1; auto with sets. - unfold union in |- *. + unfold union. elim H11; auto with sets; intros. apply t_trans with y1; auto with sets. @@ -65,7 +65,7 @@ Section WfUnion. Theorem wf_union : commut A R1 R2 -> well_founded R1 -> well_founded R2 -> well_founded Union. Proof. - unfold well_founded in |- *. + unfold well_founded. intros. apply Acc_union; auto with sets. Qed. diff --git a/theories/Wellfounded/Well_Ordering.v b/theories/Wellfounded/Well_Ordering.v index fc4e2ebce..452da1b2e 100644 --- a/theories/Wellfounded/Well_Ordering.v +++ b/theories/Wellfounded/Well_Ordering.v @@ -25,7 +25,7 @@ Section WellOrdering. Theorem wf_WO : well_founded le_WO. Proof. - unfold well_founded in |- *; intro. + unfold well_founded; intro. apply Acc_intro. elim a. intros. @@ -37,7 +37,7 @@ Section WellOrdering. apply (H v0 y0). cut (f = f1). intros E; rewrite E; auto. - symmetry in |- *. + symmetry . apply (inj_pair2 A (fun a0:A => B a0 -> WO) a0 f1 f H5). Qed. @@ -61,7 +61,7 @@ Section Characterisation_wf_relations. apply (well_founded_induction_type H (fun a:A => WO A B)); auto. intros x H1. apply (sup A B x). - unfold B at 1 in |- *. + unfold B at 1. destruct 1 as [x0]. apply (H1 x0); auto. Qed. -- cgit v1.2.3