diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-05 16:56:37 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-05 16:56:37 +0000 |
| commit | ffb64d16132dd80f72ecb619ef87e3eee1fa8bda (patch) | |
| tree | 5368562b42af1aeef7e19b4bd897c9fc5655769b /theories/Relations | |
| parent | a46ccd71539257bb55dcddd9ae8510856a5c9a16 (diff) | |
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
Diffstat (limited to 'theories/Relations')
| -rw-r--r-- | theories/Relations/Operators_Properties.v | 6 | ||||
| -rw-r--r-- | theories/Relations/Relations.v | 6 |
2 files changed, 6 insertions, 6 deletions
diff --git a/theories/Relations/Operators_Properties.v b/theories/Relations/Operators_Properties.v index f7f5512e7..3f3810083 100644 --- a/theories/Relations/Operators_Properties.v +++ b/theories/Relations/Operators_Properties.v @@ -50,7 +50,7 @@ Section Properties. Lemma clos_rt_idempotent : inclusion (R*)* R*. Proof. - red in |- *. + red. induction 1; auto with sets. intros. apply rt_trans with y; auto with sets. @@ -66,7 +66,7 @@ Section Properties. Lemma clos_rt_clos_rst : inclusion (clos_refl_trans R) (clos_refl_sym_trans R). Proof. - red in |- *. + red. induction 1; auto with sets. apply rst_trans with y; auto with sets. Qed. @@ -87,7 +87,7 @@ Section Properties. inclusion (clos_refl_sym_trans (clos_refl_sym_trans R)) (clos_refl_sym_trans R). Proof. - red in |- *. + red. induction 1; auto with sets. apply rst_trans with y; auto with sets. Qed. diff --git a/theories/Relations/Relations.v b/theories/Relations/Relations.v index f9fb2c442..ed2567396 100644 --- a/theories/Relations/Relations.v +++ b/theories/Relations/Relations.v @@ -14,16 +14,16 @@ Lemma inverse_image_of_equivalence : forall (A B:Type) (f:A -> B) (r:relation B), equivalence B r -> equivalence A (fun x y:A => r (f x) (f y)). Proof. - intros; split; elim H; red in |- *; auto. + intros; split; elim H; red; auto. intros _ equiv_trans _ x y z H0 H1; apply equiv_trans with (f y); assumption. Qed. Lemma inverse_image_of_eq : forall (A B:Type) (f:A -> B), equivalence A (fun x y:A => f x = f y). Proof. - split; red in |- *; + split; red; [ (* reflexivity *) reflexivity | (* transitivity *) intros; transitivity (f y); assumption - | (* symmetry *) intros; symmetry in |- *; assumption ]. + | (* symmetry *) intros; symmetry ; assumption ]. Qed. |