diff options
author | mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-26 12:32:18 +0000 |
---|---|---|
committer | mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-26 12:32:18 +0000 |
commit | daa75d5ffb8dfdf414bed31fbfe1e91718d6a5dc (patch) | |
tree | 4c888414b13c0762a936223b64ccebaa317ffa59 /theories/Relations/Operators_Properties.v | |
parent | 75effdc265e716651c860d0878ffbfc205646cbd (diff) |
Retire les parentheses autour des tactiques
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@766 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Relations/Operators_Properties.v')
-rwxr-xr-x | theories/Relations/Operators_Properties.v | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/theories/Relations/Operators_Properties.v b/theories/Relations/Operators_Properties.v index 99b9eb715..e3da5130f 100755 --- a/theories/Relations/Operators_Properties.v +++ b/theories/Relations/Operators_Properties.v @@ -45,15 +45,15 @@ Save. Intros. Generalize H H0 . Clear H H0. -(Elim H1; Intros; Auto with sets). -(Apply H2 with x; Auto with sets). +Elim H1; Intros; Auto with sets. +Apply H2 with x; Auto with sets. Apply H3. -(Apply H0; Auto with sets). +Apply H0; Auto with sets. Intros. -(Apply H5 with P0; Auto with sets). -(Apply rt_trans with y; Auto with sets). +Apply H5 with P0; Auto with sets. +Apply rt_trans with y; Auto with sets. Save. @@ -65,9 +65,9 @@ Section Clos_Refl_Sym_Trans. Lemma clos_rt_clos_rst: (inclusion A (clos_refl_trans A R) (clos_refl_sym_trans A R)). Red. -(Induction 1; Auto with sets). +Induction 1; Auto with sets. Intros. -(Apply rst_trans with y0; Auto with sets). +Apply rst_trans with y0; Auto with sets. Save. Lemma clos_rst_is_equiv: (equivalence A (clos_refl_sym_trans A R)). @@ -83,9 +83,9 @@ Save. (incl (clos_refl_sym_trans A (clos_refl_sym_trans A R)) (clos_refl_sym_trans A R)). Red. -(Induction 1; Auto with sets). +Induction 1; Auto with sets. Intros. -(Apply rst_trans with y0; Auto with sets). +Apply rst_trans with y0; Auto with sets. Save. End Clos_Refl_Sym_Trans. |